An early sign of satisfiability

Abstract

This note considers checking satisfiability of sets of propositional clauses (SAT instances). It shows that "unipolar sets" of clauses (containing no positive or no negative clauses) provide an "early sign" of satisfiability of SAT instances before all the clauses become satisfied in the course of solving SAT problems. At this sign the processing can be terminated by "unipolar set termination", UST thus before it is usually done by SAT solvers (Table 1). An analysis of benchmark SAT instances used at SAT Competitions shows that UST can speed up solving SAT instances stemming from many real-world problems. The efficiency of UST increases with the "skewness" of the SAT set being checked, that is the difference between probabilities of negated and unnegated literals in the set. Many real-world problems, by virtue of their semantics, are skewed (Table 2). The efficiency of UST can be increased by revealing the "hidden skewness" of SAT sets (Table 3).