What we can learn from conflicts in propositional satisfiability

Abstract

Learning is a general concept, playing an important role in many Artificial intelligence domains. In this paper, we address the learning paradigm used to explain failures or conflicts encountered during search. This explanation, derived by conflict analysis, and generally expressed as a new constraint, is usually used to dynamically avoid future occurrences of similar situations. Before focusing on clause learning in Boolean satisfiability (SAT), we first overview some important works on this powerful reasoning tool in other domains such as constraint satisfaction and truth maintenance systems. Then, we present a comprehensive survey of the most important works having led to what is called today—conflict driven clause learning—which is one of the key components of modern SAT solvers. We also overview some of the original extensions or variants of clauses learning. In theory, current SAT solvers with clause learning are as powerful as general resolution proof systems. In practice, real-world SAT instances with millions of variables and clauses are now in the scope of this solving paradigm.

1 Introduction

The SAT problem, i.e., the problem of checking whether a Boolean formula in conjunctive normal form (CNF) is satisfiable or not, is central to many domains in computer science and artificial intelligence including constraint satisfaction problems (CSP), automated planning, non-monotonic reasoning, VLSI correctness checking, etc. Today, SAT has gained a considerable audience with the advent of a new generation of solvers able to solve large instances encoding real-world problems, and the demonstration that these solvers represent important low-level building blocks for many important fields, e.g., SAT modulo theory, Theorem proving, Model checking, Quantified boolean formulas, Maximum Satisfiability, Pseudo boolean, etc. These solvers, often called modern SAT solvers (Moskewicz et al. 2001; Eén and Sörensson 2003), are based on the classical DPLL procedure (Davis et al. 1962) enhanced with: (1) an efficient implementation of unit propagation through incremental and lazy data structures, (2) restart policies (Gomes et al. 1998; Kautz et al. 2002), (3) activity-based variable selection heuristics (VSIDS-like) (Moskewicz et al. 2001), and (4) clause learning (Marques Silva and Sakallah 1996; Moskewicz et al. 2001). Clause learning is now recognized as one of the most important component of Modern SAT solvers. The main idea is that when a current branch of the search tree leads to a conflict, clause learning aims to derive a clause that succinctly expresses the causes of the conflict. Such learned clause is then used to prune the search space. Clause learning also known in the literature as conflict driven clause learning (CDCL) refers now to the most known and used First UIP learning scheme, first integrated in the SAT solver Grasp (Marques Silva and Sakallah 1996) and efficiently implemented in zChaff Moskewicz et al. (2001). Most of the SAT solvers, integrate this strong learning scheme. Theoretically, by integrating clause learning to DPLL-like procedures Davis et al. (1962), the obtained SAT solver formulated as a proof system is as powerful as general resolution (Pipatsrisawat and Darwiche 2009, 2010).

This paper deals with learning from conflict, one of the most important component of modern SAT solvers. It surveys most of the works that led to the current well known First UIP learning scheme integrated in all the state-of-the-art SAT solvers. We also present some original extensions and variants of this classical learning scheme. To get a complete picture about SAT solvers, we additionally overview the other components mentioned above.

Our goal in this survey paper is to popularize this important paradigm to the operation research community, while hoping its possible integration to enhance the efficiency of branch and bound based algorithm. SAT have strong connection with operation research. Indeed, it is directly related to 0–1 integer linear programming or pseudo boolean constraints. A linear transformation for encoding as Boolean formulas in conjunctive normal form, 0/1 linear inequalities with integral coefficients was given by Warners (1998), while a clause can be seen as a simple 0/1 linear inequality. Consequently, a CNF formula can be formulated as a system of 0/1 linear inequalities and vice versa. On the solving side, branch and bound and DPLL-like procedure both develop a search tree based on the separation principle. Interestingly enough, the well known resolution principle and cutting plane rule are heavily related.

The paper is an updated version of Hamadi et al. (2012). It is organized as follows. After some preliminary definitions and notations, relationships between SAT and integer linear programming are discussed in Sect. 3. In Sect. 4, a comprehensive overview of related AI learning based approaches are briefly discussed. A survey of clauses learning based techniques are described in Sect. 5. The other components of modern SAT solvers are described before concluding.

2 Preliminary definitions and notations

A Boolean formula $\mathcal{F}$ in Conjunctive Normal Form (CNF) is a conjunction of clauses, where a clause is a disjunction of literals. A literal is a positive (x) or negated ($\lnot {x}$) propositional variable. The two literals x and $\lnot {x}$ are called complementary. We denote by $\overline{l}$ the complementary literal of l. More precisely, if $l = x$ then $\overline{l}$ is $\lnot x$ and if $l = \lnot x$ then $\overline{l}$ is x. For a set of literals L, $\overline{L}$ is defined as $\{\overline{l} ~|~ l \in L\}$. Let us recall that any Boolean formula can be translated to CNF using linear Tseitin encoding (Tseitin 1968). A unit clause is a clause containing only one literal (called unit literal), while a binary clause contains exactly two literals. An empty clause, denoted $\perp$, is interpreted as false (unsatisfiable), whereas an empty CNF formula, denoted $\top$, is interpreted as true (satisfiable).

The set of variables occurring in $\mathcal{F}$ is denoted $V_ \mathcal{F}$. A set of literals is complete if it contains one literal for each variable in $V_\mathcal{F}$, and fundamental if it does not contain complementary literals. An interpretation $\rho$ of a Boolean formula $\mathcal{F}$ is a function which associates a value $\rho (x)$ to some of the variables $x \in V_ \mathcal{F}$. $\rho$ is complete if it assigns a value to every $x \in V_ \mathcal{F}$, and partial otherwise. An interpretation is alternatively represented by a complete and fundamental set of literals. A model of a formula $\mathcal{F}$ is an interpretation $\rho$ that satisfies the formula; denoted $\rho \models \mathcal F$.

The following notations will be heavily used throughout the paper:

• $\eta [x, c_i, c_j]$ denotes the resolvent between a clause $c_i$ containing the literal x and $c_j$ a clause containing the opposite literal $\lnot {x}$. In other words $\eta [x, c_i, c_j] = c_i\cup c_j\backslash \{x, \lnot {x}\}$. A resolvent is called tautological when it contains complementary literals.

• $\mathcal{F}|_x$ denotes the formula obtained from $\mathcal{F}$ by assigning x the truth-value true. Formally $\mathcal{F}|_x = \{c ~|~ c\in \mathcal{F}, \{x, \lnot {x}\} \cap c = \emptyset \} \cup \{c\backslash \{\lnot {x}\} ~|~ c\in \mathcal{F}, \lnot {x}\in c\}$ (that is: the clauses containing x are therefore satisfied and removed; and those containing $\lnot {x}$ are simplified). This notation is extended to interpretations: given an interpretation $\rho =\{x_1,\dots , x_n\}$, we define $\mathcal{F}|_\rho = (\dots ((\mathcal{F}|_{x_1})|_{x_2})\dots |_{x_n})$.

• $\mathcal{F}^*$ denotes the formula $\mathcal{F}$ closed under unit propagation, defined recursively as follows: (1) $\mathcal{F}^* = \mathcal{F}$ if $\mathcal{F}$ does not contain any unit clause, (2) $\mathcal{F}^* =\,\perp$ if $\mathcal{F}$ contains two unit-clauses $\{x\}$ and $\{\lnot {x}\}$, (3) otherwise, $\mathcal{F}^*= (\mathcal{F}|_{x})^*$ where x is the literal appearing in a unit clause of $\mathcal{F}$.

• $\models _*$ denotes deduction by unit propagation: $\mathcal{F}\models _{*} x$ means that a literal x is deduced by unit propagation from $\mathcal F$, i.e. $x \in \mathcal{F}^*$. We write $\mathcal{F}\models _{*} \perp$ if the formula is proved inconsistent by unit propagation. In particular, note that if we have a clause c such that $\mathcal{F}\wedge \overline{c} \models _* \perp$, then c is a consequence of $\mathcal F$. We say that c is deduced by unit propagation.

• Let $c_1$ and $c_2$ be two clauses of a formula $\mathcal{F}$. We say that $c_1$ (respectively $c_2$) subsume (respectively is subsumed) $c_2$ (respectively by $c_1$) iff $c_1 \subseteq c_2$. If $c_1$ subsume $c_2$, then $c_1 \models c_2$ (the converse is not true). Also $\mathcal{F}$ and $\mathcal{F} -{c_2}$ are equivalent with respect to satisfiability.

Let us now introduce some notations and terminology on SAT solvers based on the Davis Logemann Loveland procedure, commonly called DPLL (Davis et al. 1962). DPLL is a backtrack search procedure; at each node the assigned literals (decision literal and the propagated ones) are labeled with the same decision level starting from 1 and increased at each branching. The current decision level is the highest decision level in the assignment stack. After backtracking, some variables are unassigned, and the current decision level is decreased accordingly. At level i, the current partial assignment $\rho$ can be represented as a sequence of decision-propagation of the form $\langle ( x_k^i),x_{k_1}^i, x_{k_2}^i,\dots , x_{k_{n_k}}^i \rangle$ where the first literal $x_k^i$ corresponds to the decision literal $x_k$ assigned at level k and each $x_{k_j}^i$ for $1\le j\le n_k$ represents propagated (unit) literals at level k. Such a partial interpretation (sequence of decisions-propagations) associated to a given node of the search tree is called partial ordered interpretation.

Let $x\in \rho$, we denote by l(x) the assignment level of x, $d(\rho , i) = x$ if x is the decision literal assigned at level i. For a given level i, we define $\rho ^i$ as the projection of $\rho$ to literals assigned at a level $\le i$.

3 SAT and integer programming formulation

In this section, we briefly recall some connections between SAT and integer programming. Our goal is to convince the reader about the proximity of these two research domains and that cross-fertilization even if it has been widely investigated in the past remains an important and interesting research issue.

Let us identify Boolean values false and true with integers 0 and 1. Any CNF formula can be reformulated as a system of 0/1 linear inequalities. The following example illustrates such reformulation.

Example 1

Let $\mathcal{F}$ be a CNF formula made of the two clauses $c_1 = (x_1\vee x_2\vee \lnot x_3)$ and $c_2= (x_1\vee \lnot x_2)$. $\mathcal{F}$ can be reformulated as a system $S_\mathcal{F}$ of 0/1 linear inequalities:

$\mathcal{F}$ is satisfiable if and only if $S_\mathcal{F}$ have a feasible solution as determined by integer programming.

3.1 Branch-and-bound and DPLL

The most popular solution approach for linear 0/1 programming is branch and bound. It is very similar to the DPLL procedure, which also generates an enumeration tree by branching search. They differ mainly in that branch-and-bound solves the linear relaxation of the satisfiability problem (obtained by replacing the condition $x_i\in \{0,1\}$ with ranges $0\le x_i\le 1$) at each node of the enumeration tree whereas DPLL applies unit-propagation. There are several enhancements of this basic algorithm including branch-and-cut algorithm by Hooker and Fedjiki (1990) that uses cutting planes at several nodes of the branch-and-bound tree. For a survey on mathematical programming approaches for solving the satisfiability problem, see Chandru and Hooker (1999) and Hooker (2000).

3.2 Resolution and cutting planes

As mentioned previously, a modern SAT solver formulated as a proof system is equivalent to general resolution (Pipatsrisawat and Darwiche 2009). Resolution (Quine 1955; Robinson 1965) is a well known satisfiability procedure, that recursively applies the resolution rule (see Sect. 2) on two selected clauses containing two complementary literals and adding the obtained resolvents to the formula. This simple technique is complete for refutation. If the CNF formula is unsatisfiable, the resolution procedure is able to generate an empty clause in a finite but exponential number of steps in general. Applying subsumption at each step of the resolution procedure leads to a complete approach for satisfiability checking. In spite of its exponential worst case time and spatial complexity, resolution plays an important role in current SAT solvers. As we can see later, conflict driven clause learning is based on a restricted form of resolution.

In integer programming, resolution corresponds to cutting planes (Hooker and Fedjiki 1990). A cutting plane is an inequality verified by all the 0/1 solutions of the problem. As we can see in the following example, a cutting plane can be generated by taking a nonnegative linear combination of the inequalities in the linear relaxation, including the bounds $0\le x_i\le 1$, and to round up any fractions that result in the coefficient or right hand side. Such a cut is called a rank one cut.

Example 2

Let us take again the formula $\mathcal{F}$ given in the Example 1 and its corresponding set of inequalities $S_\mathcal{F}$.

$$\begin{aligned} \begin{array}{rlrlr} &{} x_1 + &{} x_2 + &{} (1-x_3)&{} \ge 1 \left( \frac{1}{2}\right) \\ &{} x_1 + &{}(1-x_2) &{} &{}\ge 1 \left( \frac{1}{2}\right) \\ &{} &{} &{} (1-x_3) &{}\ge 0 \left( \frac{1}{2}\right) \\ \hline &{} x_1 + &{} &{} (1 - x_3)\ge \frac{1}{2} &{}\\ \end{array} \end{aligned}$$

We recall that applying the resolution rule on the clauses $c_1$ and $c_2$ leads to the resolvent $\eta [x_2, c_1, c_2] = (x_1\vee \lnot x_3)$. This resolvent corresponds to the rank one cutting plane $x_1 + (1 - x_3)\ge \frac{1}{2}$ which is equivalent to $x_1 + (1 - x_3)\,\ge 1$ obtained by rounding up the right hand side. This resolvent is generated by combining the linear inequalities $s_{c_1}$, $s_{c_2}$ with the bound $(1-x_3)\ge 0$ where the two sides of each inequality is multiplied by $\frac{1}{2}$.

Further connexion between resolution and cutting planes can be found in Hooker and Fedjiki (1990) and Hooker (1989).

4 An historical overview of learning based approaches

Learning from conflicts appeared first in the context of constraint satisfaction problem solving (Stallman and Sussman 1977; Gasching 1979). Such approaches usually refer to non-chronological backtracking and nogood recording. A backtrack-style procedure performs a depth-first search, successively instantiating variables of the constraint network to values in order to build a solution, and backtracks when necessary, in order to escape from a conflict. In general, the current branch of the search tree might contain many irrelevant variables between the level of conflict and its real cause. Chronological backtracking may lead the solver to trashing by rediscovering the same conflict over and over again in different settings of irrelevant variables. One has to decide how far to backtrack and potentially, what to learn from the conflict. In 1977, Stallman and Sussman (1977) proposed a rule-based system for computer-aided circuit analysis. The system threads deduced facts with justifications which mention the antecedent facts and the rule used. To reduce the search space, these justifications are exploited by the system during the conflict analysis to reduce the search space. This leads to an effective control of combinatorial search which is called dependency-directed backtracking. This method is used in truth maintenance systems (Doyle 1979; McAllester 1980), and has been improved or simplified in the context of logic programming and constraint satisfaction problems by various researchers (Bruynooghe 1981; Dechter 1986, 1990).

As the learnt clauses database is of exponential size, several strategies have been proposed to reduce such spatial complexity. Most of them try to avoid such major drawback by either introducing limited and (1) relevant based learning scheme or by achieving only (2) non-chronological backtracking (without nogood recording) referred as intelligent backtracking. For example, relevance-bounded learning (Bayardo and Miranker 1996) and conflict directed backjumping (CBJ) (Prosser 1993) belong respectively to the first and the second category. We can also cite other approaches that reduce space complexity by introducing bounds on the size of the constraints recorded (Dechter 1990; Frost and Dechter 1994), and those that record constraints of arbitrary size, but delete nogoods which become irrelevant to the current portion of the search space (Ginsberg 1993).

The efficiency of clause learning currently integrated in all the state-of-the-art SAT solvers is made possible thanks to strong learning schemes, lazy data structures and constraint database management strategies. Among these chronologically ordered contributions, we can cite the important works by Marques Silva and Sakallah (1996), Bayardo and Schrag (1997), Zhang (1997), Moskewicz et al. (2001) and Zhang et al. (2001).

5 Classical clause learning: a formal description

Clause learning plays a critical role in the success of modern complete SAT solvers. The main idea is that when a current branch leads to a conflict, clause learning aims to derive a clause that succinctly expresses the causes of conflict. Such learned clause is then used to prune the search space. Clause learning also known in the literature as conflict driven clause learning (CDCL) refers now to the most known and used First UIP learning scheme, first integrated in the SAT solver Grasp (Marques Silva and Sakallah 1996) and efficiently implemented in zChaff Moskewicz et al. (2001). Most of the SAT solvers, usually called modern SAT solvers, integrate this strong learning scheme. Theoretically, by integrating clause learning to DPLL-like procedures (Davis et al. 1962), the obtained SAT solver formulated as a proof system is as powerful as general resolution (Pipatsrisawat and Darwiche 2009). Several works have been conducted in order to improve this simple learning scheme. Such improvements, include the minimization process introduced by Sörensson and Biere (2009) and Hamadi et al. (2009a) to reduce the size of the learnt clauses, the extended learning schemes proposed in Audemard et al. (2008a) and other clauses learning variants (Pipatsrisawat and Darwiche 2008; Sabharwal et al. 2012; Hamadi et al. 2009a; Jabbour 2009).

Prior to the formal description of the above classical clause learning scheme, we first formalize the graph-based framework used to learn conflict clauses.

An implication graph (Marques Silva and Sakallah 1996) is a representation which captures the variable assignments $\rho$ (interpretation) made during the search, both by branching and by propagation. This representation is a convenient way to analyse conflicts. In classical SAT solvers, whenever a literal y is propagated, we keep a reference to the clause at the origin of the propagation of y, which we denote $\overrightarrow{imp}(y)$. The clause $\overrightarrow{imp}(y)$ is in this case of the form $(x_1 \vee \dots \vee x_n \vee y)$ where every literal $x_i$ is false under the current partial interpretation ($\rho (x_i) = {{\textit{false}}}, \forall i \in 1..n$), while $\rho (y) = {{\textit{true}}}$. When a literal y is not obtained by propagation but comes from a decision, $\overrightarrow{imp}(y)$ is undefined, which we denote for convenience $\overrightarrow{imp}(y) = \,\perp$.

When $\overrightarrow{imp}(y) \not = \perp$, we denote by exp(y) the set $\{\overline{x} ~|~ x \in \overrightarrow{imp}(y)\setminus \{y\}\}$, called set of explanations of y. In other words if $\overrightarrow{imp}(y) = (x_1 \vee \dots \vee x_n \vee y)$, then the explanations are the literals $\overline{x_i}$ with which $\overrightarrow{imp}(y)$ becomes the unit clause (y). Note that for all i we have $l(\overline{x_i}) \le l(y)$, i.e., all the explanations of the deduction come from a level at most as high. When $\overrightarrow{imp}(y)$ is undefined we define exp(y) as the empty set. In an implication graph, the set of predecessors of a node corresponds to the set of explanations of the corresponding literal:

Definition 1

(Implication Graph) Let $\mathcal{F}$ be a CNF formula, $\rho$ a partial ordered interpretation, and let exp denotes the set of explanations for the unit propagated literals in $\rho$. The implication graph associated to $\mathcal{F}$, $\rho$ and exp is $\mathcal{G}^{(\rho , exp)}_\mathcal{F}=(\mathcal{N},\mathcal{E})$ where:

• $\mathcal{N} = \rho$, i.e. there is exactly one node for every literal, decision or implied;

• $\mathcal{E} = \{(x, y) ~|~ x \in \rho , y \in \rho , x \in \textit{exp}(y)\}$

For simplicity reason, we denote $\mathcal{G}^{(\rho , exp)}_\mathcal{F}$ simply as $\mathcal{G}^{\rho }_\mathcal{F}$ in the rest of this paper.

Example 3

$\mathcal{G}^\rho _\mathcal{F}$, shown in Fig. 1 is an implication graph for the formula $\mathcal{F}$ and the partial assignment $\rho$ given below : $\mathcal{F} \supseteq \{c_1,\dots ,c_{10}\}$

$$\begin{aligned} \begin{array}{rlrlrl} (c_1) &{} \lnot {x}_2 \vee \lnot {x}_{5} \vee x_{6} ~~&{} (c_2) &{} \lnot {x}_{5} \vee x_{7} ~~\\ (c_3) &{} \lnot {x}_{6} \vee \lnot {x}_{7} \vee x_{8} ~~&{} (c_4) &{} \lnot {x}_{3} \vee \lnot {x}_{8} \vee x_{9} ~~\\ (c_5) &{} \lnot {x}_{1} \vee \lnot {x}_{8} \vee x_{10} ~~ &{} (c_6) &{} \lnot {x}_{4} \vee \lnot {x}_{9} \vee x_{11}\\ (c_7) &{} \lnot {x}_{4} \vee \lnot {x}_{9} \vee \lnot {x}_{10} \vee x_{12} ~~&{} (c_8) &{} \lnot {x}_{10} \vee x_{13} ~~\\ (c_9) &{} \lnot {x}_{11} \vee \lnot {x}_{12} \vee x_{14} ~~ &{} (c_{10}) &{} \lnot {x}_{13} \vee \lnot {x}_{14} ~~\\ \end{array} \end{aligned}$$

$\rho =\{\langle \lnot {x}_1^1\dots \rangle \langle (x_2^2)\dots x_{3}^2\dots \rangle \langle (x_4^3)\dots \rangle \dots \langle (x_{5}^5)\dots \rangle \}$. The current decision level is 5.

Fig. 1

Implication Graph $\mathcal{G}_\mathcal{F}^\rho = (\mathcal{N},\mathcal{E})$

5.1 Generating asserting clauses

In this section, we formally describe the classical learning schemes used in modern SAT solvers. In the following definitions, we consider $\mathcal{F}$ a CNF formula, $\rho$ a partial assignment such that $(\mathcal{F}| _{\rho })*=\bot$ and $\mathcal{G}_\mathcal{F}^{\rho }= (\mathcal{N},\mathcal{E})$ the associated implication graph. Assume that the current decision level is m. As a conflict is reached, then $\exists x\in$ st. $\{x,\lnot {x}\}\subset \mathcal{N}$ and $l(x) = m$ or $l(\lnot {x})=m$. Conflict analysis is based on applying resolution from the top to the bottom of the implication graph using the different clauses of the form $(\overline{exp(y)}\vee y)$ implicitly encoded at each node $y\in \mathcal{N}$. We call this process an asserting clause derivation. Let us now formally define the concept of asserting clause, asserting clause derivation and unique implication point.

Definition 2

(Asserting clause) A conflict clause c of the form $(\alpha \vee x)$ is called an asserting clause iff $\rho (c)={{\textit{false}}}$, $l(x) = m$ and $\forall y\in \alpha , l(y)<l(x)$. x is called asserting literal, which we denote in short $\mathcal{A}(c)$.

We define $jump(c) = max\{l(\lnot {y}) ~|~ y\in \alpha \}$.

Definition 3

(Asserting clause derivation) An asserting clause derivation $\pi (\sigma _k)$ is a sequence of clauses $\langle \sigma _1,\sigma _2,\dots \sigma _k\rangle$ satisfying the following conditions :

• 1. $\sigma _1 = \eta [x, \overrightarrow{imp}(x), \overrightarrow{imp}(\lnot {x})]$, where $\{x, \lnot {x}\}$ is the conflict.

• 2. $\sigma _i$, for $i \in 2..k$, is built by selecting a literal $y \in \sigma _{i-1}$ for which $\overrightarrow{imp}(\overline{y})$ is defined. We then have $y \in \sigma _{i-1}$ and $\overline{y} \in \overrightarrow{imp}(\overline{y})$: the two clauses resolve. The clause $\sigma _i$ is defined as $\eta [y, \sigma _{i-1}, \overrightarrow{imp}(\overline{y})]$;

• 3. $\sigma _k$ is, moreover an asserting clause.

Note that every $\sigma _i$ is a resolvent of the formula $\mathcal F$: by induction, $\sigma _1$ is the resolvent between two clauses that directly belong to $\mathcal F$; for every $i>1$, $\sigma _i$ is a resolvent between $\sigma _{i-1}$ (which, by induction hypothesis, is a resolvent) and a clause of $\mathcal F$. Every $\sigma _i$ is therefore also an implicate of $\mathcal F$, that is: $\mathcal{F} \models \sigma _i$.

Another important remark is that in modern SAT solvers, the literals y used in the condition 2 of Definition 3 are restricted to those of the current decision level.

Definition 4

(Elementary asserting clause derivation ) An asserting clause derivation $\pi (\sigma _k)$ $= \langle \sigma _1,\sigma _2,\dots \sigma _k\rangle$ is called elementary iff $\exists i<k$ s.t. $\pi (\sigma _i)\subset \pi (\sigma _k)$ is also an asserting clause derivation.

Using the Definitions 3 and 4, we can now define the concepts of Unique Implication Point (UIP) and First UIP Marques-Silva and Sakallah (1999):

Definition 5

(Unique Implication Point (UIP in short)) A node $x\in \mathcal{N}$ is a UIP iff there exists an asserting clause derivation $\langle \sigma _1,\sigma _2,\dots , \sigma _k\rangle$ st. $\overline{x} \in \sigma _k$ and l(x) is equal to the current decision level, m. (Note that $\sigma _k$, being assertive, has exactly one such x.)

Definition 6

(First Unique Implication Point) A node $x\in \mathcal{N}$ is a First UIP iff it is obtained from an elementary asserting clause derivation; i.e. $\exists \pi (\sigma _k) = \langle \sigma _1,\sigma _2,\dots , \sigma _k\rangle$ an elementary asserting clause derivation st. $\overline{x} \in \sigma _k$ and $l(x)=m$.

Definition 7

(Last Unique Implication Point) The last UIP is defined as the literal $d(\rho , m)$, i.e. the decision literal assigned at the conflict level m.

To illustrate the previous definitions, let us consider again the Example 3.

The traversal of the graph $\mathcal{G}_\mathcal{F}^\rho$ allows us to generate two asserting clauses corresponding to the two possible UIPs (see Fig. 1). Let us illustrate the conflict resolution proof leading to the first asserting clause $\varDelta _1$ corresponding to the first UIP (see cut 1 in Fig. 1, first green line).

• $\sigma _1 = \eta [x_{14}, c_9, c_{10}] = ( \lnot {x}_{11}^5 \vee \lnot {x}_{12}^5 \vee \lnot {x}_{13}^5 )$

• $\sigma _2 = \eta [x_{13}, \sigma _1, c_8] = (\lnot {x}_{10}^5 \vee \lnot {x}_{11}^5 \vee \lnot {x}_{12}^5 )$

• $\sigma _3 = \eta [x_5, \sigma _2, c_7]= (\lnot {x}_4^3 \vee \lnot {x}_{9}^5 \vee \lnot {x}_{10}^5 \vee \lnot {x}_{11}^5 )$

• ....

• $\sigma _6 = \varDelta _1= \eta [x_9, \sigma _5, c_4] = (\lnot {x}_1^1 \vee \lnot {x}_3^2 \vee \lnot {x}_4^3 \vee \lnot {x}_{8}^5 )$

As we can see, $\sigma _6$ gives us a first asserting clause (that we’ll also name $\varDelta _1$) because all of its literals are assigned before the current level except one ($x_{8}$) which is assigned a the current level 5; $\pi (\varDelta _1)=\langle \sigma _1, \sigma _2, \sigma _3, \ldots , \sigma _6 = \varDelta _1\rangle$ is an elementary asserting clause derivation (the intermediate clauses of $\pi (\varDelta _1)$ contain more than one literal of the current decision level 5), and $x_{8}$ is a first UIP.

If we continue such a process, we obtain an additional asserting clause $\varDelta _2 = (\lnot {x}_1^1 \vee \lnot {x}_2^2 \vee \lnot {x}_3^2 \vee \lnot {x}_4^3 \vee \lnot {x}_{5}^5 )$, corresponding to a second UIP $x_{5}^5$; which is the last UIP since it corresponds to the decision literal (see cut 2 in Fig. 1, second green line).

Property 1

(Asserting clause and backjumping) Let $\pi (c= (\alpha \vee x))$ an asserting clause derivation, and $i = jump(c)$. We can safely backjump to level i and consider the partial assignment $\rho ^i\cup \{x\}$

Proof

As $\alpha \subset \overline{\rho ^i}$ the clause c is such that $(\mathcal{F} \wedge c)|_{\rho ^i} \models _* x$, which implies that $(\mathcal{F} \wedge c)|_{\rho ^i} \models x$. Furthermore c is a resolvent so $\mathcal F$ and $\mathcal{F}\wedge c$ are equivalent wrt. satisfiability; therefore $\mathcal{F}|_{\rho ^i} \models x$. This means that at level i the assignment of x to false leads to a conflict. Consequently, at level i, the literal x must be assigned to true.

Property 2

Let $\pi (c= (\alpha \vee x))$ an asserting clause derivation, and $i = jump(c)$. Then x can be deduced by unit propagation at level i, i.e. $(\mathcal{F} \wedge \overline{x})|_{\rho ^i} \models _{*} \perp$.

Proof

The assignment of all literals $y\in \alpha$ to false leads exactly to the same conflict by unit propagation (conflict side of the implication graph).

The above property shows that the asserting literal can be deduced by refutation at level i. This mean that if we apply some lookahead local processing at that level, we could derive it before actually reaching the conflict. The main difficulty, however, lies in how to select efficiently the literals to process by unit propagation. An attempt to answer this question can be found for example in the approaches proposed by Dubois et al. (1996) and Li and Anbulagan (1997).

Grasp Marques Silva and Sakallah (1996) and zChaff Moskewicz et al. (2001) use the First UIP learning scheme, the first cut encountered by a bottom up traversal of the implication graph. Other learning schemes have been proposed by other authors. The decision scheme proposed by Zhang et al. (2001), achieve a complete traversal of the implication graph until reaching the sources of the graph, leading to an asserting clause containing only the negation of decisions literals. Relsat (Bayardo and Schrag 1997) uses the last UIP learning scheme (see Definition 7), the asserting clause have exactly one literal from the current decision level corresponding to the negation of the last decision literal. Zhang et al. (2001) present a comparison of all these and other learning schemes and conclude that First UIP is the best in practice.

An important property that any asserting clause satisfies is the 1-empowering property introduced in Pipatsrisawat and Darwiche (2010). A clause c implied by F is 1-empowering if it allows unit propagation to derive a new implication that would be impossible to derive without c. Let us consider an example from Pipatsrisawat and Darwiche (2010). Let $F= (a\vee b\vee c)\wedge (a\vee b\vee \lnot c)\wedge (a\vee \lnot b\vee c)\wedge (a\vee \lnot b\vee \lnot c)\wedge (\lnot c \vee d) \wedge (c \vee e)$. The clause $(a \vee b)$ is 1-empowering with respect to F because $F\wedge \lnot b\not \models _* a$. The literal a is called an empowering literal of c with respect to F. Contrary, $(d\vee e)$, which is implied by F, is not 1-empowering (i.e., is absorbed), because $F\wedge \lnot d\models _* e$ and $F\wedge \lnot e\models _* d$. Let us give a formal definition of this important property.

Definition 8

(1-empowerment Pipatsrisawat and Darwiche (2010)) Let $(\alpha \vee l)$ be a clause where l is a literal and $\alpha$ is a sub-clause (a disjunction of literals). The clause is 1-empowering with respect to F via l iff

• 1. $F \models (\alpha \vee l)$: the clause is implied by F.

• 2. $F\wedge \bar{\alpha }\not \models _* l$: the literal l cannot be derived from $F\wedge \bar{\alpha }$ using unit propagation.

Any asserting clause is 1-empowering with respect to the formula (original formula augmented with the previous learnt clauses) at the time of its derivation with its asserting literal as an empowering literal. This property plays an important role on the power of clause learning.

In Audemard et al. (2008a, b), the authors prove that the asserting clause learned using the first UIP scheme is optimal with respect to both the backjumping level and to the number of different levels it contains. Let us describe these important properties that explain why the first UIP usually considered in modern SAT solvers is more powerful than the other UIPs.

Given a clause c we denote by levels(c) the measure defined as the set of different levels present in the clause c, i.e. $levels(c) = ~\{l(x) ~|~ x \in c\}$. This measure was first introduced in Audemard et al. (2008b).

Property 3

(Optimality w.r.t. Levels) In an asserting clause derivation $\pi (\sigma _k) = \langle \sigma _1, \dots , \sigma _k \rangle$ we have for all $i < k$, $levels(\sigma _i) \subseteq levels(\sigma _{i+1})$.

Proof

Each $\sigma _{i+1}$ is obtained from $\sigma _i$ by selecting a literal $x \in \sigma _i$ that is not a decision, and replacing this literal by its set of explanations exp(x). These explanations always contain at least another literal y such that $l(y) = l(x)$, and eventually other literals z with (1) $l(z)\in levels(\sigma _i)$ or (2) $l(z)\notin levels(\sigma _i)$. In the first case, the substitution of x in $\sigma _i$ by exp(x) leads to $\sigma _{i+1}$ with $levels(\sigma _{i+1})\supseteq levels(\sigma _i)$.

Property 4

(Optimality wrt. backjumping level (Audemard et al. 2008a, b)) Let $\pi (c = (\alpha , x))$ be an elementary asserting clause derivation and in which x is the first UIP. The back-jumping level of c is optimal: any asserting clause derivation $\pi (c')$ is such that $jump(c') \ge jump(c)$.

Proof

It can be shown that all asserting clauses containing the first UIP have the same backjump level (there could be several such clauses, in general, under our definitions, and their sets of levels may be incomparable). Let $\pi (\sigma _k)=\langle \sigma _1, \dots , \sigma _k =c'\rangle$ be an asserting clause derivation. Let i be the index of the first asserting clause in this proof. Because $\sigma _i$ is an asserting clause we have $jump(c) = jump(\sigma _i)$ and because of Property 3 we have $jump(\sigma _i) \le jump(\sigma _k) = jump(c')$.

The first UIP is the only UIP with these two optimality guarantees: one can construct examples on which the asserting clauses containing any other UIP have a strictly higher backjump level. Note that these optimality results have been proved for the first time in Audemard et al. (2008b).

5.2 Extended clauses learning

These optimality results motivated the extension of the implication graph proposed in Audemard et al. (2008a). The extended graph is obtained by considering additional arcs, called inverse arcs, derived from the satisfied clauses of the formula, which are usually ignored by conflict analysis. Traditionally, when a unit literal y is produced at a given level, the reasons (e.g. $x_1$, $x_2$) of such deduction is recorded. Such an implication is obtained from the clause $(\lnot x_1\vee \lnot x_2\vee y)$ of the original formula. Let us note that $x_1$ and $x_2$ are assigned at levels smaller or equal to the assignment level of y. Suppose that the clause $(x_1\vee \lnot y)$ belong to the formula. This mean that $x_1=true$ is also deduced from the assignment $y=true$. In this case, an “arc” was revealed for free that could as well be used to extend the graph. The extension proposed in Audemard et al. (2008a) encode this new reason (called inverse arcs) because $x_1$ assigned at level i is implied by a literal y assigned at greater or equal level. This extension allows the derivation of better asserting clauses in term of size and backjumping level.

To explain the idea behind the proposed extension, let us consider, again, the formula $\mathcal F$ given in the Example 3. We consider the same partial interpretation and we define a new formula $\mathcal{F'}$ as follow : $\mathcal{F' }\supseteq \{c_1,\dots ,c_{10}\} \cup \{c_{11},c_{12},c_{13}\}$ where $c_{11}=(\lnot {x}_{8} \vee x_{1}), c_{12}=(\lnot {x}_{8} \vee x_{3})$ and $c_{13}=(\lnot {x}_{9} \vee x_{4})$

The three added clauses are satisfied under the partial interpretation $\rho$. $c_{11}$ is satisfied by $x_1$ assigned at level 1, $c_{12}$ is satisfied by $x_{3}$ at level 2, and $c_{13}$ is satisfied by $x_{4}$ at level 3. This is shown in the extended implication graph (see Fig. 2) by the blue arcs. Let us now illustrate the usefulness of the proposed extension. Let us consider again the the asserting clause $\varDelta _1$ corresponding to the classical first UIP scheme. The following strong asserting clause can be derived.

• $\sigma '_{1} = \eta [x_1, \varDelta _1, c_{11}] = (\lnot {x}_{3}^2 \vee \lnot {x}_{4}^3 \vee \lnot {x}_{8}^5)$ 

• $\sigma '_{2} = \eta [x_{3}, \sigma '_{1}, c_{12}] = (\lnot {x}_{4}^3 \vee \lnot {x}_{8}^5)$ 

• $\sigma '_{3} = \eta [x_{4}, \sigma '_{2}, c_{13}] = (\lnot {x}_{9}^5 \vee \lnot {x}_{8}^5)$ 

• $\sigma '_{4} = \eta [x_{9}, \sigma '_{3}, c_{4}] = (\lnot {x}_{3}^2 \vee \lnot {x}_{8}^5)$ 

• $\varDelta _1^s = \eta [x_{3}, \sigma '_{4}, c_{12}] = (\lnot {x}_{8}^5)$

In this case we backtrack to the level 0 and we assign $\lnot {x}_{8}$ to true. Indeed $\mathcal{F'}\models \lnot {x}_{8}$.

As we can see $\varDelta _1^s$ subsumes $\varDelta _1$. If we continue the process we also obtain an other strong asserting clause $\varDelta _2^s= (\lnot {x}_2^2 \vee \lnot {x}_5^5)$ which subsume $\varDelta _2$. This example illustrates how inverse arcs can be used to derive strong asserting clauses i.e. with small sizes and high buckjumping levels.

Fig. 2

Implication graph with inverse arcs : $\mathcal{G}s_\mathcal{F'}^{\rho }= (\mathcal{N}',\mathcal{E}')$

If we take a look to the clauses used in the classical implication graph $\mathcal{G}_\mathcal{F}^{\rho }$ (Fig. 2) all have the following properties: (1) $\forall x\in \mathcal{N}$ the clause $c=(\overline{exp(x)}\vee x)$ is satisfied by only one literal i.e. $\rho (x)={{\textit{true}}}$ and $\forall y\in exp(x)$, we have $\rho (y)={{\textit{true}}}$ and (2) $\forall y\in exp(x)$, $l(\lnot {y})\le l(x)$. Now in the extended implication graph (Fig. 2) the added clauses satisfy property (1) and, in addition, a property (3) $\exists y\in exp(x)$ st. $l(\lnot {y})> l(x)$.

Let us now explain briefly how the extra arcs can be computed. Usually unit propagation does not keep track of implications from the satisfiable sub-formula. In this extension the new implications (deductions) are considered. For instance in the previous example, when we deduce $x_{9}$ at level 5, we “rediscover” the deduction $x_4$ (which was a choice (a decision literal) at level 3). Similarly, for $x_{8}$ deduced at level 5, we “rediscover” the deductions $x_{3}$ (made at level 2) and $x_{1}$ (made at level 1).

This proposal keeps track of these re-discoveries. Note something unusual: even a decision literal (choice point) can now have incoming arcs. This is the case for $x_4$ for instance.

It is important to note that the proposed extension can leads to implications graphs that are not acyclic. In Audemard et al. (2008a), a new concept of joint inverse arc to extend the classical conflict resolution is proposed. The extended learning scheme, exploit classical learning to generate the first asserting clause, then inverse arcs are used to eliminate the literals with higher levels. Some additional conditions are used to avoid cycles in the extended implication graph. For more details, on the practical integration to SAT solvers, we refer the reader to Audemard et al. (2008a).

5.3 Learning Bi-asserting clauses

Another Clause learning scheme is also proposed by Pipatsrisawat and Darwiche (2008). The authors exploit a new class of conflict clauses, called bi-asserting clauses, which is a relaxation of asserting clauses. It is defined as conflict clause with two literals from the current decision level.

Definition 9

[Bi-Asserting clause (Pipatsrisawat and Darwiche 2008)] A clause $c = (\alpha \vee x \vee y)$ is called a Bi-Asserting clause if $\rho (c)={{\textit{false}}}$, $l(\alpha ) < m$ and $l(y) = l(x) = m$.

In Pipatsrisawat and Darwiche (2008), the authors propose an efficient way to derive empowering bi-asserting clauses, but only with respect to the clauses used in its derivation. Indeed, the 1-empowerment property is checked on the fly, by simply checking if the resolution derivation of such clause involves a merging resolution (Andrews 1968). A resolution between two clauses $(a\vee \alpha )$ and $(\lnot a\vee \beta )$ is a merging resolution if $\alpha \cap \beta \ne \emptyset$.

This new class of bi-asserting clauses tends to be much shorter and have smaller assertion levels than asserting clauses for the same conflict. The exploitation of such kind of clauses is particularly suitable for solving unsatisfiable SAT instances.

Recently Jabbour et al. (2013), proposed another interesting approach to derive a new class of bi-asserting clauses. These clauses are obtained by traversing the implication graph separately from x and $\lnot x$. These new kinds of bi-asserting clauses are much shorter and tend to induce more implications than the classical bi-asserting clauses.

Let us, illustrate these new kind of bi-asserting clauses using a simple example. Let $\mathcal{F}$ be a CNF formula, $\rho$ a partial assignment. Assume that we have an implication graph $\mathcal{G}_\mathcal{F}^{\rho }$ associated to $\mathcal{F}$ and $\rho$. For simplicity reason, Fig. 3 depicts the implication graph restricted to the sub-graph induced by the nodes between the conflict and the first UIP.

Assume that the conflict level is 5.

Fig. 3

Sub Implications Graph $\mathcal{G}_\mathcal{F}^\rho = (\mathcal{N},\mathcal{E})$

By traversing the implication graph separately from $x_{14}$ and $\lnot x_{14}$ until the first UIP $x_1$, we derive the new bi-asserting clauses $\pi _1$, $\pi _2$, $\pi _3$, $\pi _4$ as follows:

• $\sigma _1 = \eta [x_{10}, c_{13}, c_9] = \lnot x_{15} \vee \lnot x_{11} \vee \lnot x_{8} \vee x_{14}$

• $\pi _1 = \eta [x_{11}, \sigma _1, c_{10}] = \lnot x_{15} \vee \lnot x_{8} \vee x_{14}$

• $\sigma _2 = \eta [x_4, c_7, c_3] = \lnot x_{17} \vee \lnot x_5 \vee \lnot x_{2} \vee x_8$

• $\pi _2 = \eta [x_5,\sigma _2, c_4] = \lnot x_{17} \vee \lnot x_{2} \vee x_{8}$

• $\sigma _3 = \eta [x_{12}, c_{14}, c_{11}] = \lnot x_{13} \vee \lnot x_{9} \vee \lnot x_{14}$

• $\pi _3 = \eta [x_{13}, \sigma _3, c_{12}] = \lnot x_{15} \vee \lnot x_{9} \vee \lnot x_{14}$

• $\sigma _4 = \eta [x_6, c_8, c_5] = \lnot x_{3} \vee \lnot x_{7} \vee x_9$

• $\pi _4 = \eta [x_7,\sigma _4, c_6] = \lnot x_{16} \vee \lnot x_{3} \vee x_{9}$

The new bi-asserting clauses $\pi _1$, $\pi _2$, $\pi _3$, $\pi _4$ form a set of connected clauses. More precisely, the clause $\pi _2$ is connected with $\pi _1$ by the variable $x_{8}$, $\pi _1$ is connected with $\pi _3$ by the variable $x_{14}$ and $\pi _3$ is connected with $\pi _4$ by the variable $x_{9}$. As we can observe the set of bi-asserting clauses form a chain of connected clauses. It is important to note that the classical bi-asserting clauses that can be obtained from the implication graph of Fig. 3 are:

• $\pi _1' = \lnot x_{15} \vee \lnot x_8 \vee \lnot x_9$,

• $\pi _2' = \lnot x_{15} \vee \lnot x_{17} \vee \lnot x_2 \vee \lnot x_9$,

• $\pi _3' = \lnot x_{15} \vee \lnot x_{16} \vee \lnot x_8 \vee \lnot x_3$,

• $\pi _4' = \lnot x_{15} \vee \lnot x_{17} \vee \lnot x_{16} \vee \lnot x_2 \vee \lnot x_3$.

Let us note that by classical clause learning (First UIP scheme), one can derive the asserting clause $(\lnot x_{15} \vee \lnot x_{17} \vee \lnot x_{16} \vee \lnot x_1 )$. The back-jumping level is 3.

Fig. 4

New and compact implication graph obtained from $\mathcal{G}_\mathcal{F}^\rho = (\mathcal{N},\mathcal{E})$ using the new bi-asserting clauses

In Fig. 4, we show that the original implications graph (Fig. 3) can be rewritten more compactly. Let us now consider that the new bi-asserting clauses $\pi _1$, $\pi _2$, $\pi _3$ and $\pi _4$ are added to the learnt clauses database and assume that at level 3 the literal $x_2$ is assigned to true. It is easy to see that all the literals $x_8$, $x_{14}$, $\lnot x_9$, $\lnot x_{3}$ and $\lnot x_1$ (see Fig. 4) together with the literals $x_4$, $x_5$, $x_{10}$, $x_{11}$ are implied by unit propagation. These last unit propagated literals are implied thanks to the original clauses of the formula $c_3$, $c_4$, $c_9$ and $c_{10}$. However, if we consider the original implication graph (Fig. 3), we derive by unit propagation the same set of literals except $\lnot x_9$, $\lnot x_3$ and $\lnot x_1$.

Suppose now that all the classical bi-asserting clauses $\pi _1'$, $\pi _2'$, $\pi _3'$ and $\pi _4'$ are added to the learnt clauses database, assigning $x_2$ to true at level 3 leads to the same set of implications by unit propagation. However, if we decide to assign $x_{14}$ to true at level 3, using the new bi-asserting clauses we derive $\lnot x_{9}$, $\lnot x_{3}$ and $\lnot x_{1}$ while with the classical bi-asserting clauses no literal is implied by unit propagation. Another important difference that can be made is that the derivation of all possible classical bi-asserting clauses is quadratic in the worst case, while the new bi-asserting clauses can be derived in linear time (see the Fig. 4). Consequently, searching for all classical bi-asserting clauses takes more time than for the new proposed bi-asserting clauses. Moreover, the new bi-asserting clauses are much shorter than classical ones.

From this illustrative example, we see that adding the new bi-asserting clauses to the clauses database allows to derive more implications than with classical bi-asserting clauses. We can observe that the proposed bi-asserting clauses establish a link between the asserting literal and the conflicting literals $x_{14}$ and $\lnot x_{14}$. In Jabbour et al. (2013), the authors present formally such separate conflict analysis to derive bi-asserting clauses. From the experiments presented by the authors, integrating such clauses in SAT solvers, improve their performance particularly on crafted instances.

5.4 Learning back-clauses

As mentioned previously, First Unique Implication Point (First UIP) is the traditional learning scheme. Obviously, an implications graph might contains several unique implication points from the first to the last UIP corresponding to the asserting clause involving the last decision literal of the current branch. We argued in the previous section that the first UIP is better than others with respect to both the buckjumping level and to the number of different levels involved in the clause. However, deriving other clauses connecting all these implications points, will enable unit propagation to make all inferences that all traditional asserting clauses based on all the UIPs. In Sabharwal et al. (2012), the authors proposed a learning scheme that record these kind of clauses, called back-clauses. The idea of learning back-clauses during search is first introduced in Marques Silva and Sakallah (1996). In Sabharwal et al. (2012), it is also shown that adding back-clauses is stronger than adding all asserting clauses corresponding to all UIPs.

Let us illustrate this notion using the example depicted in Fig. 1 admitting only two UIPs. From the example we can derive two asserting clauses, $\varDelta _1 = (\lnot {x}_1^1 \vee \lnot {x}_3^2 \vee \lnot {x}_4^3 \vee \lnot {x}_{8}^5 )$ and $\varDelta _2 = (\lnot {x}_1^1 \vee \lnot {x}_2^2\vee \lnot {x}_3^2 \vee \lnot {x}_4^3 \vee \lnot {x}_{5}^5 )$ corresponding to the first and last UIPs respectively. A back-clause, can be derived by resolution starting from the first UIP node ($x_8$), leading to the clause $B=(\lnot {x}_{2}^2\vee \lnot {x}_{5}^5\vee {x}_{8}^5)$. We observe that the back-clause B contains two literals from the current conflict level, it can be seen as a non conflicting bi-asserting clause, satisfied by the current partial interpretation ($\rho (x_{8}) = true$). Let us now, explain why recording such back-clauses, can leads to more propagation at the buckjumping level 3 ($jump(\varDelta _1)=3$). Suppose that, after such conflict, we record both the classical asserting clause $\varDelta _1$ corresponding to the first UIP and the back-clause B. At the backjumping level 3, the asserting literal $\lnot x_{8}$ is implied, thanks to the asserting clause $\varDelta _1$. By adding the back-clause B, the literal $\lnot x_5$ is propagated. This last literal can not be deduced by unit propagation even if we record all the asserting clauses $\varDelta _1$ and $\varDelta _2$. Consequently, connecting the different asserting clauses using back clauses, allows further propagations.

5.5 Learning for dynamic subsumption

Usually, clauses learning is used to analyse the reason of the conflict. We now describe, an original approach introduced in Hamadi et al. (2009a) that exploit clause learning to dynamically subsume some clauses of the formula. The approach exploits the intermediate steps or resolvents generated during the classical conflict analysis to subsume some of the clauses used in the underlying resolution derivation of the asserting clause.

Let us, illustrate some of the main features of this approach using the Example 3 and the implication graph $\mathcal{G}_\mathcal{F}^\rho$ (Fig. 1). The asserting clause derivation leading to the asserting clause $\varDelta _1$ is described as follows:

$\pi (\varDelta _1) = \langle \sigma _1,\sigma _2, \sigma _3, \dots , \sigma _7 = \varDelta _1\rangle$

• $\sigma _1 = \eta [x_{14}, c_9, c_{10}] = ( \lnot {x}_{11}^5 \vee \lnot {x}_{12}^5 \vee \lnot {x}_{13}^5 )$ 

• $\sigma _2 = \eta [x_{13}, \sigma _1, c_8] = (\lnot {x}_{10}^5 \vee \lnot {x}_{11}^5 \vee \lnot {x}_{12}^5 )$ 

• $\sigma _3 = \eta [x_{12}, \sigma _2, c_7]= (\lnot {x}_4^3 \vee \lnot {x}_{9}^5 \vee \lnot {x}_{10}^5 \vee \lnot {x}_{11}^5 )$ 

• $\sigma _3 = \eta [x_{11}, \sigma _2, c_7]= (\lnot {x}_4^3 \vee \lnot {x}_{9}^5 \vee \lnot {x}_{10}^5 \vee \lnot {x}_{11}^5 )$ 

• $\sigma _4 = \eta [x_{10}, \sigma _2, c_7]= (\lnot {x}_4^3 \vee \lnot {x}_{9}^5 \vee \lnot {x}_{10}^5) \subset c_7$ (subsumption)

• $\dots$ 

• $\sigma _7 = \varDelta _1 = \eta [x_9, \sigma _5, c_4] = (\lnot {x}_1^1 \vee \lnot {x}_3^2 \vee \lnot {x}_4^3 \vee \lnot {x}_{8}^5 )$

As we can see the asserting clause derivation $\pi (\varDelta _1)$ includes the resolvent $\sigma _4 = (\lnot {x}_4 \vee \lnot {x}_{9} \vee \lnot {x}_{10})$ which subsumes the clause $c_7 = (\lnot {x}_4 \vee \lnot {x}_{9} \vee \lnot {x}_{10} \vee x_{12})$. Consequently, the literal $x_{12}$ is eliminated from the clause $c_7$. In general, the resolvent $\sigma _4$ can subsume other clauses from the implication graph that include the literals $\lnot {x}_4$, $\lnot {x}_9$ and $\lnot {x}_{10}$.

Let us now give the formal presentation of of this dynamic subsumption approach.

Definition 10

(F-subsumption modulo UP) Let $c\in \mathcal{F}$. c is $\mathcal{F}$-subsumed modulo unit propagation iff $\exists c'\subset c$ such that $\mathcal{F}|_{\tilde{c'}} \models ^* \bot$

Given two clauses $c_1$ and $c_2$ from $\mathcal{F}$ such that $c_1$ subsumes $c_2$, then $c_2$ is $\mathcal{F}$-subsumed modulo UP.

Subsuming clauses during search might be time consuming. To reduce the computational cost, the authors restrict the subsumption checks to the intermediate resolvents $\sigma _i$ and to the clauses of the form $\overrightarrow{imp}({y})$ used to derive them (clauses encoded in the implication graph).

Definition 11

Let $\mathcal{F}$ be a formula and $\pi (\sigma _k)= \langle \sigma _1 \ldots \sigma _k\rangle$ an asserting clause derivation. For each $\sigma _i \in \pi$, we define $\mathcal{C}_{\sigma _i} = \{\overrightarrow{imp}({y}) \in \mathcal{F}| \exists j \le i$ st. $\sigma _j = \eta [y, \overrightarrow{imp}({y}), \sigma _{j-1}]\}$ as the set of clauses of $\mathcal{F}$ used for the derivation of $\sigma _i$.

Property 5

Let $\mathcal{F}$ be a formula and $\pi (\sigma _k) = \langle \sigma _1,\sigma _2,\dots , \sigma _i,\dots , \sigma _k\rangle$ an asserting clause derivation. If $\sigma _i$ subsumes a clause c of $\mathcal{C}_{\sigma _k}$ then $c\in \mathcal{C}_{\sigma _i}$.

Proof

As $\sigma _{i+1} = \eta [y, \overrightarrow{imp}({y}), \sigma _i]$ where $\lnot {y}\in \sigma _i$, we have $\sigma _i\not \subset \overrightarrow{imp}({y})$. The next resolution steps can not involve clauses containing the literal $\lnot {y}$. Otherwise, the literal y in the implication graph will admit more than one possible explanation, which is not possible by definition of the implication graph. Consequently, $\sigma _i$ can not subsume clauses from $\mathcal{C}_{\sigma _k}- \mathcal{C}_{\sigma _i}$.

Property 6

Let $\mathcal{F}$ be a formula and $\pi$ an asserting clause derivation. If $\sigma _i\in \pi$ subsumes a clause c of $\mathcal{C}_{\sigma _i}$ then c is $\mathcal{C}_{\sigma _i}$-subsumed modulo UP.

Proof

As $\sigma _i\in \pi$ is derived from $\mathcal{C}_{\sigma _i}$ by resolution, then $\mathcal{C}_{\sigma _i}\models \sigma _i$. By definition of an asserting clause derivation and implication graphs, we also have $\mathcal{C}_{\sigma _i} \models ^* \sigma _i$ (see Sect. 5). As $\sigma _i$ subsumes c ($\sigma _i\subseteq c$), then $\mathcal{C}_{\sigma _i}\models ^* c$.

The Property 6 shows that if a clause c encoded in the implication graph is subsumed by $\sigma _i$, such subsumption can be captured by subsumption modulo UP, while the Property 5 mention that subsumption checks of $\sigma _i$ can be restricted to clauses from $\mathcal{C}_{\sigma _i}$. Consequently, a possible general dynamic subsumption approach can be stated as follows: Let $\pi (\sigma _k)= \langle \sigma _1,\ldots ,\sigma _i,\dots , \sigma _k\rangle$ be an asserting resolution derivation. For each resolvent $\sigma _i\in \pi (\sigma _k)$, we apply subsumption checks between $\sigma _i$ and all the clauses in $\mathcal{C}_{\sigma _i}$.

In the following, we show that we can reduce further the number of clauses to be checked for subsumption by considering only a subset of $\mathcal{C}_{\sigma _i}$. Obviously, as $\sigma _i$ is a resolvent of an asserting clause derivation $\pi (\sigma _k)$, then there exists two paths from the conflict nodes x and $\lnot {x}$ respectively, to one or more nodes of the implication graph associated to the literals of $\sigma _i$ assigned at the conflict level. Consequently, we derive the following property:

Property 7

Let $\pi$ be an asserting clause derivation, $\sigma _i\in \pi$ and $c \in { \mathcal C}_{\sigma _i}$. If $\sigma _i$ subsumes c, then there exists two paths from the conflict nodes x and $\lnot {x}$ respectively, to one or more nodes of the implication graph associated to the literals of c assigned at the conflict level.

Proof

The proof of the property is immediate since $\sigma _i\subset c$. As this property is true for $\sigma _i$ which is derived by resolution from the two clauses involving x and $\lnot {x}$. Then it is also, true for its supersets (c).

For a given $\sigma _i$, the Property 7 leads us to another restriction of the set of clauses to be checked for subsumption. Indeed, we only need to consider the set of clauses ${ \mathcal P}_{\sigma _i}$, linked (by paths) to the two conflicting literals x and $\lnot {x}$.

We illustrate this characterization using the Example 3 (see also Fig. 1). Let $\pi (\sigma _k) =\langle \sigma _1, \dots , \sigma _6 \rangle$ where $\sigma _6 = (\lnot {x}_{1} \vee \lnot {x}_{2} \vee \lnot {x}_{4} \vee \lnot {x}_8)$. We have ${ \mathcal C}_{\sigma _6} = \{c_4, c_5, c_6, c_7, c_8, c_9,c_{10} \}$ and ${ \mathcal P}_{\sigma _6} = \{c_4, c_5, c_7, c_8\}$. Indeed, from the nodes associated to the clause $c_6$ we only have one path to the node $x_{14}$. Consequently, the clause $c_6$ might be discarded from the set of clauses to be checked for subsumption. Similarly, the clause $c_9$ and $c_{10}$ are only linked to one node of the set $\{ x_{14}, \lnot {x}_{14} \}$. Then $c_9$ and $c_{10}$ are not considered for subsumption tests.

Property 8

Given an asserting clause derivation $\pi (\sigma _k) =\langle \sigma _1, \dots ,\sigma _k \rangle$. The time complexity of our general dynamic subsumption approach is in $O(|{ \mathcal C}_{\sigma _k}|^2$).

Proof

From the definition of ${ \mathcal C}_{\sigma _i}$, we have $|{ \mathcal C}_{\sigma _i}| = i+1$. In the worst case, we need to consider $i+1$ subsumption checks. Then for all $\sigma _i$ with $1\le i\le k$, we have to check $\sum _{1\le i\le k} (i+1) = \frac{k\times (k+3)}{2}$. As $k= |{ \mathcal C}_{\sigma _k}|$, then the worst case complexity is in $O(|{ \mathcal C}_{\sigma _k}|^2$).

The worst case complexity is quadratic even if we consider ${ \mathcal P}_{\sigma _k}\subset { \mathcal C}_{\sigma _k}$.

To design an efficient dynamic simplification technique, one need to balance the run time cost and the quality of the simplification. In Hamadi et al. (2009a), a restriction of the general dynamic subsumption scheme, called dynamic subsumption on the fly, which applies subsumption only between the current resolvent $\sigma _i$ and the last clause from the implication graph used for its derivation. More precisely, suppose $\sigma _i = \eta [y, c, \sigma _{i-1}]$, subsumption checks are only performed between $\sigma _i$ and c. The following property gives a sufficient condition under which y can be removed form c

Property 9

Let $\pi$ be an asserting clause derivation, $\sigma _i\in \pi$ such that $\sigma _i = \eta [y, c, \sigma _{i-1}]$. If $\sigma _{i-1}-\{y\} \subseteq c$, then c is subsumed by $\sigma _i$.

Proof

Let $c = (\lnot {y} \vee \alpha )$ and $\sigma _{i-1} = (y \vee \beta )$. Then $\sigma _i=(\alpha \vee \beta )$. As $\sigma _{i-1}-\{y\} \subseteq c$, then $\beta \subseteq \alpha$. So, $\sigma _i = \alpha$ which subsumes $(\lnot {y} \vee \alpha ) = c$.

Considering modern SAT solvers that include conflict analysis, the integration of this dynamic subsumption approach is done with negligible additional cost. Indeed, by using a simple counter during the conflict analysis procedure, one can verify the sufficient condition given in the Property 9 in constant time. Indeed, at each step of the asserting clause derivation, the next resolvent $\sigma _i$ is generated from a clause c and a resolvent $\sigma _{i-1}$. In the classical implementation of conflict analysis, one can check in constant time if a given literal is present in the current resolvent. Consequently, during the visit of the clause c, we only need to compute the number n of literals of c that belong to $\sigma _{i-1}$. If $n \ge |\sigma _{i-1}|-1$ then c is subsumed by $\sigma _i = \eta [y, c, \sigma _{i-1}]$.

5.6 Learning from success

In Jabbour (2009), Said Jabbour showed that new explanations for implied (unit propagated) literals can be generated even if a partial assignment does not lead to a conflict. Let us explain this issue, using an example.

Example 4

Let $\mathcal{F}'$ the new formula obtained from $\mathcal{F}$ (see Example 3) by removing the clause $c_{10}$ and adding the clause $c_{11}=(\lnot x_2\vee x_{8}\vee x_{14})$. The implication graph $\mathcal{G}_\mathcal{F'}^\rho$ is the a sub-graph of $\mathcal{G}_\mathcal{F}^\rho$ (see Fig. 1) induced by the set of nodes $\mathcal{N}\backslash \{\lnot x_{14}, x_{13}\}$. Clearly, the partial assignment $\rho$ does not lead to a conflict at the decision level 5. We can remark, that the clause $c_{11}$ is not recorded in the implication graph $\mathcal{G}_\mathcal{F'}^\rho$ as it contains two literals $x_{8}$ and $x_{14}$ assigned to true. Moreover, the literal $x_{14}$ is assigned by unit propagation at level 5 due to the clause $c_9$ and $\rho$. Let us now illustrate how one can deduce a new reason (clause) asserting that $x_{14}$ can be assigned at level less than 5. A traversal of the implication graph starting from the node $x_{14}$, leads to the clause : $\varDelta = (\lnot x_1^1\vee \lnot x_3^2 \vee \lnot x_4^3\vee \lnot x_8^5\vee x_{14}^5)$.

The clause $\varDelta$ contains only two literals $\lnot x_{8}$ and $x_{14}$ from the current decision level 5 and all its literals are assigned false except $x_{14}$ which is assigned to true. Now, if we apply one additional resolution step between $\varDelta$ and $c_{11}=(\lnot x_2\vee x_{8}\vee x_{14})\in \mathcal{F}'$, we obtain a new asserting clause $\varDelta ' = (\lnot x_1^1\vee \lnot x_2^2\vee \lnot x_3^2 \vee \lnot x_4^3\vee x_{14}^5)$ . This last clause expresses that the literal $x_{14}$ assigned at level 5 can be assigned at level 3. Indeed, as $\mathcal{F}'\models \varDelta '$ and the literals $\lnot x_1, \lnot x_2, \lnot x_3$ and $\lnot x_4$ are assigned false at levels less than 3, we deduce that the literal $x_{14}$ assigned at level 5 can be assigned by unit propagation at level 3 thanks to the new reason $\varDelta '$.

In Jabbour (2009), this idea is used to reorder the current partial assignment thanks to the new derived better reasons for unit propagated literals. These reasons allows to assign such literals at previous levels.

6 Modern SAT solvers

In this section we first give a brief description of the other components of modern SAT solvers not covered in the previous sections. Then we present the CDCL-based SAT algorithm. This will give to the reader the whole picture about modern SAT solvers including the learning component. For a more detailed description, the reader can see Sais (2008) and Biere et al. (2009).

Modern SAT solvers are especially efficient with structured SAT instances coming from industrial applications. On application domains, Gomes et al. (2000) have identified a heavy tailed phenomenon, i.e., different variable orderings often lead to dramatic differences in solving time. This explains the introduction of restart policies in modern SAT solvers, which attempt to discover a good variable ordering. Variable State Independent Decaying Sum (VSIDS) and other variants of activity-based heuristics, on the other hand, were introduced to avoid thrashing and to focus the search on the most constrained parts of the formula. Restarts and VSIDS play complementary roles since they implement the two principles of respectively, diversification and intensification. Conflict driven clause learning (CDCL) is the third component, leading to non-chronological backtracking. The activity of the variables are updated during the learning process, allowing VSIDS to always select the most active variable as the new decision point. As the number of learned clauses might be exponential in the worst case, several deletion strategies are proposed to keep a learnt clauses database of manageable size. On the other hand, to allow solving large SAT instance, the introduction of lazy data-structure, called watched literals is crucial for the efficiency of modern SAT solvers. Reducing the size of the input formula in a preprocessing step is another important component, usually integrated in all the state-of-the-art SAT solvers.

6.1 Restarts strategies

Restarts policy were introduced for the first time as early as 1994 in Crawford and Baker (1994). When a solver restarts, the current partial interpretation is left and the search starts again at the root of the search tree, while maintaining several informations cumulated from the previous runs (e.g. learned clauses, variables activities). Restarts are presented by Gomes et al. (1998) to eliminate the heavy tailed phenomena observed on many families of SAT instances. Indeed, this observed phenomena demonstrates that on many instances different variables ordering might lead to dramatic performance variation of a given SAT solver. Restarts aim to eliminate the long runs by increasing the probability to fall on the best variables ordering. In modern SAT solvers, restarts dive the search to the most actives variables and aims to compact the assignment stack and to improve the order of assumptions.

Different restart policies have been previously presented. Most of them are static, and the cutoff value follows different evolution schemes (e.g. arithmetic, geometric, Luby ). To ensure the completeness of the SAT solver, in all these restarts policies, the cutoff value in terms of the number of conflicts increases over the time. The performance of these different policies clearly depends on the considered SAT instances. More generally, rapid restarts [e.g. Luby et al. (1993)] perform well on industrial instances, however on hard SAT instances slow restarts is more suitable. Generally, it is hard to say in advance which policy should be used on which problem class (Huang 2007). More recently, several dynamic and adaptive restarts policies are proposed, the cutoff value is computed during search using observed informations on the running behavior of the solver (Biere 2008; Pipatsrisawat and Darwiche 2009; Hamadi et al. 2009b).

6.2 Activity based heuristics

Branching heuristics aim to select the next variable to assign at each node of the search tree. Such variable selection strategy induces an assignment ordering which is known to be crucial for the efficiency of SAT solvers. Many heuristics have been proposed in the literature, most of them are based on syntactical arguments such as the number of occurrences of the variables, the size of the clauses, etc. One of the most popular strategies, is the dynamic largest individual sum (DLIS) heuristic (Marques-silva 1999), that choose the variable and the assignment that directly satisfy the largest number of clauses. Other sophisticated heuristic functions have been proposed, one can cite the Jeroslow and Wang (1990) heuristic and many other variants which select the variable occurring most frequently in short clauses. All these heuristics need to maintain such arguments during search, which can be very costly on large SAT instances.

Recently, the Chaff SAT solver proposed the use of the variable state independent decaying sum (VSIDS) heuristic (Moskewicz et al. 2001). An activity is associated to each variable. Each time a variable occurs in a recorded learnt conflict clause, its activity is increased. Additionally, to give more importance to the variables involved in the most recent learnt clauses, the activity of all the variables are multiplied by a constant less than 1. MiniSAT uses similar ideas (Een and Sörensson 2005). However, the activity update is not limited to the variables occurring in the final learnt conflict clause, but considers all the variables occurring in any clause used in the conflict analysis.

Activity based heuristics take their origin from the principle used in the break-out local search method (Morris 1993), where the score of falsified clauses is increased during the search and used to escape from local minima. Brisoux et al. (1999), proposed an extension of the clause-weighting scheme to DPLL-like techniques. Every time a conflict is reached, the score of the falsified clauses is increased. The next variable is chosen according to its occurrence in most falsified clauses. The MiniSAT heuristic (Een and Sörensson 2005) updates the activity of the variables encountered between the conflict side and the first UIP, while in Brisoux et al. (1999), only the variables of the two last clauses at the origin of the contradiction are updated. VSIDS and MiniSAT heuristics are cheap to maintain and they are shown to be very effective on a variety of problems.

6.3 Lazy data structures—watched literals

The two watched literals scheme introduced in Zchaf Moskewicz et al. (2001), now integrated in most SAT solvers allows efficient unit propagation. This lazy data structure is an improvement of the one introduced earlier by Zhang (1997) in the solver Sato. The idea behind two watched literals, is to maintain an invariant for each active clause by marking or “watching” two special literals not assigned the value false. A clause containing such two watched literals cannot be involved in unit propagation. Such invariant is maintained with a very small overhead, while no update is needed in case of backtracking. This leads to a substantial saving of computation time. For more details on how such invariant is maintained see Moskewicz et al. (2001) and Een and Sörensson (2005).

6.4 Learnt database deletion strategies

Conflict driven clause learning is recognized as a powerful technique both in theory and practice. However, the set of clauses that can be derived from conflicts is of exponential size in the worst case. In practice, the number of such clauses can sometimes be greater than the number of clauses of the original formula. Several strategies have been designed to cope with this combinatorial explosion problem. To maintain a relevant learnt clauses database of polynomial size - and consequently a unit propagation of reasonable cost - all these strategies dynamically reduce the learnt database by deleting clauses considered to be irrelevant to the next search steps. The most popular strategy considers a learnt clause as irrelevant if its activity or its involvement in conflict analysis is marginal. Several clauses deletion strategies have been integrated in different SAT solvers (Marques-Silva and Sakallah 1999; Moskewicz et al. 2001; Eén and Sörensson 2003). In most cases, these strategies prefer to keep a learnt clauses database, with smaller, recent and active clauses. In Audemard et al. (2011), a new dynamic management policy of the learnt clauses database is introduced. It is based on a dynamic freezing and activation principle of the learnt clauses. At a given search state, it activates the most promising learnt clauses while freezing irrelevant ones. In this way, previously learned clauses can be discarded for the current step, but may be activated again in future steps of the search process. This policy tries to exploit pieces of information gathered from the past to deduce the relevance of a given clause for the remaining search steps.

In Guo et al. (2014), we proposed two new measures to predict the quality of learned clauses. The first one is based on the backtracking level (BTL), while the second is based on a notion of distance, defined as the difference between the maximum and minimum assignment levels of the literals involved in the learned clause.

More recently, Jabbour et al. (2014) revisited size-bounded learning strategies proposed more than fifteenth years ago (Bayardo and Schrag 1997; Bayardo and Miranker 1996; Marques Silva and Sakallah 1996) and show that these strategies remains a competitive with the state-of-the-art ones. They also demonstrate that adding randomization to size bounded learning is a nice way to achieve controlled diversification. It allows to favor short clauses, while maintaining a small fraction of large clauses necessary for deriving resolution proofs on some SAT instances.

Finally, size-bounded clause sharing strategies are also considered in several portfolio and divide and conquer based parallel SAT solvers (e.g. Hamadi et al. 2009b; Hamadi and Wintersteiger 2013; Hamadi et al. 2008, 2011).

6.5 Preprocessing

Many preprocessing techniques have been proposed over the years. In this section, we particularly limit our presentation to the most popular and useful ones. Among them, SatElite (Eén and Biere 2005) is clearly the most efficient and used preprocessing technique. Once again, it is based on variable elimination through the resolution rule. SatElite is an extension of NIVER (non increase variable elimination by resolution) originally proposed in Subbarayan and Pradhan (2004). The extension includes variable elimination by substitution using boolean functions, subsumption and self-subsuming resolution. As mentioned by Subbarayan and Pradhan (2004), on industrial instances, resolution leads to the generation of many tautological resolvents. This can be explained by the fact that many clauses represent Boolean functions encoded through a common set of variables. This property of the encodings might also be at the origin of many redundant or subsumed clauses at different steps of the search process. The utility of (SatElite) on industrial problems has been proved, and therefore one can wonder if the application of the resolution rule could be performed not only as a pre-processing stage but systematically during the search process. Unfortunately, dynamically maintaining a formula closed under subsumption might be time consuming. An attempt has been made recently in this direction by Zhang (2005). Another original technique called learning for dynamic subsumption is proposed in Hamadi et al. (2009a). At each conflict, it exploits clause learning to subsume clauses of the original formula and of the learnt clauses database. Designing strong preprocessing techniques able to greatly reduce the size of the formula remains an important research issue [see for example recent works by Heule et al. (2010, 2011), and Piette et al. (2008)].

6.6 CDCL-based SAT algorithm

Let us now give a general formulation of a CDCL-based SAT solver (Algorithm 1) (Pipatsrisawat and Darwiche 2009). As we can see the algorithm starts with an empty set of decision literals and an empty learnt clauses database (lines 1 and 2). At each iteration, the current formula $\mathcal{S}$ is closed under unit propagation (line 5). In case of conflict (lines 6–10), if the set of decisions literals is empty (line 6), the formula is answered unsatisfiable, otherwise a new asserting clause is derived by learning from conflict (line 7). In this last case, the algorithm backtracks to the assertion level m (line 9) and adds the asserting clause to the learnt clauses database (line 10). If no conflict occurs (lines 12–21), the algorithm either reduces the learnt database (lines 12–13) and/or restarts the search process (lines 15–17) using reduction and restarts policies respectively. Then a new decision literal is selected according to VSIDS heuristics and polarity functions (Een and Sörensson 2005; Pipatsrisawat and Darwiche 2007). The chosen literal is then added to the set of decisions with its associated level (line 21). If all the variables are assigned (line 19–20) a model is found and the formula is answered satisfiable.

Modern SAT solvers are based on the general scheme depicted in Algorithm 1. Several variants of this basic scheme are designed and implemented. For more details about these solvers and their performances, see the annual SAT competition or SAT race evaluation (http://www.satcompetition.org/).

7 General conclusion

In this survey, we presented learning from conflict, one of the most powerful reasoning technique in propositional satisfiability. Learning from conflict is a general concept used to explain failures or conflicts encountered during search. This explanation, derived by conflict analysis, and generally expressed as a new constraint, is usually used to dynamically avoid future occurrences of similar situations. After a brief discussion of most of the related works in SAT and other domains, we formally described clause learning currently integrated in most of the state-of-the-art modern SAT solvers. To give a more comprehensive view, other important components of SAT solvers such as restarts, activity based heuristics, learnt clauses database deletion strategies, lazy data structures and preprocessing are also sketched. Finally a general SAT algorithm is given to illustrate the interaction between all these strong and powerful components.

The proximity between propositional satisfiability and 0/1 linear programming, suggests that cross-fertilization remains an important issue that will benefits to both domains. We hope that this survey will give to the operation research community a comprehensive vision about clause learning and satisfiability solving.