An early sign of satisfiability

TL;DR

This paper introduces unipolar set termination (UST), an early sign of satisfiability in SAT problems, which can speed up solving by terminating earlier when unipolar clause sets are detected, especially in skewed real-world instances.

Contribution

The paper proposes the novel concept of unipolar set termination (UST) as an early satisfiability indicator and demonstrates its effectiveness in speeding up SAT solving, particularly for skewed instances.

Findings

UST can significantly speed up SAT solving on real-world benchmarks.

The efficiency of UST increases with the skewness of the SAT set.

Revealing hidden skewness further enhances UST performance.

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).