Introduction

Many practical problems of computer science are in the complexity class NP. There are many well studied formalisms that can handle problems of this class, among them are constraint satisfaction [20], answer set programming [7], or satisfiability checking [3]. Although the two former formalisms admit a richer language, the latter approach is still very competitive even if the expressivity of its language is comparatively low.

The propositional satisfiability problem (SAT) consists of a propositional formula and asks whether there is a satisfying assignment for the Boolean variables occurring in the formula. From a complexity theory point of view SAT is NPcomplete [4] and, thus, intractable. Still, there are many industrial and academic applications that can be solved nicely with modern SAT solvers. For instance a SAT-based railway scheduling software outperformed the native version [9]. Likewise, haplotype matching [13] can be solved nicely with modern SAT solvers.

The success of the SAT approach lies in the strength of today's SAT solvers. SAT solvers do not operate on testing all possible variable assignments, but on constructing an assignment by successively interleaving two processes, viz., guessing and propagating the assignment of literals. The main inference rule is unit propagation, an efficient form of resolution. Combined with a decision rule it is the core of the basic algorithm known as the DPLL algorithm [5]. In the case that a contradiction is found in the formula with respect to the current variable assignment, advanced SAT solvers backtrack and learn a conflict clause which prevents the current and similar conflicts. With the addition of so-called learned clauses the basic algorithm is known as CDCL algorithm [16].

Modern systematic SAT solvers are highly tuned and complex proof procedures employing many advanced techniques like clause learning [16], nonchronological backtracking, restarts [8], clause removal [2,6], decision heuristics [2,17], and formula simplification techniques [12]. Specialized, cache-conscious data structures [10] further improve the performance. This way, today's solvers like Riss, 1 MiniSAT or Lingeling can handle formulas with millions of variables and millions of clauses.

However, the success of modern solvers carries a price tag: increased code complexity. Successful SAT solvers like the above mentioned ones consist of multiple thousand lines of code and are written in programming languages with side effects like C or C++. Due to the code complexity, the behavior of SAT solvers is hard to understand and state-of-the-art SAT solver internals are hard to teach. Moreover, finding additional techniques and integrating them into a SAT solver is getting more complex, as we have to consider the interplay with all the remaining techniques. Consequently, abstracting from specific algorithms, data structures, and heuristics is extremely important in order to discover and prove properties of a modern SAT solver as well as to understand the principles of SAT solving.

This problem was tackled by different formalizations, notably Linearized DPLL [1], Rule-based SAT Solver Descriptions [15], and Abstract DPLL [18]. However, these systems do not appropriately model modern SAT solvers anymore. In particular, preprocessing and applying preprocessing techniques interleaved with search, known as inprocessing, became a crucial part in SAT solving. Applying formula simplification techniques also during search is an attractive idea since it allows to use valuable formula simplifications while taking learned clauses into account. For example, the SAT solver Lingeling benefits considerably from this approach.

The contribution of this paper is the formalism Generic CDCL that models the computation of modern SAT solvers. Equipped with a small set of simple state transition rules, we can model all well-established techniques like preprocessing, inprocessing, restarts, clause sharing, as well as clause learning and forgetting. This formalism allows us to reason about the behavior of SAT solvers independently of the specific implementation. Additionally, the framework is a first step to explain how modern SAT solvers are working in a compact and easy way. Besides the presentation of Generic CDCL, the main result of this paper is the proof that Generic CDCL and, consequently, all its instances are sound.

The paper is structured as follows: In Section 2 we describe basic concepts of satisfiability testing. We present Generic CDCL in Section 3, where we also prove that Generic CDCL correctly solves the satisfiability problems. Afterwards, we compare Generic CDCL with related formalism in Section 4 and we conclude the paper in Section 5.

Preliminaries

The Satisfiability Problem

We assume a fixed infinite set V of Boolean variables. A literal is a variable v (positive literal ) or a negated variable v (negative literal ). The complement x of a positive (negative, resp.) literal x is the negative (positive, resp.) literal with the same variable as x. The complement of a set S of literals, denoted with S, is defined as S = {x | x ∈ S}. Finite sets of clauses are called formulas, where a clause is a finite set of literals. Sometimes, we write a clause {x 1 , . . . , x n } also as the disjunction (x 1 ∨ . . . ∨ x n ) and a formula {C 1 , . . . , C n } as the conjunction (C 1 ∧ . . . ∧ C n ). The empty clause is denoted by ⊥, the empty formula by . The formula obtained from F by replacing all occurrences of the variable v by the variable w is denoted by F [v → w]. The set of all variables occurring in a formula F (in positive or negative literals) is denoted by vars(F ); the set of all literals occurring in F by lits(F ). For instance, if x, y ∈ V, then F = {{x, y}, {y}} is a formula, its alternative representation using logical connectives is (x ∨ y) ∧ y, vars(F ) = {x, y}, and lits(F ) = {x, y}.

The semantics of formulas is based on the notion of an interpretation. An interpretation I is a set of literals which does not contain a complementary pair x, x of literals. An interpretation

I is total iff for each v ∈ V either v ∈ I or v ∈ I.

The satisfaction relation |= is defined as follows: Let I be an interpretation, then

I |= , I |= ⊥, I |= (x 1 ∨ . . . ∨ x n ) iff I |= x i for some i ∈ {1, . . . , n}, and I |= (C 1 ∧ . . . ∧ C n ) iff I |= C i for all i ∈ {1, . . . , n}.

Interpretation I is a model for the formula F iff I |= F . In the case that a formula F has a model, then F is satisfiable, otherwise it is unsatisfiable.

We relate formulas by three relations: the entailment, the equivalence and the equisatisfiability relation: Formula F entails formula F iff every total model of F is a model of F . Two formulas F and F are equivalent, in symbols F ≡ F , iff F entails F and F entails F . Two formulas F and F are equisatisfiable, in symbols F ≡ sat F , iff either both are satisfiable or both are unsatisfiable.

For instance, the interpretation I = {x, ¬z} is a model of the formula F 1 = (x ∨ y) ∧ (x ∨ z) and, therefore, F is satisfiable. The formula F 2 = x ∧ x has no model and, therefore, is unsatisfiable. The formula F 3 = x ∧ z is satisfiable and, therefore, the formulas F 1 and F 3 are equisatisfiable, but the formulas F 1 and F 2 are not equisatisfiable. In fact, F 3 |= F 1 since every total model I of the formula F 3 must contain x and z and, hence, the two clauses of F 1 are satisfied by I. Finally, we find for all clauses C and formulas

F that C ∨ ≡ ∨ C ≡ , C ∨ ⊥ ≡ ⊥ ∨ C ≡ C, F ∧ ≡ ∧ F ≡ F , and F ∧ ⊥ ≡ ⊥ ∧ F ≡ ⊥.

Let

C i | 1 ≤ i ≤ n) such that C 1 = C, C n = D and C i is a resolvent of the clause C i−1 and

some clause in the formula F for all i ∈ {2, . . . , n − 1}; one should observe that F entails D and that the addition of entailed clauses to a formula preserves equivalence.

Variable Assignments and the Reduct Operator

Let J be a finite sequence of literals. In J each literal may be marked as a decision literal by placing a dot on top like in ẋ; if a literal x is not marked, then it is a propagation literal. Let J be a sequence of literals of length n. We say that literal x ∈ J iff there is a k ∈ {1, . . . , n} such that x = x k . Let J 1 = (x 1 , . . . , x n ) and J 2 = (y 1 , . . . , y m ) be two sequences of literals; their concatenation J 1 J 2 is the sequence (x 1 , . . . , x n , y 1 , . . . , y m ). If a finite sequence J of literals does not contain a complementary pair of literals, then J represents an interpretation. As this condition is always met in this paper, we identify sequences of literals with interpretations whenever appropriate.

The reduct of a formula F w.r.t. an interpretation J, in symbols F | J , is defined as F | J := {C| J | C ∈ F and for every literal x ∈ C we find that x ∈ J}, where C| J = C \ {x | x ∈ J}. Intuitively, the reduct operator expresses the state of a SAT solver, where the formula F is the working formula and J is the working assignment. For instance, let F = {{x, y}, {z}}, then F | x = {{y}, {z}}, F | z = {{x, y}, ⊥} and F | y z = , where the interpretations are written as sequences of literals. One should observe that the reduct operator does not distinguish between propagation and decision literals.

Lemma 1 below summarizes the properties of the reduct operator: (i) The reduct is monotone. (ii) A formula F is satisfiable iff there exists an interpretation J such that the reduct of a formula w.r.t. J is the empty formula. (iii) If the reduct of a formula F w.r.t. the interpretation {x} is unsatisfiable, and the formula F entails the literal x, then the formula F is unsatisfiable. (iv) The reduct operator is a semantic operator in the sense that it cannot distinguish equivalent formulas.

Lemma 1 (Reduct Operator). Let F, F be formulas and x a literal.

(i) F | J ⊆ (F ∪ F )| J for every interpretation J.

(ii) F is satisfiable iff there exists a J such that

F | J = . (iii) If F | x is unsatisfiable and F |= x, then F is unsatisfiable. (iv) If F ≡ F , then F | J ≡ F | J for every interpretation J.

Proof. See [19, pp.10-12].

Generic CDCL

Modern SAT solvers are based on the linearized DPLL [5] algorithm and consists of the following components: termination criteria, a decision component that picks the branching literals, an inference component that adds propagation literals to the working sequence of literals, a backtracking component that rolls back wrong decisions and a formula management component that simplifies the working formula. We maintain two data structures during the execution of modern SAT solvers: the working formula, and the working set of literals. Together they define the state. The components are modelled as a transition relation over the set of states; the union of the rules in Fig. 1 is then the transition relation SAT-rule:

F J SAT SAT iff F | J = .

UNSAT-rule: F J UNSAT UNSAT iff ⊥ ∈ F | J and J contains only propagation literals.

DEC-rule:

F J DEC F J ẋ iff x ∈ vars(F ) ∪ vars(F ) and {x, x} ∩ J = ∅.

INF-rule:

F J INF F J x iff F | J ≡sat F | J x and {x, x} ∩ J = ∅.

LEARN-rule:

F J LEARN F ∪ {C} J iff F |= C.

FORGET-rule:

F J FORGET F \ {C} J iff F \ {C} |= C.

BACK-rule:

F J J BACK F J. INP-rule: F ε INP F ε iff F ≡sat F .

Fig. 1: Transition relations of Generic CDCL. These relations apply to all formulas F and F , clauses C, literals x and lists of literals J and J . ε denotes the empty sequence of literals.

of Generic CDCL: Formally, we model the computation of modern SAT solvers by means of state transition systems as follows:

Definition 2 (Generic CDCL). Generic CDCL is a state transition system whose sets of states is {F J | F is a formula and J is a sequence of literals} ∪ {SAT, UNSAT}, whose initial state for the input formula F is init(F ) = F ε, whose set of terminal states is {SAT, UNSAT}, and whose transition relation is defined as:

:= { SAT , UNSAT , DEC , INF , LEARN , FORGET , BACK , INP }.

The SAT-rule terminates the computation with the output SAT, if the reduct of the working formula w.r.t. the working set of literals is the empty formula. This condition can be decided in linear time w.r.t. the size of the working formula F . By Lemma 1 (ii) the working formula is then satisfiable.

The UNSAT-rule terminates the computation with the output UNSAT, if no model of the working formula exists. This is the case when a conflict occurs in the top level, i.e. ⊥ ∈ F | J and the sequence J of literals contains only propagation literals. These conditions can be decided in polynomial time.

The DEC-rule extends the working sequence of literals by an unassigned literal ẋ as a decision literal.

The INF-rule extends the working list of literals by a propagation literal x, if the reducts of the working formula w.r.t. the working sequence of literals and its extension are equisatisfiable.

The BACK-rule models backtracking, as well as backjumping and restarts, by deleting outermost right literals in the working sequence of literals.

The LEARN-rule adds a clause C to the working formula, if it is entailed by the working formula F . Deciding whether F |= C holds, is coNP-complete.

Similarly to the INF-rule, SAT solvers avoid this check by using techniques for creating the clause C that ensure this property, as for example resolution.

The FORGET-rule deletes a clause C of the working formula

F , if F \ {C} |= C.

The question whether F \ {C} |= C holds is coNP-complete. Typically, we use tractable algorithms to identify redundant clauses. For instance, clauses that were introduced by the LEARN-rule but have turned out to be useless and did not participate in the elimination of other clauses in the formula can be removed.

For more details on the deletion of clauses see [12].

The INP-rule models formula simplifications that are used in pre-and inprocessing. It replaces the working formula with an equisatisfiable formula when the working sequence of literals is empty.

Let * be the reflexive and transitive closure of . Let x 0 x for all states x, and x n z for all natural numbers n ∈ N if and only if there exists a state y such that x n−1 y z. In the next subsection we investigate the question whether Generic CDCL correctly solves the SAT problem. Formally, we define Generic CDCL to be sound iff for all formulas F 0 we have that init(F 0 )

* SAT implies that F 0 is satisfiable and init(F 0 ) * UNSAT implies that F 0 is unsatisfiable.

Generic CDCL is Sound

Before proceeding to the soundness proof of Generic CDCL, it will be necessary to study two invariants of Generic CDCL that are presented in the proposition below: (i) states that the rules of Generic CDCL do not change the satisfiability of the working formula, and (ii) states that whenever the working sequence of literals is of the form J 1 x J 2 , where x is a propagation literal, the reducts of the working formula w.r.t. J 1 and J 1 x are equisatisfiable.

Proposition 3 (Invariants). Let F 0 , F be formulas, J be a sequence of literals, and

n ∈ N. If init(F 0 ) n F J, then 1. F 0 ≡ sat F , and 2. F | J1 ≡ sat F | J1 x

, for all sequences of literals J 1 , J 2 and propagation literals x with J = J 1 x J 2 .

Proof. The claims are proven by induction on n. For the base case n = 0, 1. follows from F 0 = F and 2. holds since the J is empty. For the induction step, assume that the claim holds for the state F J and suppose that F J R F J where R ∈ {DEC, INF, LEARN, FORGET, BACK, INP}: ẋ with {x, x} ∩ J = ∅. 1. follows since F 0 ≡ sat F holds by induction. 2. holds because the appended literal is a decision literal. Formally, let J 1 , J 2 be literal sequences, y be a propagation literal such that J = J 1 y J 2 ẋ. By induction, we conclude that

F | J 1 ≡ sat F | J 1 y . Hence, F | J 1 ≡ sat F | J1 y .

-BACK-rule: In this case, F = F and J = J J . 1. follows since F 0 ≡ sat F by induction. 2. holds because the literal sequence J is a prefix of J. Formally, let J 1 , J 2 be literal sequences and y be a propagation literal such that J = J 1 y J 2 . By induction, we conclude that

F | J 1 ≡ sat F | J 1 y

, and consequently we know that

F | J 1 ≡ sat F | J 1 y .

-LEARN-rule: In this case, F = F ∪ {C} where F |= C and J = J. 1. follows since F ≡ F and the addition of the entailed clause C preserves equivalence of the working formula. 2. follows from the reduct operator being a semantic operator by Lemma 1.iv and therefore F | J 1 ≡ sat F | J 1 y holds by induction for every literal sequences J 1 , J 2 and propagation literals y with J = J 1 y J 2 .

-FORGET-rule: This case can be treated as in the LEARN-rule.

-INF-rule: In this case, F = F and J = J x for some propagation literal x with {x, x} ∩ J = ∅. 1. follows since F 0 ≡ sat F holds by induction. 2. follows from the definition of the INF-rule: Consider the literal sequences J 1 , J 2 and a propagation literal y such that J = J 1 y J 2 . In the case that y = x, we know that J 2 is the empty sequence of literals and consequently F | J 1 ≡ sat F | J 1 y holds by the definition of the INF-rule. In the case of y = x, we can conclude the claim by induction.

-INP-rule: In this case, F ≡ sat F and J is the empty sequence. Consequently, 1. holds by the definition of the INP-rule, and 2. is satisfied as J = ε.

We can now show the main theorem in this paper.

Theorem 4 (Soundness). Generic CDCL is sound.

Proof. We divide the proof in two parts, first proving that the output SAT is correct, and then proving that the output UNSAT is correct. Let F 0 , F be formulas, J be a sequence of literals and suppose that init(F 0 ) * F J SAT(UNSAT, resp.).

SAT By the definition of the SAT-rule, we know that F | J = . By Lemma 1.ii, we know that the formula F is satisfiable. From the result that the formula F is satisfiable together with the property that the formulas F 0 and F are equisatisfiable given in Prop. 3(1.), we conclude that the input formula F 0 is satisfiable.

UNSAT By the definition of the UNSAT-rule, we know that ⊥ ∈ F | J and the working sequence of literals J = (x 1 . . . x n ) contains only propagation literals. Since a conflict occurs, F | J is unsatisfiable. From the result that the formula F | J is unsatisfiable and the literal sequence J contains only propagation literals we can repeatably apply Prop. 3(2.) and we obtain that the formula F is unsatisfiable. Since the formula F is unsatisfiable and the formulas F and F 0 are equisatisfiable by Prop. 3(1.), we conclude that F 0 is unsatisfiable.

Generic CDCL Subsumes Important SAT Solving Techniques

We now describe some important SAT solving techniques, and demonstrate that Generic CDCL can adequately model these techniques.

Subsumption

For a formula F , the clause C ∈ F subsumes the clause D ∈ F iff C ⊂ D. In this case, D can be deleted because F \ {D} |= D. Consequently, F J FORGET F \{D} J holds for every literal sequence J. Removing subsumed clauses is done as a preprocessing step in SAT solvers and during clause learning.

Tautologies A clause C is a tautology if it contains a complementary pair of literals. Every formula F entails a tautology and the LEARN-rule in Generic CDCL subsumes this techniques. Tautologies are eliminated during preprocessing.

Conflict-Directed Backtracking and Learning [21] is an improvement of naive backtracking that takes the reason of the conflict into account. Consider the state F J ẋ J and a clause C ∈ F where C| J ẋ J = ⊥. The clause C is the conflict clause. If there is a linear resolution derivation from the conflict clause C to a clause D in the formula F such that D| J is the unit clause y, the technique rewrites the state F J ẋ J into the state F ∪ {C} J y. Conflict-directed backtracking and learning can be simulated by the following transition steps:

F J ẋ J BACK F J LEARN F ∪ {D} J INF F ∪ {D} J y.

Blocked Clause Elimination [11]

A clause C is blocked in the formula F if it contains a literal x such that all resolvents of the clause C and clauses D ∈ F upon x are tautological. Blocked clauses are removed from a formula during preand inprocessing. If C is blocked in F , then F ≡ sat F \ {C} and, therefore, the INP-rule subsumes the blocked clause elimination technique.

Unit Propagation A clause that contains a single literal is a unit clause. Unit propagation adds the propagation literal x to the literal sequence J, whenever the reduct of the working formula w.r.t. J contains the unit clause (x). Since F | J |= x, we know that F | J ≡ sat F | J x and consequently the INF-rule subsumes unit resolution.

Pure Literal

A literal x is pure in the formula F , if x ∈ lits(F ). For pure literals, it holds that F ≡ sat F | x and, therefore, whenever a literal x is pure in the formula F | J for some literal sequence J, Generic CDCL can add the pure literal to the working literal sequence: F J INF F J x.

Related Work

Several attempts have been made to formalize sequential SAT solvers in terms of transition systems or proofs calculi: Abstract DPLL [18], Linearized DPLL [1], and Rule-based SAT solver description [15]. In general, these formalization are based on a notion of state like Generic CDCL.

However, these formalizations cannot adequately model recent SAT solvers: For instance, Linearized DPLL does not model the SAT solver MiniSAT, because Linearized DPLL restricts decision literals to occur in the working formula, but the solver MiniSAT can also select the complements of such literals. Additionally, Linearized DPLL does not model formula simplification techniques such as blocked clause elimination, or probing-based inference techniques. Similarly, Abstract DPLL and the Rule-based SAT solver description [15] do not model formula simplifications that changes the semantics of formulas like blocked clause elimination. Maric highlighted the implementation of clause learning techniques in his Rule-based SAT solver description [15], but it does not include recent developments such as clause strengthening. All these formalizations consider DPLLbased SAT solvers, but the ancient pure literal rule is not subsumed in these systems. In contrast, Generic CDCL subsumes all recent SAT techniques to the best of our knowledge.

In [12] Jarvisalo et. al. developed a formal system to model clause learning, forgetting and formula simplification techniques to understand the side-effects of the combination of different rules. They drew our attention to the interplay of the learned clause database with inprocessing techniques. The interplay of clause sharing and formula simplification techniques in parallel SAT solvers was analyzed in [14], where the state of a sequential SAT solver was modelled just as the working formula. We believe that Generic CDCL is an important fragment to understand sequential SAT solvers with inprocessing and their cooperation in the parallel-portfolio setting with clause sharing.

Conclusion

The propositional satisfiability problem is of great practical interest and can be efficiently answered by modern SAT solvers like Riss, Lingeling or MiniSAT. Today, modern SAT solvers are highly tuned proof procedures with many advaned techniques. Therefore, it is desireable to investigate SAT solving techniques in combination with each other and to abstract from implementations.

In this paper, we developed Generic CDCL, a formalism that models the computation of modern SAT solvers in terms of a state transition system, where each transition rule abstracts a component in a SAT solver. In particular, the transition rules INF and INP model formula simplification techniques like blocked clause elimination and inference techniques such as the pure literal rule. We have examined invariants in Generic CDCL and have shown that Generic CDCL is sound. In contrast to previous work on formalizations of SAT solvers, we can model all recent techniques. The findings add to our understanding of the interplay of inprocessing techniques with the other components of SAT solvers.

A limitation of Generic CDCL is its lack of details in the learning and inference component. As future work, we plan to investigate properties such as completeness, confluence and termination.