Held by Gabor Kusper in 16 July 2020 on Zoom
Abstract
We will discuss 3 topics:
How to state the pre- and postconditions in Java;
How does the CSFLOC SAT solver work;
What is the Black-and-White SAT problem.
How to state the pre- and postconditions in Java?
Actually, we have several ways. The first is a must: we use the self documenting facility of Java to state in natural language what is the pre- and postcondition of the next method. The next way is very popular and it is called TDD: Test Driven Development. In this case, we write several unit tests for each method which serve as the documentation of the method. We have to write also tests, which cover the cases what happens if the caller violates the precondition and the rest of them defines cases to check the postcondition. The next possibility is to use assert. Assert is just a normal statement. It checks runtime whether the given condition holds or not. If not then it raises an error, so it stops the program. It has the advantage that we can turn this on and off. We teach these techniques in the frame of programming technologies.
How does the CSFLOC SAT solver work?
This SAT solver is based on the Clear Clause View. A clear clause, or full length clause is a clause where each variable is present either as a positive or negative literal. If we use the symbols: +, -, x to depict positive literals, negative literals, and no occurrence, respectively; then clear clause means no x symbol in the clause. The Clear Clause View means that we understand a clause as the set of its subsumed full-length clauses. It is easy to see that there are pow(2,n) full-length clauses. A SAT instance is unsatisfiable if it subsums all possible full-length clauses, satisfiable otherwise. CSFLOC counts the subsumed full-length clauses of the input SAT instance. It uses ordered clauses, where variables has an index from 1 to n. It is based on several lemma. We will discuss those lemmas and show that CSFLOC is sound and complex. We will see also some code fragments, call options and runtime results.
What is the Black-and-White SAT problem?
The Black-and-White SAT problem is a special SAT problem, which has only two solutions, and those solutions are the opposite of each other. Usually the solutions are the white assignment, where each variable is true, or the black one, where each variable is false. The notion is motivated by directed graphs (digraphs). We can represent a digraph as CNF formula in the following way: each edge, say (A, B), can be represent by implication, like A implies B, i.e., not A or B, and these subformulea are connected by conjunctions. In this way we get a 2-SAT representation what we call the strong model of digraphs. We show that if the input digraph is strongly connected then its representation is a Black-and-White SAT problem. We also introduce other digraph representation, which have the same property: if the input is a strongly connected digraph, then the output is a Black-and-White SAT problem. We also show some corollaries.