Towards a more efficient 3SAT Algorithm I
J. M. Robson
LaBRI

Dec 9, 2003


abstractWe present an algorithm for deciding 3SAT which incorporates some new ideas and has a run time bounded by O(1.516185n). While this is not yet competitive with the best known algorithms (O(1.481n)), it represents only a first step in exploiting these new methods and further reductions are certainly possible.
résumé Un nouvel algorithme de résolution de 3SAT est présenté utilisant de nouvelles idées et ayant un temps de calcul borné par O(1.516185n). Si ce temps reste supérieur à celui des meilleurs algorithmes connus (O(1.481n)), il n'est qu'une première étape dans l'exploitation de ces nouvelles méthodes et, sans doute, ce temps peut être réduit davantage.

1  Introduction

1.1  3SAT and its history

1.2  Other algorithms

1.3  A New Algorithm

2  Ideas and Notation

[`a] is the complement of the variable or literal a, [^a] is the variable occurring in the literal a and [a\tilde] is an occurrence of either a or [`a].

2.1  The Fibonacci algorithm

If every expression considered (except the original one at the root of the call tree) contained at least one 2-clause, say (a,b), there would be a simple algorithm with time bound proportional to fn; namely set a=true and solve; set a=false, b=true and solve. A simple argument shows that we can handle expressions without 2-clauses which arise so that this bound remains valid.

Suppose that in the computation for an original expression E, an expression E ¢ having no 2-clauses arises. E ¢ consists of a subset of the clauses of E and, by the logic of the algorithm, E ¢® E. But for any E ¢ which is a subset of the clauses of E, E ® E ¢, so we have E satisfiable if and only if E ¢ satisfiable. Hence we can drop all the other branches of the tree and only solve for E ¢.

A little care is needed to avoid a situation where we drop branches which have already been completely analysed, thereby not saving any time.

We will use variants of this argument in many places.

2.2  Branching

branching on a literal a   Two subproblems, one obtained by setting a=true and simplifying, the other obtained by setting a=false and simplifying.

branching on the equality of two literals a and b   Two subproblems, one obtained by setting a=b and simplifying, the other obtained by setting a=[`b] and simplifying.

2.3  Forced assignments

When branching on a literal a, in the a=true branch, we can assume that there is no satisfying assignment with a=false since such an assignment would be found in the a=false branch. Thus we can assume that some clause involving a would be false except for the assignment a=true, that is that the other literals in the clause are false. If there is a single 3-clause including a, say (a,x,y), that means we can set x=y=false; if there are two, say (a,v,w) and (a,x,y), we can add to the expression [`(v,w)] È[`(x,y)] or, to keep in CNF, ([`v],[`x]), ([`v],[`y]), ([`w],[`x]) and ([`w],[`y]).

More generally:
If one branch contains no new 2-clauses, we can prune the other branch; we call this the case of a subexpression. If one branch contains a unique new 2-clause say (x,y), we can set x=y=false in the other branch. If one branch contains exactly two new 2-clauses say (v,w) and (x,y), we can add the 2-clauses ([`v],[`x]), ([`v],[`y]), ([`w],[`x]) and ([`w],[`y]) in the other branch.

2.4  2-clauses

The graphs G0 and G1. Both have vertices corresponding to the variables of the expression and edges corresponding to (some) 2-clauses. G0 has edges for every 2-clause; G1 is a subgraph of G0 with maximum degree 1. We will sometimes refer to edges present in G1 as marked edges.

3  The Algorithm

3.1  Simplifications

Various simplifications are applied whenever possible before the main recursive algorithm is applied to an expression. A simplification is called strong if it reduces the number of variables and weak otherwise.

Strong simplifications  

Weak simplifications  

3.2  Choice of where to branch

A summit of maximum degree in G0, that is a variable with the maximum number of occurrences in 2-clauses.

4  Analysis

4.1  Claimed behaviour

Consider an expression containing n variables with m edges in its graph G1. We claim that the number of leaves in its computation tree is at most
an bm × ì
ï
ï
ï
ï
ï
ï
í
ï
ï
ï
ï
ï
ï
î
c¨ if G0 has clauses (a,b), (b,c), (c,d), (d,a)
c3 if G0 has a vertex of degree  ³  3
c± if the expression has two 2-clauses (a,b), (
-
a
 
,c)
c2 if G0 has a vertex of degree  ³  2
c1 if G0 has exactly one edge
c0 if G0 has no edges
1 otherwise

where a = 1.516185, b = (a-1+a-2)-1/2 ( » 0.958790), c0=2a-1b3 ( » 1.162648), c2=b3 ( » 0.881395), c1=b2(1/a+1/a2) ( » 1.032262), c±=a-2(1+b) ( » 0.852086), c3=2a-2b ( » 0.834159), c3=a-1+a-4 ( » 0.848780). We will establish this by induction on n. We will write f(n,m) for an bm.

4.2  degree 0

Choose an arbitrary variable a and branch on it. In all cases we take a=true forced in the a=true branch. W.l.o.g. suppose a has no more positive occurrences than negative. Consider this number of positive occurrences which must be at least two or a simplification would introduce a 2-clause.

4.2.1  two occurrences

Say (a,v,w), (a,x,y). In the a=true branch we add ([`v],[`x]), ([`v],[`y]), ([`w],[`x]) and ([`w],[`y]). Unless there is then a strong simplification (for instance because v=x), two of these edges can be marked and we obtain a G0 with a square. In the a=false branch we have two marked edges or a vertex of degree 2 in G0 or a strong simplification. The conclusion follows since:
a-1(b2c¨+b2) £ c0

4.2.2  at least three occurrences

There are two subproblems each with one less variable and at least three edges in G0. Condition:
2a-1b3 = c0

4.3  degree 1

We choose a 2-clause, say (a,b). The analysis depends on the number of occurrences of [`a]. There must be at least one such occurrence or a simplification would be applicable.

4.3.1  Special case: (a,b) the only 2-clause and exactly one clause ([`a],[`b],c)

We branch on a considering the number of occurrences of the literals a, b, [`a] and [`b].

some literal has only one occurrence   We can apply a simplification which will take us out of this special case.

some literal has only two occurrences   If it is a or b, suppose wlog that it is (a,x,y). We can add clauses ([`a],[`b],[`x]) and ([`a],[`b],[`y]) which will take us out of this special case.
Otherwise suppose wlog that it is ([`a],x,y). Unless one of x and y is c[\tilde], we add ([`c],[`x]) and ([`c],[`y]) in the a=false, b=true branch giving at least one marked edge and a vertex of degree two; in the a=true branch we have at least the two 2-clauses ([`b],c) and (x,y).
a-1b+ a-2 c2 £ c1

all literals have at least 3 occurrences   We have the clauses (a,b), ([`a],[`b],c), ([`a],d,e), ([`a],f,g), (a,h,i), (a,j,k), ([`b],l,m), ([`b],n,o). In the branch a=true we have three 2-clauses (d,e), (f,g), ([`b],c). In the branch a=false, b=true, we have (h,i), (j,k), (l,m), (n,o). (We cannot have killed one of these clauses because for instance h is b or l is [`a] because of applicable simplifications and our exclusion of multiple ([`a],[`b],c) clauses.) If {(h,i),(j,k)}={(l,m),(n,o)} we can simply set a=[`b]. Otherwise we have three 2-clauses.
a-1b2+a-2b2 = c1

4.3.2  Other cases of a clause ([`a],[`b],c)

If there is a clause ([`a],[`b],c) and either the clause (a,b) is not the only 2-clause or there are two or more clauses ([`a],[`b],ci), branch on a=b. In the a=b branch we necessarily have a=b=true and then c=true (or ci=true for all ci).

two or more clauses ([`a],[`b],ci)   The a=b=true, ci=true branch has removed r ³ 4 variables and at most r-1 marked edges (and either there is at least one new 2-clause or we have a subexpression); the a ¹ b branch has removed one variable and one possibly marked edge and may have left an expression with one or no 2-clauses; but there will be an expression with no 2-clauses only if both the first branch had at least three new 2-clauses (since otherwise some new 2-clauses can be added) and (a,b) was the only 2-clause (since otherwise another 2-clause will have survived).


a-4+a-1b-1c0 £ c1

a-4b-2+a-1b-1c1 £ 1 £ c1

only the clause ([`a],[`b],c) but at least 2 2-clauses   The a=b branch now has r=3; the a ¹ b branch cannot leave an expression with no 2-clauses because any 2-clauses other than (a,b) survive.
a-3b-1+a-1b-1c1 £ 1 £ c1

4.3.3  two occurrences of [`a]

Say the occurrences are ([`a],c,d) and ([`a],e,f). We branch on a with [`a] forced in the a=false branch. The cases where [^b], [^c], [^d], [^e], [^f] are not distinct variables are easily dealt with. Otherwise we consider whether there is already a 2-clause involving [^c], [^d], [^e] or [^f].

No such 2-clause   In the a=true branch, we lose a variable [^a] and at most one marked edge but we gain two edges (c,d) and (e,f) which can both be marked. In the a=false,  b=true branch, we lose two variables ([^a], [^b]) and at most one marked edge but we gain four edges ([`c],[`e]), ([`c],[`f]), ([`d],[`e]) and ([`d],[`f]), of which two can be marked and we are left with a square in G0.
a-1b+ a-2bc¨ £ 1

Some such clause   Note that the clause cannot be of a form such as (c,d) because then, a simplification would occur. In the a=true (resp. a=false forced) branch, we lose one (resp.two) variable(s) and at most one marked edge but we are left in each branch with a vertex of degree at least two in G0.
(a-1 +a-2)b-1c2 = 1 £ c1

4.3.4  three or more occurrences of [`a]

We may assume that there are also at least three occurrences of [`b] since otherwise we could apply the above arguments with b instead of a. In the a=true (resp. a=false) branch, we lose one (resp.two) variable(s) and at most one marked edge but we gain three or more edges so that either we gain three marked edges or we have a vertex of degree two or more in G0. (The fact that the occurrences of [`b] produce new 2-clauses in the a=false, b=true branch depends on the fact that there were no clauses ([`a], [`b],c).)
(a-1 +a-2)b2 = 1 £ c1

4.4  degree 2; same sign

Say the two edges are (a,b) and (a,c) and note that there can be at most two marked edges involving [^a], [^b] and [^c].

4.4.1  One occurrence of [`a]

If [`a] has exactly one occurrence, say ([`a],d,e), as in the degree 1 case we can add (a,[`d]) and (a,[`e]). This has taken us into the degree greater than 2 case except when {b,c}={[`d],[`e]}. The action here depends whether [^b] and [^c] both have degree 1 in G0 or not.

both have degree 1   Note that the clause ([`a],[`b],[`c]) cannot be the only occurrence of [`b] or for the same reasons as above, the clause (b,c) could be added taking us into the next paragraph. Branch on b. In the b=true branch, we have (a,c) and ([`a],[`c]) so we can simplify by a=[`c]; we have removed two variables and at most one marked edge and there is a new 2-clause arising from another occurrence of [`b]. In the b=false branch, we must have a=true; we have removed two variables and at most one marked edge but there must be at least two edges added to G0 or there would be either a subexpression (no edges added) or a drastic improvement in the b=true branch (2-clause (x,y) added in b=false, x=y=false in b=true).
a-2(c1+b) £ c2

otherwise   Suppose it is [^b] that has degree 2. If the other 2-clause involving [^b] is not (b,c), we can take b instead of a and this takes us into a different section. If we do have (a,b), (a,c), (b,c), ([`a],[`b],[`c]), we branch with either a=true, b=[`c] or a=false, b=c=true.
a-2b-1c0 + a-3 £ c2

4.4.2  Two occurrences of [`a]

If [`a] has two occurrences we use exactly the same analysis as in Section 4.3.3 except that in the a=false branch we now also have c=true but possibly one more marked edge removed.
a-1b+ a-3 c¨ £ c2

a-1b-1 +a-3b-2c2 £ c2

4.4.3  More than two occurrences of [`a]

Otherwise we branch on a. In the a=false branch, we have b=c=true; we consider the number of new 2-clauses introduced by this partial assignment (which has left us a new expression E¢).

no new 2-clauses   E¢ is a subexpression of E and E¢ is satisfiable if and only if E is. So we simplify E to E¢.

one new 2-clause   By the reasoning of Section 2.3 we can add [`x] and [`y] to the expression in the a=true branch and simplify.

two new 2-clauses   In the a=true branch we lose one variable and at most one marked edge but we gain at least three new edges from the occurrences of [`a]. Hence we gain either three new marked edges or a vertex of degree two or more in G0. In the a=false branch we lose three variables and at most two marked edges but we gain two new edges. Hence we gain either two new marked edges or a vertex of degree two or more in G0. If the two new edges added in the second branch were (v,w), (x,y), we add the square ([`v],[`x]), ([`v],[`y]), ([`w],[`x]), ([`w],[`y]) in the first.
a-1b2c¨ + a-3 £ c2

at least three new 2-clauses  

In the a=false branch we now gain at least three new edges. Hence we gain either three new marked edges or a vertex of degree two or more in G0.
a-1b2 + a-3b £ c2

4.5  degree 2; different sign

Say we have (a,b),  ([`a],c). We branch on a. We lose two variables in each branch and at most one marked edge in one branch and two in the other. By the reasoning of Section 2.3 we can assume there are at least two new 2-clauses in each branch.
a-2(1+b) £ c±

4.6  degree 3 and more

Say we have (a,b), (a,c), (a,d). (cases with degree more than three or occurrences of both a and [`a] are easily handled) Branch on a giving subexpressions with one and four variables and at most one and three marked edges respectively removed. If the a=false, b=c=d=true branch has less than three new 2-clauses, we can improve the a=true branch which dominates the time, so we assume the contrary. The a=true branch has at least one new 2-clause or it would be a subexpression.
a-1+a-4 £ c3

4.7  A square in G0

In this case, which arises frequently when one branch has two new 2-clauses, we have two subproblems, one with a=c=true and the other with b=d=true, so provided we can deal with all cases where one branch has less than three new 2-clauses, we hope to have?
c¨=2a-2b

4.7.1  one new 2-clause

Say we had ([`a],e,f). The b=d=false (forced) branch now has e=f=false and e and f cannot be b or d or a simplification would be applicable. In each branch the number of marked edges removed is at most the number of variables removed and at least one new 2-clause has been added (or we have a subexpression).
(a-2b-1+ a-4b-3)c1 £ c¨

4.7.2  two new clauses

A new 2-clause when b=d=true cannot be ([`a],[`c]) or the a=c=true branch would have b=true or d=true. So in this branch we can add the 2-clause ([`a],[`c]). Moreover, if the new clauses when b=d=true are (p,q), (r,s), we can add ([`p],[`r]), ([`r],[`q]), ([`q],[`s]) and ([`s],[`p]) in the a=c=true branch. The only cases where this does not add at least one new 2-clause are those where all four of these clauses are already known to be true when a=c=true; now if, for instance, the clauses (p,q), (r,s) arose from 3-clauses ([`b],p,q), ([`d],r,s), we conclude that b=false or d=false when a=c=true and we add the clause ([`b],[`d]) in the a=c=true branch.
2a-2b = c¨

5  Where next?

5.1  Taking account of more edges

A simple next step would be to distinguish between the case of one or two vertices of degree 2 on the one hand and three or more on the other hand. Most cases where we know that there is a vertex of degree 2 in fact are ones where there are at least three (typically we have added three 2-clauses and the worst case is that either all are isolated edges (b3) or all have at least one degree 2 vertex (c2); separating out these cases would exclude many possibilities of recursive calls having maximum degree 1. We would then only need to insist that this new c23 be at most b3.

Allow degree up to two in G1 which would be renamed G2. Give each variable vi a weight wi according to its degree in G2: 1 if degree 0, b11/2 if degree 1 and (b1b2)1/2 if degree 2. Prove time for an expression:
  £ an
Õ
variables vi 
wi× ì
ï
ï
í
ï
ï
î
c3 if G0 has a vertex of  degree  ³  3 else
c2 if G0 has a vertex of  degree  ³  2
c0 if G0 has no edges
1 otherwise




File translated from TEX by TTH, version 3.05.
On 9 Dec 2003, 11:53.