Con ict-directed clause learning (CDCL) is the basis of SAT solvers with impressive performance on many problems. CDCL with restarts (CDCL-R) has been shown to have essentially the same reasoning power as unrestricted resolution (formally, they p-Simulate each other). We show that this property generalizes to multi-valued CNF formulas. In particular, for Signed (or Multi-Valued) CNF formulas, and Regular Formulas, we show that a natural generalization of CDCL-R to these logics has essentially the same reasoning power as natural generalizations of resolution from the literature. These formulas are possible reduction targets for a number of multi-valued logics, and thus a possible basis for e cient reasoning systems for these logics.
Multi-valued logics are among the most established formal methods for
reasoning with uncertainty. In this paper, we study a property relating resolution
proofs and a family of satis ability algorithms for multi-valued CNF formulas,
as de ned in, for example, [
The dominant algorithm in modern SAT solvers is the con ict-directed clause
learning algorithm, introduced in [
Because most SAT solvers require input in CNF, it is standard to solve
propositional logic reasoning problems by reduction to CNF. Validity or satis ability
of many multi-valued and fuzzy logics (as well as annotated logics, and others)
can be reduced to Signed or Multi-Valued CNF formulas [
We assume the reader is familiar with the standard CDCL-R algorithm. (A
self-contained description of CDCL and its relationship to resolution can be
found in [
A number of algorithms and solvers for signed or multi-valued formulas, or
special cases of them, have been described in the literature. We leave a review
of these to a longer paper. Here we point out only that our algorithm, while
presented very di erently, seems essentially the same as that described in [
The organization of the paper is as follows. In Section 2 we de ne Signed CNF formulas, the speci c families of formulas we study, and binary resolution for these formulas. The properties of resolution proofs which are central to the proof are de ned in Section 3. In Section 4 we describe an algorithm which embodies the core reasoning in (our generalization of) CDCL-R, while Section 5 shows that repeated calls to this algorithm can refute formulas as e ciently as resolution. In Section 6 we give our generalized CDCL-R algorithm, de ne p-simulation and give the main theorem. We conclude brie y in Section 7. 2
Let D be a nite set of truth values and P a countably in nite set of multi-valued propositional atoms. Signed CNF formulas for D are constructed from literals of the form p2S, where S is a non-empty proper subset of D and p 2 P. (In the literature on Signed CNF, literals are usually written S:p, but we prefer the set notation for readability.) Formally S is a string of constant symbols, denoting elements of D, enumerating the set S. This is typically glossed over, so that S is used both for the set of truth values and the string representing it.
A clause is a disjunction of literals, and a formula is a conjunction of clauses.
When convenient we identify clauses with sets of literals, and formulas with sets
of clauses. An assignment for formula and truth value set D is a function
mapping the propositional symbols in to D. By \assignment", we often mean
partial assignment. Assignment satis es literal p2S if (p) is in the subset of D
denoted by the string S. De nitions of satisfaction, implication, and equivalence
of CNF formulas follow in the standard manner [
A number of variants of this basic logic have been studied. Typical variants restrict the allowed literals, or impose structure on the truth set D. We consider the following three. (Unfortunately, terminology is not uniform in the literature, so our terms may correspond only roughly to those in some other papers.) 1. Multi-Valued CNF (MV-CNF): Formulas as just described, with the requirement that each propositional symbol p occurs in at most one literal in any clause. 2. Regular CNF over a lattice (Reg-CNF): Let D = hD; i be a lattice.
We call a literal p2S regular for D i S is either the upset "i = fs 2 D j i sg, or the downset #i = fs 2 D j s ig of some i in D. A formula is regular for D if every literal in is regular for D.
Let D = hD; i be a set with total order. For each literal p2S, there is some i 2 D for which S is "i, #i, or a complement of one of these, "i or #i.
For generic remarks, we use the term \signed CNF" or \signed formula", and we use one of these speci c terms when remarks apply to a speci c case. Example 1. Consider the signed formulas with D = f0; 1g. These are equivalent to classical CNF formulas.
Example 2. Consider regular formulas for D = hD; <i, where, D is the set f s 0 1 ; s 1 1 ; s 2 1 ; : : : ss 11 g, and < is the standard order on Q. Formulas for D correspond to the standard multi-valued logics with nite truth value set, which were the original motivation for the study of signed CNF formulas.
The complement of a regular atom is not necessarily regular, and may not even be equivalent to any disjunction of regular atoms. Thus, the regular CNF do not allow complements of literals. We included the third case, regular CNF over a total order, with complements, because it corresponds naturally to standard multi-valued logics. However, the proof for Multi-Valued CNF captures this case, so we mention it directly only on occasion. 2.1
Let Signed Binary Resolution be the following derivation rule p2S _ A p2R _ B p2(S \ R) _ A _ B
We say the two antecedent (top) clauses in (1) were resolved on p to produce the resolvent (bottom) clause. Two literals p2S and p2R clash if S 6= R. If R \ S is non-empty, we call the literal p2(R \ S) the residue, and otherwise we say that the clash is annihilating. A pair of clashing literals which are annihilating are inconsistent. (1)
Rule (1) is the basis of resolution proof systems for our three families, but we need two variants. In each case, a resolution derivation of clause C from a set of clauses is a sequence of clauses hC1; : : : ; Csi, where each Ci is either in or derived from two earlier clauses in by the resolution rule, and Cs = C. The length of the derivation is s. A refutation of is a derivation of the empty clause, denoted . A resolution rule is sound and refutation complete for a family of formulas if every formula in the family is unsatis able i it has a refutation using the rule.
Multi-Valued CNF: We obtain a sound and refutation-complete proof system
if we imbue rule (1) with implicit merging and annihilation [
Regular CNF: In this case, arbitrary literals on the same propositional symbol
cannot be merged because the result may not be regular. Hence, we allow
a clause to contain multiple literals on the same propositional symbol. The
following restricted signed resolution rule is sound and complete for regular
formulas over a lattice [
(p2"i _ A) (p2#j _ B) (A _ B) provided i 6 j: (2)
In the restriction for Regular formulas, and also in the case of Regular formulas with negation, there are no residuals: the clashing literals are always annihilated.
If is a set of clauses and L a set or sequence of literals, we may write ; L as an abbreviation for [ f(l) j l 2 Lg. We say literal p2S is at least as strong as p2R if S R, and stronger if S ( R. If p2S is at least as strong as p2R, then also (p2S) j= (p2R). 3
The ability of CDCL-R to e ciently simulate resolution proofs is closely tied to
a property of resolution refutations involving unit resolution. (See [
For a set or sequence of literals L, we denote by L the of literals which are the complements of literals in L. In particular, if C is a clause, then C the set of complements of literals in C. Thus, ; C `ur indicates, intuitively, that the restriction of obtained by setting all literals of C false can be refuted by unit propagation. For regular formulas, this operation is always de ned, since the complement of a regular literal need not be regular. For this case, we make use of the following sets. For each sequence L = l1; l2; : : : lk of literals, L denotes the set of sets of literals of the form C = (l10; l20; : : : lk0) where each li0 is inconsistent with li. In particular, for each clause C = (l1; l2; : : : lk), we denote by C the set of sequences of literals of the form L = l10; l20; : : : lk0 (except order does not matter) where each li0 is inconsistent with li.
and C a clause with j= C. For sets of MV-CNF or Reg-N-CNF formulas (those with complements) we say C is a-empowering for i C = (A _ a) and 1. ; C `ur , 2. ; A 6 `uurr ,
For Reg-CNF, which does not have complements, we say that C is a-empowering for i C = (A _ a) and 1. For some C0 2 C;,A0 ;6 C`ur0 `ur , 2. If A0 2 A then , 3. If A0 2 A, and b a literal inconsistent with a, then ; A0 6 `ur b. C is empowering for by otherwise.
if it is a-empowering, for some a 2 C, and is absorbed
Intuitively, a clause C is empowering for if ; C has a unit refutation, but ; A does not, where C = (A _ a). Notice that ; C is with one or more unit clauses added, in contrast to [ fCg, which is with one more clause.
clauses for which 6`ur , and a signed resolution refutation of . Then contains a clause that is empowering for .
Proof. The rst part may be expressed identically for formulas with or without complements. Let C be the rst clause in that does not satisfy condition 1 of De nition 1. Such a clause exists, because the su ces if no earlier clause does. C is the resolvent of two earlier clauses of , say C1 = (p2S1 _ A1), and C2 = (p2S2 _ A2), where p2S1 and p2S2 clash. We claim one of C1 or C2 is empowering for . Both are logically implied by , because they are in and signed resolution is sound. Both satisfy condition 1 of De nition 1, by choice of C.
We complete the argument for formulas with complements as follows. Both satisfy condition 2 of De nition 1, because C = (p2(S1 \ S2) _ A1 _ A2), so if ; A1 `ur or ; A2 `ur then ; C `ur , contradicting choice of C. Now, suppose both C1 and C2 fail condition 3 of De nition 1. That is, for some R1 S1 and R2 S2, we have ; A1 `ur (p2R1) and ; A2 `ur (p2R2). Resolving (p2R2) and (p2R1) produces a unit clause containing atom p2(R1 \ R2), which is at least as strong as p2(S1 \ S2). Then ; C `ur , again contradicting choice of C. So at least one of C1 or C2 is empowering for .
The completion for formulas without complements is the same, but messier: Both C1 and C2 satisfy condition 2, because C = (p2(S1 \ S2) _ A1 _ A2), so if ; A01 `ur for some A01 2 A1 or ; A02 `ur for some A02 2 A2, then ; C0 `ur for some C0 2 C, contradicting choice of C. Now, suppose both C1 and C2 fail condition 3. That is, for some A01 2 A1, A02 2 A2, R1 S1 and R2 S2, we have that ; A01 `ur (p2R1) and ; A02 `ur (p2R2). Resolving (p2R2) and (p2R1) produces a unit clause containing atom p2(R1 \ R2), which is at least as strong as p2(S1 \ S2). Then there is a C0 2 C with ; C0 `ur , again contradicting choice of C. So either C1 or C2 is empowering for . 4
The core of the CDCL algorithm can be viewed as a back-and-forth between two processes, one which guesses at partial assignments, and one which derives new clauses. We rst consider an algorithm, that we call Probe-and-Learn, which embodies a \single round" of this interaction. Describing the algorithm requires some terminology.
For multi-valued formulas, the guessing involves restrictions on assignments, rather than assignments. We will call such restrictions \decision sequences". De nition 1. A decision sequence for D and of distinct literals such that: is a sequence = ha1; a2; : : : asi
2. If ai is p2S, then S \ TfR j p2R = aj and j < ig 6= ;. (That is, each successive literal further restricts the possible assignments.) 3. The set of literals in is satis able.
For any non-empty decision sequence maximal proper pre x = hl1; : : : lk 1i. = hl1; : : : lk 1; lki, let denote the
Each decision sequence de nes a set of truth assignments, namely those consistent with each literal in the sequence. For any decision sequence and literal l, we say that makes l false if no assignment consistent with is consistent with l. makes l true if every assignment consistent with satis es l.
Unit propagation is a central feature in CDCL algorithms, and in particular of the \back-and-forth" process embodied in Probe-and-Learn. We will de ne unit propagation for multi-valued formulas, as used in our algorithm, in terms of decision sequences.
De nition 2 (UP( ; )) For any clause set and decision sequence for , we denote by UP( ; ) the decision sequence 0 de ned by the xpoint of the following operation:
If contains a clause C = (l _ B) where but neither makes l true or false, extend makes every literal of B false, with l.
Unit propagation corresponds to unit resolution, in a context where we are interested in collecting implied restrictions on truth assignments rather than derived clauses. In particular, UP( ; ) makes a clause of false if and only if [ `ur .
A second process, closely related to unit propagation, involves derivation of clauses called asserting clauses.
asserting clause for clause set and decision sequence i 1. ; C `ur , or in the case of Reg-CNF, for each A 2 C, ; A `ur ; 2. For each literal a 2 C, there is a literal at least as strong as a, s.t. ; `ur ; 3. For exactly one literal a 2 C, ; 6`ur , for any atom at least as strong as a.
C is a con ict clause for and if it satis es only the rst two conditions.
The Probe-and-Learn algorithm, is presented as Algorithm 1. It takes a clause set and decision sequence as an argument. If unit propagation from satis es , the procedure returns. If unit propagation from makes a clause of false, we call this a con ict. If necessary, the procedure extends (by unspeci ed means) until one of these cases holds. In the case of a con ict, the handlecon ict procedure is called. Handle-con ict returns an asserting clause and an appropriate pre x of . The newly derived clause C is constructed so that makes all literals but one false, so after adding it to , unit propagation will set at least one more literal and satisfy this clause. It is possible that further propagation happens, and a sequence of new clauses is derived and added to .
Algorithm 1: Probe And Learn
Input: Finite poset D, signed clause set and decision sequence .
Output: Clause set 0, and a decision sequence 0 12 whilea UmPin(im;al)e6jx=tensaionndof 62s.t. aeinthder ;U P`u(r ; d)oj= or ; `ur 3 ; C handle-con ict( ; ). ; 4 [ fCg ; 5 end 6 return ; ; ;
There is no restriction on the method by which handle-con ict can generate an asserting clause. For correctness of Probe-and-Learn, it is su cient that, whenever the call handle-con ict( ; ) returns 0; C, then 1. 0 is a proper pre x of ; 2. C is an asserting clause for 0; , as de ned in De nition 2, unless it is the empty clause. 3. if C is the empty clause, is empty.
For the p-simulation results of Section 6.1, handle-con ict() must run in polynomial time. For the concrete simulation bounds of Sections 5 and 6, it must run in linear time (as is the case in the standard implementations in SAT solvers.)
The standard \clause-learning schemes" used in CDCL SAT solvers involve a resolution derivation closely connected to the unit propagation sequence that establishes a con ict. A generalized version of this process can also be used in our multi-valued handle-con ict. In the following sub-section, we demonstrate the derivation of a particular one. (This one derives a clause analogous to the soballed \1UIP asserting clause", which is the basis of the asserting clause derived in most CDCL SAT solvers.) 4.1
We need to show that, whenever Algorithm 1 calls handle-con ict, an asserting clause exists and can be constructed e ciently. For the formula with complements, this is trivial: If is a minimal decision sequence with ; `ur , then , the set of complements of decision literals, is an asserting clause for S = h ; i. For the case of regular formulas, we give a concrete construction, upon which implementation of handle-con ict can be based. This construction is the generalization of the standard method used in most CDCL SAT solvers.
Consider a decision sequence . We may carry out unit propagation in from , incrementally constructing extensions of by appending literals that unit propagation sets. Each time we observe a clause C = (a_A) for which the current decision sequence makes every literal in A false but leaves a undetermined, we append a to the decision sequence and call C the \reason for a". A con ict is detected when a literal that is inconsistent with a is already in the decision sequence (in other words, C has been made false.) Let denote the resulting decision sequence, up to but not including the con icting literal. For each literal l in , de ne the decision level of l to be the size of the minimum pre x l of such that ; l `ur l. If l is in , then its decision level is its index in . If l is set by unit propagation from only its decision level is 0.
For signed formulas, when a con ict is detected, we must have a clause C = (A _ l), with l = p2S, in which all atoms are made false by the sequence l. This does not entail existence of a clause (B _ p2R), where R \ S = ;. The reason is that resolution steps need not be annihilating (there may be a residue of the clashing literals). If a clause C = (A_p2R_l), involved in unit propagation, is the reason for extending the decision sequence with l, then some set of previously derived unit clauses on the atom p annihilated p2R. It does imply that the collection of literals on propositional symbol p which appear on l eliminate all values in S as candidates for assignment to p. More precisely, among the literals in l is a sub-sequence of literals p = hp2R1; : : : p2Rri such that ([Ri) \ S = ;. Mark each literal, of each clause, involved in the unit propagation sequence, with this sequence of literals. We begin with a clause C0 = C, and generate a sequence of clauses Ci, by means of the following algorithm:
Algorithm 2: Signed-CNF 1UIP Clause Derivation 1 while C contains more than one literal with decision level j j do 2 p2S the last literal in which clashes with a literal in C; 3 p2R a literal of C marked with p2S; 4 A the reason for p2S; 5 C the resolvent of C and A; 6 end
Lemma 2. Each clause generated by Algorithm 2 is a con ict clause, and the clause returned by the algorithm is an asserting clause, according to De nition 2. Proof. Let C0; C1; : : : be the sequence of clauses derived by Algorithm 2. C0 is trivially a con ict clause. Assume that Ci = (p2S _ Bi) is a con ict clause, that p2R is the literal of Ci identi ed in line 3, and that A = (p2S _ Ai) is the reason for p2S being added to the assignment. Then Ci+1 = (p2(;SC0\`uRr) _ Bi _ Ai) is the resolvent of Ci and Ai. Clearly, for any C0 2 Ci+1, , because, intuitively, setting all literals of Ci+1 false makes A e ectively unit, thus setting p2R, after which we use the fact that Ci is a con ict clause. Since unit propagation from makes Ci false and makes A unit, it also makes Ci+1 false. Thus, Ci+1 is a con ict clause.
The clause returned by this algorithm is the analog of the 1UIP clause used in
standard CDCL-R solvers, and we believe is the same clause as generated by the
method in [
Proposition 1. Unit propagation and derivation of an asserting con ict clause can be carried out in time linear in j j.
Proposition 2. Let be a decision sequence for s.t.
ur [ ` . Then 1. Probe-and-Learn( ; ), using a poly-time handle-con ict, runs in time polynomial in j j.
Proof. Each iteration of the body of the loop performs unit propagation and executes handle-con ict, which performs the asserting clause derivation. On each iteration of the loop, except possibly the terminating iteration in the case that a satisfying assignment is found, is set to a proper pre x of its previous value. The maximum length of decision sequence is jDj j j. We assume D is xed, so the total time spent in the loop is O(j j (time for handle-con ict)). 5
Here, we show that, for any resolution refutation of MV-CNF or Reg-CNF formula , there is a sequence of calls to probe-and-learn which refutes in time polynomial in the combined size of and . We begin by showing that any empowering clause can be absorbed by a sequence of calls to probe-andlearn.
First, suppose that C = (A _ a) is an a-empowering clause for . Let be a decision sequence consisting of the literals of an element of A, in any order, f ollowed by a literal which is inconsistent with a. If handle-con ict() uses the DECISION learning scheme, then Probe-and-Learn( ; ) extends with at least one clause which is in , and thus it absorbs C.
When probe-and-learn does not use the DECISION learning scheme, it is a little more complicated, because the clauses derived might not include any literals based on atoms from C. However, with a suitable sequence of calls we can be sure to derive clauses which make C absorbed.
Lemma 3. Suppose C = (A_a) is a-empowering for . Then there is a sequence of calls to probe-and-learn which generate an extension 0 of such that C is absorbed by 0. Moreover, the total execution time for this sequence of calls is polynomial in the size of , provided the time for handle-con ict is also. Proof. Let be a decision sequence from A, followed by a literal which is inconsistent with a. Probe-and-learn must extend = 0 to a set 1 by adding at least one derived clause, which (because it is an asserting clause) has fewer literals than . As long as C remains empowering for i, we call probe-and-learn again as follows. On each repetition, since C is still a-helpful, no con ict is found until after a is asserted. It follows that each asserting clause derived has a di erent asserted atom, so the number of repetitions is bounded by the product of j j and jDj. Moreover, eventually a itself, or some atom stronger than a, will be the asserted atom, at which point C is no longer a-helpful. If C is still helpful, we repeat for each atom b for which C is still b-helpful, after which C is no longer helpful for . The entire sequence of calls requires time polynomial in j j.
To see that an appropriate sequence of calls to probe-and-learn can refute in time not much longer than the size of some given refutation, we identify a sequence of empowering clauses, and absorb each.
Lemma 4. Let be a set of signed clauses, and a resolution refutation of . Then, there is a sequence of calls to probe-and-learn, which refutes in time polynomial in the combined sizes of and , provided handle-con ict is polynomial time. j j.
Pforloloowf.s.WIfe gie`nurera,tewea asreeqduoennec.e Ot0h:e:r:wisse,ofletsuApebresetthseofrst,cwlaiutshe in0 = tha,t aiss empowering for i. By Lemma 3, there is a sequence of calls to probe-and-learn which generates a superset of i for which A is not empowering. Let this be i+1. The total execution time is polynomial at most j j times a polynomial in 6
The CDCL algorithm with restarts (CDCL-R) can be described in terms of a sequence of calls to Probe-And-Learn. This is illustrated by Algorithm 3.
Algorithm 3: Con ict-Directed Clause Learning with Restarts (CDCL-R) Input: nite poset D and nite set Output: SAT or UNSAT // Clause set, initialized to the input clauses. ; // Decision sequence, initialized to empty. ; of signed clauses for D. 4 5 6 7 8 9 10 11 end 1 2 hi 3 repeat
; Probe-and-Learn(D; ; ) ; if U P ( ) j= then
return SAT if = hi then
return UNSAT if Time to Restart then
hi
While many details have been abstracted away, Algorithm 3 is essentially the algorithm implemented by most CDCL-based solvers. It begins with the empty decision sequence. In the rst call to Probe-and-Learn, the decision sequence is extended until a clause is made false, after which clause learning and backjumping are carried out (by handle-con ict, in Probe-and-Learn). In subsequent executions of the loop body, the decision sequence resulting from the most recent handle-con ict is extended until either a satisfying assignment is produced, or Probe-and-learn again nds a con ict.
At this level of abstraction, the signed version and classical version are not distinguishable, except for the input parameter D. We make D argument to Probe-and-Learn to make explicit the fact that Probe-and-Learn (and, in particular, handle-con ict), must be appropriate to D and the class of formulas in question. Further, if D is of size 2, then with appropriate choice for Probe-andLearn, this algorithm is equivalent to the classical CDCL. Our algorithm does not allow for deletion of learned clauses, because the proof does not allow for this, but this can be trivially added.
Since CDCL-R can be viewed simply as a repeated application of Probe-andLearn, with possible restarts, it is straightforward to see that CDCL-R can be guided to refute a formula with a resolution refutation the size of . in time polynomial in
cision sequence for CDCL-R on input , is a nite sequence of symbols satisfying: 1. each symbol is either a literal of or the distinguished symbol R, (for \restart"), 2. each maximal sub-sequence without an R is a decision sequence for .
We may take two views on extended decision sequences. On one view, we may take it as a record or witness of an actual execution of CDCL-R. On the other, we may view it as a string to control an intended execution of CDCL-R. Lemma 5. If has a resolution refutation of size s, then there is an execution of CDCL-R on input which refutes in time polynomial in s. Proof. (Sketch) The only change to the strategy for repeated Probe-and-Learn given above is that, after each Probe-and-Learn call we restart, so that Probeand-Learn is always called with the empty decision sequence. Thus, instead of implementing the strategy for probes by setting the arguments to Probe-andLearn, we do it by having Probe-and-Learn select (on line 1) the decision sequence speci ed by the strategy. 6.1
Propositional proof complexity is the study of the relative power of proof systems
for propositional logic, measured by minimum length of proofs for tautological
formulas. The abstract de nition of propositional proof system introduced in the
seminal paper of Cook and Reckow [
is a set of strings L (the proofs) with a polytime function VL (a veri er for L) such that VL(x) = if x is an L-proof that is unsatis able, and VL(x) = ? otherwise.
Proof system A p-simulates proof system B if there exists a polynomial function poly(), such that for every unsatis able formula and every B-proof B of , there is an A-proof A of with j A j poly(j B j).
As a simplifying convention, we require that the minimum size of a proof of
is j j. This is not standard in proof complexity, but is necessary for relevance
to practical satis ability algorithms, and is followed also in, e.g., [
To view a satis ability algorithm as a proof system, we may take any trace of the algorithm on an unsatis able clause set as a proof of the unsatis ability of , provided that the trace re ects the running time of the algorithm, and that we can e ciently verify that the trace corresponds to an execution that reports \unsatis able". For present purposes, we may use extended decision sequences as CDCL-R proofs.
Theorem 1. CDCL-R for MV-CNF (resp. Reg-CNF), with polytime handlecon ict, p-simulates signed resolution for MV-CNF (resp. Reg-CNF). Proof. (Sketch) To show that CDCL-R p-simulates resolution, we show that for any resolution refutation of clause set , there is an extended decision sequence s.t., when CDCL-R is executed in accordance with on input , it runs in time polynomial in the length of , and reports UNSAT. This is given to us by Lemma 5.
To see this, it is enough to observe that signed formulas and resolution, when
jDj = 2, are equivalent to the classical case. We state this corollary to point out
that our result is indeed a generalization of that in [
Theorem 2. Signed resolution p-simulates CDCL-R for MV-CNF and RegCNF formulas, with 1UIP handle-con ict.
Proof. (Sketch) Consider an execution of CDCL-R that halts and outputs \UNSAT", and let the extended decision sequence corresponding to this execution. The size of is certainly polynomial in the length of execution. The set of clauses produced by handle-con ict, together with the input clauses, together with the clauses generated by unit propagation when unsatis ability is nally determined, constitute a resolution refutation. A symbol of is consumed for every clause produced by handle-con ict, so the set of learned clauses at the end is of size polynomial in the size of . The set of unit clauses derived by unit propagation at the end is certainly polynomial in the size of the set of learned clauses plus the input set. It follows that the entire refutation is of size polynomial in j j + j j. 7
We have presented a natural generalization of the SAT algorithm known as
CDCL with restarts to signed CNF formulas. Adapting the proofs from [