New Worst-Case Upper Bounds for SAT.
In 1980 Monien and Speckenmeyer proved that satisfiability of a propositional formula consisting of i>K clauses (of arbitrary length) can be checked in time of the order 2i>K / 3. Recently Kullmann and Luckhardt proved the worst-case upper bound 2i>L / 9, where i>L is the length of the input formula. The algorithms leading to these bounds are based on the i>splitting method, which goes back to the DavisPutnam procedure. i>Transformation rules (pure literal elimination, unit propagation, etc.) constitute a substantial part of this method. In this paper we present a new transformation rule and two algorithms using this rule. We prove that these algorithms have the worst-case upper bounds 20. 30897 i>K and 20. 10299 i>L, respectively.
Introduction
.
SAT (the problem of satisability of a propositional formula in conjunctive normal
can be easily solved in time of the order 2 N , where N is the number of variables in the
input formula. In the early 1980s this trivial bound was reduced for formulas in 3-CNF by
Monien and Speckenmeyer [20] (see also [22]) and independently by Dantsin [1] (see also
[4] and [2]). After that, many upper bounds for SAT and its subproblems were obtained
[21, 17, 25, 13, 14, 26, 16, 8, 23, 24]. Most authors consider bounds w.r.t. three main
parameters: the length L of the input formula, the number K of its clauses and the number
N of the variables occurring in it. Before the conference proceedings version of this paper
[9], the best known worst-case upper bounds for SAT were:
p(L)2 L=9 [16],
p(L)2 K=3 [21] (see also [16]),
where p is a polynomial. Also, the upper bound p(L)2 L=4 for satisability problem for general
Boolean formulas (i.e., not necessarily in CNF) is known [28]. Recently Paturi, Pudlak, Saks
and Zane [24] proved that 3-SAT is checkable in the randomized time O(2 0:446N ), but it is still
Some of the work described in this paper was presented at the 9th ACM-SIAM Symposium on Discrete
Algorithms (SODA'98) [9].
y Steklov Institute of Mathematics at St.Petersburg, 27 Fontanka, 191011 St.Petersburg, Russia.
Email: hirsch@pdmi.ras.ru, URL: http://logic.pdmi.ras.ru/~hirsch/index.html. Supported in
part by grants from INTAS and RFBR.
unknown whether the trivial upper bound 2 N for the general SAT problem can be improved.
Kullmann and Luckhardt in [16] simplied the algorithm of Monien and Speckenmeyer from
[21] and presented also an improved algorithm of the same complexity p(L)2 K=3 which works
better when the ratio of the number of clauses to the number of variables is greater than
2:64557. In the conference proceedings version of this paper [9] we presented two algorithms
which improve the bounds p(L)2 to
p(L)2 0:30897K and p(L)2 0:10537L respectively. In this journal version we improve the second
algorithm and prove the worst-case upper bound p(L)2 0:10299L . Our new algorithm uses the
p(L)2 0:30897K -time algorithm as a subroutine; the proof of the corresponding upper bound is
much simpler than the proof in the conference proceedings version [9].
The most popular methods for solving SAT are the local search method and the splitting
method . Many experimental and average-case results show the signicant power of the local
search method (for references, see the survey [7]). However, most best known worst-case
upper bounds for SAT and its NP-complete subproblems are obtained using the splitting
method [21, 16, 8] (for worst-case upper bounds for the local search method see [10, 11,
12]). The splitting method is also useful in proving worst-case upper bounds for exact and
approximate MAXSAT solving [18, 3, 19].
The splitting method goes back to the Davis{Putnam procedure [6]. Let l be a literal
occurring in a formula F . Let F [l] be the formula obtained from F by assigning the value
T rue to the literal l, i.e. by removing all clauses containing l and deleting all occurrences of
l from the other clauses. In short, the main idea of the Davis{Putnam procedure is that F is
satisable i at least one of the formulas F [l] and F [ l ] is satisable. In a wider sense [5], a
splitting algorithm constructs a tree by reducing satisability of a formula F to satisability
of several formulas F [I 1 ]; F [I obtained from F by assignments I 1 ; I
spectively. Then, a splitting algorithm simplies each of the formulas F [I 1 ]; F [I
according to transformation rules which do not change their satisability. These transformations
take a polynomial time. Their role is to reduce some of the parameters L, K or
N of the formulas F [I 1 ]; F [I and to simplify these formulas by eliminating pure
literals (a literal is pure if its negation does not occur in the formula), 1-clauses (1-clause is
a clause consisting of one literal) and other \easy pieces".
Recurrent equations are often used in complexity analysis of algorithms. Kullmann and
Luckhardt in [16] described a very similar, but simpler technique which is very useful in the
estimation of the running time of splitting algorithms. One can consider an execution of
a splitting algorithm as a branching tree, i.e. a tree such that formulas labelling children
are simpler than formulas labelling parents (leaves are labelled with the simplest formulas).
With each node of this tree we associate a branching vector of non-negative numbers and
a polynomial constructed from this vector. One can estimate the number of leaves in the
tree using the largest of the positive roots of these polynomials. Precise denitions and
formulations are given in Sect. 3.
Transformation rules play an important role in splitting algorithms. Two simplest rules
were proposed in the original paper of Davis and Putnam [6]: we can eliminate pure literals
and 1-clauses. All transformation rules we use are described in Sect. 4. This paper introduces
a new transformation rule which goes up to the following simple observation: if each clause
of our formula contains at least one negative literal, then this formula is trivially satisable
by the assignment in which all variables have the value F alse. Let P (l; F ) be a property of
a literal and a formula, for example, \F contains exactly two occurrences of l and at least
three occurrences of l ". In addition, we suppose that for each variable v in the formula F
at most one of the literals v and v satises P . Given F , the literals that satisfy the property
P will be referred as P -literals.
The black and white literals principle. Let F be a formula in CNF. At least
one of the following two alternatives holds.
(1) There is a clause in F that contains a P -literal and does not contain the
negations of any other P -literals.
(2) Satisability of F is equivalent to satisability of the formula obtained
from F by removing all clauses containing the negations of P -literals.
A formal proof of the black and white literals principle is given in Lemma 4.3. Figure 1
illustrates this principle. White circles (-) denote P -literals, black circles () denote their
negations, circles with dots (-) denote other literals (i.e., literals which are neither P -literals
nor the negations of P -literals; note that the negation of such literal is again neither P -literal
nor the negation of a P -literal). Columns correspond to clauses of the formula. The gure
contains two formulas, the rst one satises the condition (1), the second one satises the
condition (2).
(1)
| {z }
(2)
@
@
@
@
@

Figure

1: Two alternatives of the black and white literals principle.
This principle is the key point of our algorithm corresponding to the upper bound p(L)2 0:30897K :
In this algorithm we use the presence of clauses that contain a P -literal and do not contain
the negations of other P -literals for a certain property P . The black and white literals principle
is a kind of insurance: it guarantees that if we cannot nd a required clause, then we
can replace F by a simpler formula, or F does not contain any P -literals at all. This principle
is one of re-formulations of the following simple property: for any partial assignment A
(i.e., a set of literals which does not contain simultaneously x and x for any variable x) for
a formula F in CNF, either there is a clause in F containing only literals from A, or setting
the values of all these literals to F alse does not change the satisability of F .
Another known re-formulations of this property are the generalized sign principle [16] and
the autarkness principle [20, 22, 17] (see also [16]). A comprehensive study of the autarkness
principle can be found in [15].
The use of the black and white literals principle leads to two new bounds for SAT presented
in this paper and also to several upper bounds for the satisability problem for
formulas in CNF{(1,1) [8] (a formula is in CNF{(1,1) if each literal occurs in it positively
at most once; the satisability problem for these formulas is NP-complete).
In Sect. 2 we give basic denitions. Section 3 contains the technique that allows us to
estimate the size of a branching tree. In Sect. 4 we explain transformation rules that we
use in our algorithms. In Sect. 5 and Sect. 6 we describe the algorithms having the upper
bounds p(L)2 0:30897K and p(L)2 0:10299L respectively, and the corresponding proofs.
2 Basic denitions.
Let V be a set of Boolean variables. The negation of a variable v is denoted by v. Given a
set U , we denote Ug. Literals are the members of the set Positive
literals are the members of the set V . Negative literals are their negations. If w denotes
a negative literal v, then w denotes the variable v. A clause is a nite set of literals that
does not contain simultaneously any variable together with its negation. The empty clause
is interpreted as F alse. A formula in CNF (CNF-formula) is a nite set of clauses. The
empty formula is interpreted as T rue. The length of a clause is its cardinality, the length of
a formula is the sum of the lengths of all its clauses. The length of a clause C is denoted by
jCj. A k-clause is a clause of the length k. A k + -clause is a clause of the length at least k.
A k -clause is a clause of the length at most k. If we say that a literal v occurs in a clause
or in a formula, we mean that this clause or this formula contains the literal v. However, if
we say that a variable v occurs in a clause or in a formula, we mean that this clause or this
formula contains the literal v, or it contains the literal v.
An assignment is a nite subset of W that does not contain any variable together with
its negation. Informally speaking, if an assignment I contains a literal w, it means that w
has the value T rue in I. To obtain F [I] from F and an assignment I
remove from F all clauses containing the literals w i ,
delete all occurrences of the literals w i from the other clauses.
For short, we write F [w
An assignment I is satisfying for a formula F if F [I] is the empty formula. A formula is
satisable if there exists a satisfying assignment for it. We say that two formulas F and G
are equi-satisable if both are satisable, or both are unsatisable.
Let w be a literal occurring in a formula F . This literal is a i-literal if F contains exactly
i occurrences of w. It is a (i;j)-literal if F contains exactly i occurrences of w and exactly j
occurrences of w. It is a (i;j + )-literal if F contains exactly i occurrences of w and at least j
occurrences of w. It is a (i;j )-literal if F contains exactly i occurrences of w and at most
occurrences of w. Similarly, we dene (i
We denote the number of occurrences of a literal w in a formula F by #w
the sum of the lengths of the clauses containing w by }w When the meaning of F is
clear from the context, we omit F . A literal w is a }i-literal if Similarly, we dene
3 Estimation of the size of a branching tree.
Kullmann and Luckhardt introduced in [16] a notion of a branching tree. It is intended for
estimating the time complexity of splitting algorithms, since a tree of formulas which such an
algorithm splits, is a branching tree. One can consider an execution of a splitting algorithm
as a tree whose nodes are labelled with CNF-formulas such that if some node is labelled with
a CNF-formula F , then its sons are labelled with (simplied) formulas F [I 1 ]; F [I 2 ];
for some assignments I
Suppose we have a tree whose nodes are labelled with formulas in CNF. To each formula
F we attach a non-negative integer The tree is a branching tree if,
for each node, the complexity of the formula labelling this node is strictly greater than the
complexity of each of the formulas labelling its sons. In this paper we use
is the number of variables in F ;
is the number of clauses in F ;
is the length of F .
We prove two upper bounds, w.r.t. K and w.r.t. L. However, in this section we do not x
any concrete measure of complexity.
Let us consider a node in our tree labelled with a formula F 0 . Suppose its sons are labelled
with formulas F 1 , F 2 , . , Fm . A branching vector of a node is an m-tuple
are positive numbers not exceeding The characteristic polynomial of
a branching vector ~ t is dened by
The characteristic polynomial h ~ t (x) is a monotone function of x on the interval (0; +1),
and h ~ t exactly one positive root. We denote
this root by ( ~ t ) and call it the branching number . We suppose leaves. We
omit one pair of parentheses and write
Example 3.1 For example,
0:69424::: is the golden ratio;
The branching number of a tree T is the largest of the branching numbers ( ~ t ) of its
nodes. We denote it by  max;T . The following lemma proved by Kullmann and Luckhardt
allows us to estimate the number of leaves in a branching tree using its branching number.
Lemma 3.1 (Kullmann, Luckhardt, [16]) Let T be a branching tree, let its root be labelled
with a formula F 0 . Then the number of leaves in T does not exceed ( max;T
This lemma already allows us to estimate the running time of a splitting algorithm
if we know the branching number of the splitting tree and the algorithm processes each
its leaf in a polynomial time. However, our algorithm corresponding to the upper bound
calls the algorithm corresponding to the upper bound p(L)(6; 7; 6; 7) K
as a subroutine and thus processes some of the leaves in an exponential time. To estimate
the overall running time, we use the following simple generalization of Lemma 3.1.
Lemma 3.2 [8] Let T be a branching tree, let its root be labelled with a formula F 0 . Let G l
denote the object labelling a leaf l of the tree T . Let
l is a leaf of T
Proof is the induction on the construction of the tree.
Base. The tree consisting of the unique node. In this case
Step. Consider the tree T presented in Fig. 2. Let ~ be the branching tuple
in its root.
l is a leaf of T
s
l is a leaf of T j
f((G l ))A
s
s
(by denition of the tuple ~ t)

Figure

2: A splitting tree
s
s
(by denition of h ~ t )
(max(;  max;T (by monotonicity of h ~ t )
ut
Now if we know the branching number of the tree corresponding to a splitting algorithm,
then we can estimate its running time. We explicitly require our algorithms to perform
splittings with branching numbers not greater than we wish (and we only need to prove that
there always exists a splitting satisfying this condition). For this purpose, the algorithm has
to compare branching numbers corresponding to dierent vectors. Of course, this can be
done just by the examination of a constant number of cases and the use of the monotonicity
of  . However, a more general statement holds.
Lemma 3.3 (Kullmann, Luckhardt, [16]) Let m, k be natural constants, x 1
positive rational numbers. The problem whether
than (y 1 ;y solvable in time polynomial of max(x 1 ;x
In the following, when estimating the running time of our algorithms, we use frequently
inequalities like (7; 15) < (5; 17) or (5; 17) < (6; 7; 6; 7) 1=3 without proofs. One can check
these inequalities by approximate calculation of the branching numbers. However, there are
several simple observations that may help to prove some of this inequalities easier.
Lemma 3.4 (Kullmann, Luckhardt, [16])
(1) Permutations of the components of a branching vector do not aect the corresponding
branching number.
(2) The branching number strictly decreases as one or more components of the branching
vector increase.
4 Transformation rules.
In this section F denotes a formula in CNF.
Lemmas 3.1 and 3.2 allows us to take into consideration only the dierences between
the complexity of an input formula and the complexities of the formulas obtained from it
by splitting. The higher these dierences are, the smaller the number of leaves is. Thus,
to obtain a good algorithm, we should reduce as much as possible the complexities of the
formulas obtained by splitting. Here we explain transformation rules that allow us to do it.
More precisely, we explain that in certain cases we can nd a simpler formula equi-satisable
with F . In the following we use these rules so that they never increase the parameter under
consideration (the number of clauses in a formula or the length of a formula).
Elimination of 1-clauses. If F contains a 1-clause fag, then the formulas F and F [a] are
equi-satisable since all assignments that contain a are unsatisfying.
Subsumption. If F contains two clauses C and D such that C  D, then F and F nfDg are
equi-satisable since each assignment that satises the clause C, satises also the clause D.
Resolution with subsumption. Suppose we are given a literal a and clauses C and D
such that a is the only literal satisfying both conditions a 2 C and a 2 D. In this case, the
clause (C [ D) n fa; ag is called the resolvent by the literal a of the clauses C and D. We
denote it by R(C; D).
Let now F contain such clauses C and D. It is clear that adding R(C; D) to the formula
does not change its satisability. However, it increases its size. To avoid this eect, we
use this rule only if R(C; D)  D. In this case we reduce the satisability problem for the
formula F to the satisability problem for D)g.
Elimination of a variable by resolution. Given a literal a, we construct the formula
DP a
adding to F all resolvents by a;
removing from F all clauses containing a or a.
Lemma 4.1 (Davis, Putnam, [6]) The formulas F and DP a are equi-satisable.
This transformation can increase the size of a formula or/and the number of clauses in
it, but we use this rule only if it does not increase the parameter under consideration (the
number of clauses in a formula or the length of a formula). Note that in particular, this
transformation does not increase any of the parameters of F if a is a pure literal, and thus
it eliminates pure literals.
Elimination of blocked clauses. The clause C is blocked for a literal a w.r.t. F if C
contains the literal a, and the literal a occurs only in the clauses of F that contain the
negation of at least one of the literals occurring in C n fag. (Note that F may or may not
contain C.) In other words, there are no resolvents by a of the clause C and any other
clause of the formula F . For a CNF-formula F and a literal a occurring in it, we dene the
assignment
ag j the clause fa; xg is blocked for a w.r.t. Fg:
When the meaning of F is clear from the context, we omit F and write I(a).
The notion of a blocked clause was introduced and investigated by Kullmann in [13, 14].
We use the following two facts about blocked clauses.
Lemma 4.2 (Kullmann, [13, 14])
(1) If a clause C is blocked for a literal a w.r.t. F , then F , F n fCg and F [ fCg are
equi-satisable.
(2) Given a literal a, the formula F is satisable i at least one of the formulas F [a]
and F [I(a)] is satisable.
Application of the black and white literals principle. Let P be a binary relation
between literals and formulas in CNF, such that for a variable v and a formula F , at most
one of P (v; F ) and P (v; F ) holds.
Lemma 4.3 Suppose that each clause of F that contains a literal w satisfying P (w; F )
contains also at least one literal b satisfying P (b; F ). Then F and F [fl j P (l; F )g] are equi-
Proof. This is a particular case of the autarkness principle [20, 22, 17, 16]. We denote
Suppose G is satisable. Consider a satisfying assignment I for the
formula G. It is clear that the assignment I [ . On the other hand,
each assignment satisfying F satises also G. ut
5 A bound w.r.t. the number of clauses.
In this section we present Algorithm 5.1 which checks satisability of formula F in the time
is a polynomial). This algorithm has two subroutines, Function
REDUCEK and Function SPLITK . Function REDUCEK simplies the input formula
using the transformation rules (see Sect. 4). Function SPLITK is intended for reducing the
satisability problem for the input formula to the satisability problem for several simpler
formulas. The execution of this algorithm can be viewed as follows: Function REDUCEK
simplies the input formula, then SPLITK splits it into several formulas, REDUCEK sim-
plies each of these, and so on.
In the following, we denote by REDUCEK the formula that Function REDUCEK
outputs on input F . Similarly we dene SPLITK
Function REDUCEK .
Input: A formula F in CNF.
Output: A (simplied) formula in CNF.
Method.
(KR1) Elimination of 1-clauses. If F contains a 1-clause
Repeat this step while F contains 1-clauses.
(KR2) Application of the black and white literals principle. If each clause C in F
that contains a (2;3 contains also a (3
F := F [fa j a is a (3
Elimination of a variable by resolution. Choose a literal a such that a or a
occurs in F and maximal. If there are several such
literals, then choose a literal with # a minimal. If   0, then F := DP a
Repeat this step while F satises this condition.
If F has been changed at steps (KR1){(KR3), then go to step (KR1), otherwise
return F .
ut
Function SPLITK .
Input: A formula F in CNF.
Output: If F is satisable, then T rue, otherwise F alse.
Method.
(KS1) The empty formula. If
containing the empty clause. If ; 2 F , then return F alse.
Splitting into two subproblems. For each literal a occurring in F , construct two
If there exists a literal a such that (K(F
then choose the formulas F 1 and F 2 corresponding to this literal. If SPLITK returns
T rue for at least one of these, then return T rue, otherwise return F alse.
Splitting into four subproblems. Choose a literal a occurring in F . For each
two literals b and c occurring in F [a] and F [a] respectively, construct four formulas
F 11 =REDUCEK
F 21 =REDUCEK
F 22 =REDUCEK
If there exist literals b and c such that
then choose the formulas F 11 , F 12 , F 21 and F 22 corresponding to these literals. If
returns T rue for at least one of these, then return T rue, otherwise return
F alse.
ut
Algorithm 5.1.
Input: A formula F in CNF.
Output: If F is satisable, then T rue, otherwise F alse.
Method.
Return SPLITK (REDUCEK
ut
In Sect. 4 we explained that none of the steps of REDUCEK changes the satisability of
the formula. The steps (KR1){(KR4) cannot be repeated more than K(F
since none of them increases the number of clauses or the number of variables, and during
each iteration (KR1){(KR4){(KR1) at least one of these quantities decreases. Each of these
steps takes a polynomial time. Thus, REDUCEK does not change the satisability of the
formula and returns the answer in a polynomial time.
We now construct a tree which re
ects the behaviour of Algorithm 5.1 (together with
Functions REDUCEK and SPLITK ). Its internal nodes are labelled with formulas that
Algorithm 5.1 splits at steps (KS3) and (KS4). Its leaves are labelled with formulas that
satisfy the conditions of the steps (KS1) and (KS2). Each internal node labelled with F has
two sons labelled with F 1 and F 2 or four sons labelled with F 11 , F 12 , F 21 and F 22 . Since
the conditions of the steps (KS3) and (KS4) guarantee that the corresponding branching
numbers do not exceed (6; 7; 6; 7), by Lemma 3.1 the number of leaves in the tree is at most
is the input formula. Thus, the Algorithm 5.1 returns the answer
in the time p(L(F ))(6; 7; 6; 7) K(F ) , where p is some polynomial.
It remains to prove that Algorithm 5.1 performs correctly, i.e., each formula in CNF
reduced by REDUCEK satises at least one of the conditions of the steps (KS1){(KS4). To
prove this statement, we need two simple lemmas concerning the output of REDUCEK .
Lemma 5.1 Let F 1 be the value of F at step (KR1) of Function REDUCEK at some point
of time (maybe after eliminating several 1-clauses), F 2 be the corresponding output formula
of Function REDUCEK , d and e be literals occurring in F 1 .
(1) If d is a (1 ;1
(2) If d and e are (1 ;1 and there are no clauses in F
that contain d and e simultaneously, then 2.
Proof. (1). If REDUCEK modies once more the formula at steps (KR1) or (KR2), then at
least one clause will be deleted from it. Otherwise, at least one clause will be eliminated at
step (KR3) since K(F 1 ) K(DP d
(2). W.l.o.g we suppose that F 1 contains at most one 1-clause, this clause (if any) contains
a 1-literal and after eliminating this clause the formula F 1 does not contain 1-clauses at
all. If F 1 contains exactly one 1-clause, then it will be eliminated at step (KR1), and one
more clause will be eliminated by (1) since at least one of the literals d and e remains a
Now let F 1 contain no 1-clauses. If REDUCEK modies this formula at step (KR2), then
at least one clause, i.e., at least two occurrences will be eliminated.
Now F has the value F 1 before the step (KR3). W.l.o.g. we suppose that
of the step (KR3). At step (KR3) a 1 -literal will be chosen. After the rst application of
DP , at least one of the literals d and e remains a 1 -literal and its negation or the literal
itself remains in the formula. Hence, by (1) at least one more clause will be eliminated. ut
Lemma 5.2 Let F be a formula in CNF. Then the formula REDUCEK does not contain
1-clauses, 1 -literals and (2;2)-literals.
Proof. Function REDUCEK eliminates 1-clauses at step (KR1). If d is a 1 -literal or a
(2;2)-literal, then K(DP d eliminates such literals at
step (KR3). ut
Theorem 5.1 Algorithm 5.1 performs correctly and stops in the time p(L)(6; 7; 6; 7) K <
p(L)2 0:30897K , where L is the length of the input formula, K is the number of clauses in it,
and p is a polynomial.
Proof. We have shown above that it su-ces to prove that each formula F in CNF reduced
by REDUCEK satises at least one of the conditions of the steps (KS1){(KS4). Suppose
F does not satisfy the conditions of the steps (KS1){(KS4). We now consider all possible
cases. We prove that each of this cases is impossible. All symbols have the same meaning
as they have at the corresponding steps of Function SPLITK . For
The key observation is that if the formula F contains few \frequent" variables, then after
the transformation of F into F [a]; F [a] for some literal a we can apply Lemma 5.1. We now
prove this more formally.
Case 1: The formula F contains a (3
All clauses of the formula F containing the literal a disappear in F [a], all its clauses containing
the literal a disappear in F [a]. Since a is a (3 4. Thus, in terms
of the step (KS3), i.e., the condition of the step (KS3) is
Case 2: The formula F contains a clause that contains a (3;3)-literal a and a (2;3
b.
All three clauses of the formula F containing a disappear in F [a], all three clauses containing
a disappear in F [a]. In addition, b becomes a (1 ;1 + )-literal in F [a]. Thus, in terms of the
step (KS3) we have 1  1 by Lemma 5.1. Hence,  i.e., the
condition of the step (KS3) is satised.
Case 3: The formula F contains a 2-clause consisting of 2-literals.
All clauses of the formula F containing a disappear in F [a], all its clauses containing a
disappear in F [a]. By Lemma 5.2, a is a (2;3 3. Similarly to
Case 2, in terms of the step (KS3) we have 1  1. In addition, C becomes a 1-clause in
F [a] and will be eliminated at step (KR1), i.e. 2  1. We now have
4, i.e., the condition of the step (KS3) is satised.
Case 4: The formula F contains a 3 consisting of 2-literals.
sg. All clauses of the formula F containing a i disappear in F [a i ], all
its clauses containing a i disappear in F [a i ]. By Lemma 5.2, a i is a (2;3
In addition, a 2 and a 3 become
in F [a 1 ]. If C is the only clause that contains a 2 and a 3 simultaneously, then by Lemma 5.1
we have K(F [a 1 ]) K(REDUCEK 2. Otherwise, a 3 becomes a (0;3
in F [a 2 ], i.e. K(F [a 2 ]) K(REDUCEK 2. Depending on which of these two
alternatives takes place, we choose a 1 or a 2 as a in terms of the step (KS3). We now have
i.e., the condition of the step (KS3) is satised.
Case 5: The conditions of Cases 1{4 are not satised.
Since the step (KR2) does not change F , it contains only 3-literals. Since F does not satisfy
the condition of the step (KS3), for each literal a,
3:
Let a be a literal occurring in F . We now prove that there exist literals b and c such that the
condition of the step (KS4) is satised. We consider three sub-cases (the rst two of them
are similar to Cases 2{4).
Case 5.1: There exists a clause in F [a], such that a 1 is a (3;3)-literal
and a 2 is a 2-literal.
We suppose in terms of the step (KS4). Similarly to Case 2, 11  4, 12  3.
Case 5.2: There exists a clause in F [a], such that a 1 is a (2;3)-literal
and a are 2-literals.
We suppose in terms of the step (KS4). Similarly to Cases 3{4, 11  3, 12  4,
or 11  4, 12  3. (Note that by (5.1) the literals a i and a j cannot occur together in two
clauses.)
Case 5.3: The conditions of Cases 5.1{5.2 are not satised.
Since by (5.1) the steps (KR1){(KR3) do not reduce the number of clauses in the formula
F [a] and the conditions of Cases 5.1{5.2 are not satised, this formula consists of clauses
that contain only (2;2)-literals and clauses that contain only (3;3)-literals. Since exactly
three clauses of the formula F disappear in F [a], all occurrences of any (3;3)-literal cannot
disappear in F [a]. Hence, it contains at least one (2;2)-literal b 1 . Let b 1 be a 2-literal. The
formula F does not contain 2-clauses by (5.1). Similarly, it cannot contain two clauses,
each containing the literals a and b 1 simultaneously. Thus, F [a] contains a 3
are 2-literals.
We choose the literal b 1 as b. Both clauses of the formula F [a] that contain b 1 disappear
in F [a; b 1 ]. In addition, these clauses contain only (2;2)-literals which become
literals. Thus, by Lemma 5.1
3:
On the other hand, two clauses of F [a] containing b 1 disappear in F [a; b 1 ], and two more
clauses disappear by Lemma 5.1 since b 2 and b 3 become )-literals. We note that by
(5.1) the formula F contains only one clause that contains b 2 and b 3 simultaneously. Thus,
We now have that in each of Cases 5.1{5.3 there exists a literal b in F [a] such that
7. A literal c can be chosen similarly. Hence, the
condition of the step (KS4) is satised. ut
6 A bound w.r.t. the length of a formula.
In this section we present Algorithm 6.1 which checks satisability of formula F in the
time p(L(F ))2 0:10299L(F ) (where p is a polynomial). As in the previous section, we dene
two subroutines, Function REDUCE L and Function SPLIT L . We use them similarly to
REDUCEK and SPLITK : Function REDUCE L simplies the input formula, then SPLIT L
splits it into several formulas, REDUCE L simplies each of these, and so on.
Function REDUCE L .
Input: A formula F in CNF.
Output: A (simplied) formula in CNF.
Method.
(LR1) Elimination of 1-clauses. If F contains a 1-clause
Repeat this step while F contains such a clause.
Subsumption. If F contains two clauses C and D such that C  D, then F :=
fDg. Repeat this step while F contains such clauses.
Elimination of blocked clauses. If F contains a blocked clause C, then F :=
fCg. Repeat this step while F contains blocked clauses.
Resolution with subsumption. If F contains two clauses C and D such that
R(C; D)D, then F := [fR(C;D)g. Repeat this step while F contains
such clauses.
Elimination of a variable by resolution. Choose a literal a such that a or a
occurs in F and
Repeat this step while F satises this condition.
If F has been changed at steps (LR1){(LR5), then go to step (LR1), otherwise
return F .
ut
Function SPLIT L .
Input: A formula F in CNF.
Output: If F is satisable, then T rue, otherwise F alse.
Method.
(LS1) The empty formula. If
containing the empty clause. If ; 2 F , then return F alse.
containing no 2-clauses. If F does not contain 2-clauses, apply Algorithm
5.1 to F and return its answer.
Splitting into two subproblems. For each literal a occurring in F , construct two
If there exists a literal a such that (L(F )
choose the formulas F 1 and F 2 corresponding to this literal. If SPLIT L returns T rue
for at least one of these, then return T rue, otherwise return F alse.
ut
Algorithm 6.1.
Input: A formula F in CNF.
Output: If F is satisable, then T rue, otherwise F alse.
Method.
Return SPLIT L (REDUCE L
ut
Similarly to REDUCEK , Function REDUCE L does not change the satisability of the
formula and returns the answer in a polynomial time.
We now construct a tree which re
ects the behaviour of Algorithm 6.1 (together with
Functions REDUCE L and SPLIT L ). Its leaves are labelled with formulas that satisfy the
conditions of the steps (LS1){(LS3). Algorithm 6.1 processes in a polynomial time formulas
satisfying the conditions of the steps (LS1) and (LS2), and passes formulas satisfying the
condition of the step (LS3) to Algorithm 5.1 which processes such a formula F in the time
is a polynomial (note that F
contains no 2 -clauses since 1-clauses are eliminated at step (LR1)).
Internal nodes of our tree are labelled with formulas that Algorithm 6.1 splits at step (LS4).
Each internal node labelled with F has two sons labelled with F 1 and F 2 . Since the condition
of the step (LS4) guarantees that the corresponding branching number does not exceed
3.2 the running time of Algorithm 6.1 is upper bounded
by q(L(G))(6; 7; 6; 7) L(G)=3 for input formula G, where q is a polynomial.
It remains to prove that Algorithm 6.1 performs correctly, i.e., each formula in CNF
reduced by REDUCE L satises at least one of the conditions of the steps (LS1){(LS4). We
need three simple lemmas concerning the output of REDUCE L to prove this statement.
Lemma 6.1 Let F be a formula in CNF, d be a literal occurring in it.
(1) If d is a (1;2 )-literal occurring in a 3 -clause, then L(DP d
(2) If d is a (1;1 )-literal occurring in a 2 -clause, then L(DP d 2:
(3) If d is a (1;1)-literal, then L(DP d 2:
Proof. By straightforward calculations. ut
Lemma 6.2 Let F 1 be the value of F at one of the steps (LR1){(LR5) of Function REDUCE L ,
F 2 be the corresponding output formula of Function REDUCE L , d be a literal occurring in
(1) If d is a (1;2 )-literal occurring in a 3 -clause, then
(2) If d is a (1;1 )-literal occurring in a 2 -clause, then 2:
Proof. (1). Note that any change of the formula at steps (LR1){(LR4) is a removal of some
clauses and/or a change of other clauses by their subsets, and thus results in decreasing the
length of the formula by at least one occurrence. If the formula does not change any more
before the step (LR5), then at least one occurrence will be removed by Lemma 6.1(1).
(2). Suppose that after F gets the value F 1 , Function REDUCE L modies the formula
before the step (LR4). This modifying cannot result in increasing the length of a clause or
in increasing the number of occurrences of a literal. Moreover, if the formula changes at
these steps, at least one occurrence is removed. If only one occurrence is removed, then at
least one of the literals d, d remains in the formula. If this is the occurrence of d, then by
Lemma 6.1(1) at least one more occurrence will be removed at step (LR5), and (2) holds.
Otherwise, d becomes a pure literal and will be removed at step (LR5), thus (2) holds again.
Suppose now that REDUCE L does not modify the formula before the step (LR5).
Then, (2) follows from Lemma 6.1(2). ut
We use the following simple properties of the formula reduced by Function REDUCE L
in the proof of 6.1 without explicit mentioning.
Lemma 6.3 Let G. Then
(1) F does not satisfy any of the conditions of the steps (LR1){(LR5);
(2) there are no 1-clauses in F ;
(3) there are no pure literals and (1;1)-literals in F ;
(4) there are no 2-clauses in F containing a 1-literal;
(5) for any literal d occurring in F , } d
for any 1-literal d occurring in F , } d +# d  7;
(7) for any literal d occurring in F , } d +# d  5.
Proof. (1) is trivial; (2){(7) since F does not satisfy the conditions of the step (LR1)and
see also Lemma 6.1. ut
Theorem 6.1 Algorithm 6.1 performs correctly and stops in the time p(L)(6; 7; 6; 7) L=3 <
p(L)2 0:10299L , where L is the length of the input formula and p is a polynomial.
Proof. We have shown above that it is su-cient to prove that each formula F in CNF reduced
by REDUCE L satises at least one of the conditions of the steps (LS1){(LS4). Suppose F
does not satisfy the conditions of the steps (LS1){(LS3). We now consider the two possible
cases: when F contains at least one 1-literal a, and when it contains no 1-literals. We prove
that in each of these cases F satises the condition of the step (LS4).
Informally, this is done as follows. In the rst case we show that the assignment I(a)
contains many literals. The second case is handled by careful examination of sub-cases: we
choose a 2-clause fc; dg in F and examine the following sub-cases:
there are many occurrences in the clauses containing the literal c (or d);
F contains many occurrences of the literal c (or d).
In these two sub-cases we show that many occurrences are eliminated during the transformation
of F into F [c]; F [c] (or F [d]; F [d]) and the subsequent elimination of 1-clauses
obtained from the clauses containing the literals c; c (or d; d). The third sub-case is:
none of the previous sub-cases holds.
In this sub-case one of c and d is a (2;2)-literal occuring only in 2- and 3-clauses which
allows us to use Lemma 6.1 after one occurrence of this literal is eliminated during the
splitting by another literal.
In the following we denote
F 2 and a literal a have the same meaning as they have at step (LS4) of Algorithm 6.1.
Case 1: The formula F contains a 1-literal a.
be the only clause containing a. Let
and } a +# a  7 by Lemma 6:3, we have # a  max(7 } a ;
be the number
of 3 -clauses among all clauses that contain a.
During the transformation of the formula F into F 2 , all occurrences of the literal a and
all clauses containing a will be eliminated. Thus,
+# a
5:
During the transformation of the formula F into F 1 , the clause D and all occurrences
of the literal a will be eliminated; all 2-clauses containing a will be eliminated too (at
step (LR1)). Since D is not blocked for any a i w.r.t. F , for each there exists
clause D i in F such that D i \ fa; a g. All these clauses will be eliminated
since all clauses fa; a i g are blocked for a w.r.t. F (i.e. fa; a clauses
containing a, all clauses D i and the clause D are distinct. Thus, we have
r+(7 r)+(# a
We now have i.e., the
condition of the step (LS4) is satised 1 .
Case 2: The formula F does not contain 1-literals.
Since F does not satisfy the condition of the step (LS3), it contains a 2-clause dg.
Let us note that
The formula F does not contain other clauses that contain
the literal d and the literal c, or the literal d and the
literal c, or the literal d and the literal c, simultaneously.
This proposition is true since F does not satisfy the conditions of the steps (LR2) and (LR4).
Also, in this case I(c) = fcg and I(d) = fdg by (6.2) and the denition of I(: : :).
Let us denote one of the literals c, d by a (we shall choose later which one). We denote
the remaining literal by b. Let  be the number of 3 -clauses among all clauses that contain
a (note that # a   1), let
be the number of 3 -clauses among all clauses that contain
a. We now count the occurrences that disappear during the transformation of the formula
F into F [I(a)] (= F [a]) and F [a] and subsequent elimination of 1-clauses resulted from the
2-clauses containing the literals a and a.
During the transformation of the formula F into F 1 , all occurrences of the literal a and
all clauses containing a will be eliminated; all 2-clauses that contain a will be eliminated too
(at step (LR1)), there are (# a
clauses.
1 Kullmann and Luckhardt [16] prove for a very similar algorithm that in this case
thus, (5; 17) in the condition of the step (LS4) can be replaced by (8; 12). However, this would not improve
our upper bound while would make the proof longer; thus, we present here this simpler proof.
The formula F [a] contains the 1-clause fbg obtained from the 2-clause D. It will be
eliminated at step (LR1). If F contains other 2-clauses containing a, the clauses obtained
from them will be eliminated at step (LR1) too. The number of such clauses is (# a 1 ).
During the transformation of the formula F into F 2 , all occurrences of the literal a and all
clauses containing a or b will be eliminated. By (6.2), D is the only clause containing b in
which the literals a; a can occur. Thus, even if we count only occurrences that disappear in
clauses containing a or a before the rst application of the step (LR2), we have
We consider several sub-cases.
Case 2.1: } c  6 and } d  6.
From (6.3) and (6.4) we have
Thus, i.e., the condition of the step (LS4) is satised.
Case 2.2: # c  3 or # d  3.
Let a 2 fc; dg be the literal for which # a  3 holds, let b be the remaining literal in fc; dg.
Thus, we have
a +# a  22:
Thus, i.e., the condition of the step (LS4) is satised.
Case 2.3: # or } d  5.
Let a 2 fc; dg be a literal such that } a be the remaining literal in
fc; dg. Then 4  } b  5 and } a  } b . In this case b is a 2-literal, it occurs in D and in one
other 2- or 3-clause. We denote this clause by C b .
The literal b becomes a (1;2)-literal in F [I(a)] (= F [a]). We now complete the proof
by showing that several literal occurrences will be eliminated in addition to the occurrences
counted by (6.3). There are three sub-cases.
Case 2.3.1: At least two occurrences are eliminated before the rst application of step (LR2)
in addition to the occurrences counted by (6.3).
In this case,
+(# a )9;
a +# a  20:
Case 2.3.2: Exactly one occurrence is eliminated before the rst application of step (LR2)
in addition to the occurrences counted by (6.3).
We remind that (6.3) counts only occurrences to the clauses containing one of the literals
a,a. By (6.2) the occurrence of the literal b to the clause C b or any occurrence of the literal
b cannot be eliminated during the transformation of the formula F into the formula F [a]. If
we counted any of these occurrences in the # a
term of (6.3), then it was an elimination
of a 1-clause fbg obtained from a 2-clause fa; bg. Since it is impossible to have two distinct
identical clauses fa; bg in the formula, the other two occurrences (another occurrence of the
literal b and the occurrence of the literal b in C b ) eliminated at this moment are not counted
by (6.3); this fact contradicts the assumption of Case 2.3.2.
Thus in this case b remains a (1;2)-literal before the rst application of the step (LR2). By
Lemma 6.2(1) at least one more occurrence will be eliminated after that and thus (6.5){(6.7)
hold.
Case 2.3.3: No occurrences are eliminated before the rst application of step (LR2) in
addition to the occurrences counted by (6.3).
Similarly to Case 2.3.2, b remains a (1;2)-literal before the rst application of the step (LR2)
during transformations of the formula F [a] by Function REDUCE L . Thus, if jC b
two more occurrences are eliminated by Lemma 6.2(2), and (6.5){(6.7) hold.
If, however, jC then we can apply only Lemma 6.2(1), but in this case } a  }
and thus
10;
Hence, in all three sub-cases 2.3.1{2.3.3, i.e., the condition
of the step (LS4) is satised. ut
7 Conclusion and further work
In this paper we have improved the existing upper bounds for SAT with respect to K (the
number of clauses) and L (the length of a formula). The key point in our algorithms and
proofs is the black and white literals principle, a new transformation rule which can be viewed
as a re-formulation of two previously known principles: the autarkness [20, 22, 17, 15] and
the generalized sign principle [16].
Our proofs (as well as the proofs of the previous upper bounds [21, 16]) are neither short
nor elegant. It would be a kind of breakthrough to nd a compact way to present proofs
of upper bounds for splitting algorithms. It is believable that such a way could lead to
even better bounds, since currently our possibilities to create new heuristics and prove the
corresponding upper bounds are limited by the length of a comprehensible proof. On the
other hand, it is a challenging problem to prove (more) tight lower bounds for (some class
splitting algorithms: currently, the exponential lower bounds for resolution proofs (see,
e.g., [27]) are far enough from the known upper bounds for splitting algorithms. (Most of
splitting algorithms can be viewed as resolution proofs and vice versa.)
Another direction for work is to nd randomized algorithms that give better upper bounds
for SAT (or to nd a way how to apply modern randomized algorithms that have already been
invented for 3-SAT in recent breakthrough papers [23, 24]). Also, it remains a challenging
problem to nd a less-than-2 N upper bound where N is the number of variables.



--R

Tautology proof systems based on the splitting method
Less than 2 n satis
Approximation algorithms for Max Sat: a better performance ratio at the cost of a longer running time
Exponential upper bounds for the satis
A machine program for theorem-proving
A computing procedure for quanti
Algorithms for Satis
Separating the signs in the satis
Two new upper bounds for SAT
Local Search Algorithms for SAT: Worst-Case Analysis
Hard formulas for SAT local search algorithms
SAT local search algorithms: worst-case study

New methods for 3-SAT decision and worst-case analysis
Investigations on autark assignments
Algorithms and their complexity
Obere Komplexit
Parametrizing above guaranteed values: MaxSat and Max-Cut
New upper bounds for MaxSat

Upper bounds for covering problems
Solving satis

An Improved Exponential-time Algorithm for k-SAT
Solving 3-satis ability in less than 1:579 n steps
Pure literal look ahead: An O(1:497 n
The Complexity of Propositional Proofs
A satis
--TR

--CTR
Rainer Schuler, An algorithm for the satisfiability problem of formulas in conjunctive normal form, Journal of Algorithms, v.54 n.1, p.40-44, January 2005
Bolette Ammitzbll Madsen, An algorithm for exact satisfiability analysed with the number of clauses as parameter, Information Processing Letters, v.97 n.1, p.28-30, January 2006
Evgeny Dantsin , Andreas Goerdt , Edward A. Hirsch , Ravi Kannan , Jon Kleinberg , Christos Papadimitriou , Prabhakar Raghavan , Uwe Schning, A deterministic (2 - 2/(k+ 1))n algorithm for k-SAT based on local search, Theoretical Computer Science, v.289 n.1, p.69-83, 23 October 2002
Ramamohan Paturi , Pavel Pudlk , Michael E. Saks , Francis Zane, An improved exponential-time algorithm for k-SAT, Journal of the ACM (JACM), v.52 n.3, p.337-364, May 2005
Tobias Riege , Jrg Rothe , Holger Spakowski , Masaki Yamamoto, An improved exact algorithm for the domatic number problem, Information Processing Letters, v.101 n.3, p.101-106, February, 2007
Ryan Williams, Algorithms for quantified Boolean formulas, Proceedings of the thirteenth annual ACM-SIAM symposium on Discrete algorithms, p.299-307, January 06-08, 2002, San Francisco, California
Haiou Shen , Hantao Zhang, Improving exact algorithms for MAX-2-SAT, Annals of Mathematics and Artificial Intelligence, v.44 n.4, p.419-436, August    2005
Jens Gramm , Edward A. Hirsch , Rolf Niedermeier , Peter Rossmanith, Worst-case upper bounds for MAX-2-SAT with an application to MAX-CUT, Discrete Applied Mathematics, v.130 n.2, p.139-155, 15 August
Edward A. Hirsch, Worst-case study of local search for MAX-k-SAT, Discrete Applied Mathematics, v.130 n.2, p.173-184, 15 August
Laurent Simon , Daniel Le Berre , Edward A. Hirsch, The SAT2002 Competition, Annals of Mathematics and Artificial Intelligence, v.43 n.1-4, p.307-342, January 2005
Oliver Kullmann, Lean clause-sets: generalizations of minimally unsatisfiable clause-sets, Discrete Applied Mathematics, v.130 n.2, p.209-249, 15 August
Rolf Niedermeier , Peter Rossmanith, An efficient fixed-parameter algorithm for 3-hitting set, Journal of Discrete Algorithms, v.1 n.1, p.89-102, February
SAT;worst-case upper bounds