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
- Pure literals: if there is a clause (a), set a=true.
- two 2-clauses with the same pair of variables: if there are two 2-clauses
(a,b) and (a,[`b]), set a=true; if there are (a,b)
and ([`a],[`b]), set
a=[`b].
- a literal with no occurrences: if there is no clause involving a literal
a, set a=false.
- empty clause: if there is an empty clause, return false
Weak simplifications
- duplicate clauses: if two clauses are identical (up to permutation
of literals) delete one of them.
- two occurrences of a variable in a clause: if a clause contains the
same literal twice, delete one occurrence; if a clause contains a and [`a], delete the clause.
- one clause a subclause of another: if there are two clauses (a,b)
and (a,b,c), delete the (a,b,c).
- one 3-clause a direct consequence of another 3-clause and a 2-clause:
if there are three clauses ([`a],b) (equivalent
to aÞ b), (a,c,d) and (b,c,d), delete (b,c,d).
- a new 2-clause a direct consequence of a 3-clause and another 2-clause:
if there are two clauses (a,b) (equivalent to [`a]Þ b) and ([`a],b,c),
add the implied 2-clause (b,c) unless it is already present.
- unique occurrence: if a clause (a,b,c) is the sole occurrence of (the
literal) a, add the clauses ([`a],[`b]) and ([`a],[`c]) unless they are already present. That is we decide
that we will only have a=true if we are forced to because b=c=false.
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 |
|
|
|
|
|
|
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:
4.2.2 at least three occurrences
There are two subproblems each with one less variable and at least three
edges in G0. Condition:
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).
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.
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).
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.
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.
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.
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).)
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).
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.
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.
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.
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.
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.
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.
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?
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).
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.
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 |
|
|
|
|
|
|
File translated from TEX by
TTH,
version 3.05.
On 9 Dec 2003, 11:53.