Solving SAT by an Iterative Version of the Inclusion-Exclusion Principle

摘要

Our goal is to present a basic, novel, and correct SAT solver algorithm, show its soundness, compare it with a standard SAT solver, give some ideas in which cases might it be competitive. We do not present a fine-tuned, state-of-the-art SAT solver, only a new basic algorithm. So we introduce CCC, a SAT solver algorithm which is an iterative version of the inclusion-exclusion principle. CCC stands for Counting Clear Clauses. It counts those full length (in our terminology: clear) clauses, which are subsumed by the input SAT problem. Full length clauses are n-clauses, where n is the number of variables in the input problem. A SAT problem is satisfiable if it does not subsume all n-clauses. The idea is that in an n-clause each of n variables is present either as a positive literal or as a negative one. So we can represent them by n bits. CCC is motivated by the inclusion-exclusion principle, it counts full length clauses as the principle does in case of the SAT problem, but in an iterative way. It works in the following way: It sets its counter to be 0. It converts 0 to an n-clause, which is the one with only negative literals. It checks whether this n-clause is subsumed by the input SAT problem. If yes, it increases the counter and repeats the loop. If not, we have a model, which is given by the negation of this n-clause. We show that almost always we can increase the counter by more than one. We show that this algorithm always stops and finds a model if there is one. We present a worst case time complexity analysis and lot of test results. The test results show that this basic algorithm can outperform a standard SAT solver, although its implementation is very simple without any optimization. CCC is competitive if the input problem contains lot of short clauses. Our implementation can be downloaded and the reader is welcome to make a better solver out of it. We believe that this new algorithm could serve as a good basis for parallel algorithms, because its memory usa- e is constant and no communication is needed between the nodes.