Reducing SAT to 2-SAT
Abstract
Description of a polynomial time reduction of SAT to 2-SAT of
polynomial size.
http://arxiv.org/abs/0704.0108v1
Reducing SAT to 2-SAT
Sergey Gubin
November 4, 2018
1 Introduction
Among all dimensions, 2-SAT possesses many special properties unique in
the sense of computational complexity [1, 2, 3, 4, 5]. But in light of works
[6, 8, 7, 9] a problem arose: either those properties are accidental or there
are polynomial time reductions of SAT to 2-SAT of polynomial size. This
article describes one such reduction.
2 Presenting SAT with XOR
In [6] was described one of the ways to present SAT with a conjunction of
XOR. Let us summarize it.
Let Boolean formula f define a given SAT instance:
f = c1 ∧ c2 ∧ . . . ∧ cm. (1)
Clauses ci are disjunctions of literals:
ci = Li1 ∨ Li2 ∨ . . . ∨ Lini , i = 1, 2, . . . , m
- where ni is the number of literals in clause ci; and Lij are the literals. Using
distributive laws, formula (1) can be rewritten in disjunctive form:
f = d1 ∨ d2 ∨ . . . dp, p = n1n2 . . . nm.
Clauses dk in this presentation are conjunctions of m literals - one literal
from each clause ci, i = 1, 2, . . . , m:
dk = L1k1 ∧ L2k2 ∧ . . . ∧ Lmkm , k = 1, 2, . . . , p. (2)
∗Author’s email: sgubin@genesyslab.com
It is obvious that formula (1) is satisfiable iff there are clauses without com-
plimentary literals amongst conjunctive clauses (2). Disjunction of all those
clauses is the disjunctive normal form of formula (1). Thus, formula (1) is
satisfiable iff there are members in its disjunctive normal form.
There is a generator for conjunctive clauses (2):
(ξi1 ⊕ ξi2 ⊕ . . .⊕ ξini) = true, (3)
- where Boolean variable ξµν indicates whether literal Lµν participates in con-
junction (2). Solutions of equation (3) generate conjunctive clauses (2). Let’s
call the variables ξ the indicators. To select from all solutions of equation (3)
those without complimentary clauses, let’s use another Boolean equation.
For each of the combination of clauses (ci, cj), 1 ≤ i < j ≤ m, let’s build
a set of all couples of literals participating in the clauses:
Aij = { (Liµ, Ljν) | ci = Liµ ∨ . . . ; cj = Ljν ∨ . . . }.
Let Bij be a set of such couples of indicators (ξiµ, ξjν), that the literals they
present are complimentary:
Bij = { (ξiµ, ξjν) | (Liµ, Ljν) ∈ Aij, Liµ = L̄jν }.
There are C2m sets Bij , 1 ≤ i < j ≤ m, and
|Bij| ≤ min{ni, nj}.
Let’s mention that some of the sets can be empty. Then, the following equa-
tion will select from all solutions of equation (3) those without complimentary
clauses:
1≤i<j≤m
(ξ,ζ)∈Bij
(ξ̄ ∨ ζ̄) = true. (4)
Due to the above estimations of the number of sets Bij and of their sizes, the
number of clauses in formula (4) is
n = O(t2m
- where t2 is the second number in the row of clauses’ sizes sorted by value:
t1 = max{n1, n2, . . . , nm}, t2 = max
min{ni, nj}, . . .
Because satisfiability of formula (1) means that the disjunctive normal
form of formula (1) has conjunctive clauses, formula (1) is satisfiable iff the
following formula/equation is satisfiable:
g ∧ h = true. (5)
The reasons for replacing formula (1) with formula (5) are explained in
[6]. The number of true-strings in truth-tables of XOR clauses of formula
(3) is linear over initial input. The number of true-strings in truth-tables of
disjunctive clauses of formula (4) is just 3. The number of all clauses in (5)
is cubic over initial input. It can be estimated as
m+ n = O(t2m
Thus, application of the simplified compatibility matrices method [6] to equa-
tion (5) will produce a polynomial time algorithm for SAT. But let’s return
to the reduction.
3 SAT vs. 2-SAT
Let’s apply the simplified method of compatibility matrices [6] to equation
(5). The method consists of sequential Boolean transformations of compat-
ibility matrices of equation (5). Let’s mention that after m iterations, due
to the allocation of formula (4) at the end of formula (5), there will only be
compatibility matrices of equation (4) left in play. They will be grouped in
an upper triangular box matrix
S = (Fm+µ,m+ν)1≤µ<ν≤n. (6)
The matrix is displayed below:
Fm+1,m+2 Fm+1,m+3 . . . Fm+1,m+n
Fm+2,m+3 . . . Fm+2,m+n
. . .
Fm+n−1,m+n
If there are no complimentary literals in different clauses of formula (1),
then formula (4) is just missing. The size of matrix (6) is 0× 0. In this case,
formula (1) is reducible to 1-SAT instance
ω1 ∧ ω2 ∧ . . . ∧ ωm,
- where
ωi = ξi1 ⊕ ξi2 ⊕ . . .⊕ ξini, i = 1, 2, . . . , m.
This singularity belongs to the set of all 2-SAT instances.
If, during the first m iterations, a pattern of unsatisfiability arises (one of
the compatibility matrices becomes filled with false entirely), then formulas
(5) and (1) are both unsatisfiable [6]. This case may be thought of as a case
of formula (1) being reduced to an unsatisfiable formula
false.
Let’s include this singularity in the set of all 2-SAT instances.
Otherwise, boxes Fm+µ,m+ν in matrix (6) are what is left of the compati-
bility matrices of equation (4) after the first m iterations of the method.
Due to their construction [6], the boxes are 3× 3 matrices:
Fm+µ,m+ν = (xij)3×3, 1 ≤ µ < ν ≤ n (7)
- where xij ∈ {false, true}. The number of boxes is C
n. Thus, the number
of all elements in matrix (6) is
e = 9C2n = O(t
Let’s enumerate the elements arbitrarily:
y1, y2, . . . , ye.
Then, distribution of true/false in matrix (6) can be described with a 1-SAT
formula/equation
w = η1 ∧ η2 . . . ∧ ηe = true, (8)
- where ηi are literals over a set of Boolean variables
{ b1, b2, . . . , be }.
The literals are
bi, yi = true
b̄i, yi = false
, i = 1, 2, . . . , e.
Let’s take the following 2-SAT instance:
h ∧ w. (9)
Box matrix (6) is an initialization of the modified method of compatibility
matrices [6] for formula (9): compatibility matrices of formula (4) are de-
pleted to satisfy equation (8). Thus, continuation of the simplified method
of compatibility matrices for equation (5) from its Step m+ 1 to its finish is
an application of the modified method of compatibility matrices to system
(9) from its Step 1 to its finish [6]. After n−2 iterations, both methods must
result with the same version of satisfiability of formula (1). Thus, formulas
(5) and (1) are satisfiable iff 2-SAT formula (9) is satisfiable. The number of
clauses in formula (9) is
e+ n = O(t22m
According to [6], the time to deduce formula (9) can be safely estimated as
O(t41t
4 SAT vs. 1-SAT
Let’s take one step further. Applying to formula (1)/(5) either of the varia-
tions of the compatibility matrices method [6] will produce a Boolean matrix.
Let it be a matrix R:
R = (rij)a×b.
Size of the matrix depends on the method’s variation and the order of clauses
in formula (1). The size can be changed if permute the clauses and repeat the
method [6]. The formula (1) is satisfiable iff matrix R contains true-elements
[6] (elements which are true). The existence/absence of the true-elements is
the only invariant.
If formula (1) is unsatisfiable, then that formula is reducible to formula
“false”. Otherwise, formula (1) is reducible to a 1-SAT instance.
Proof. Let’s enumerate elements of matrix R in arbitrarily order:
z1, z2, . . . , zab.
Let B be a set of t = ab Boolean variables:
B = { bi ∈ {false, true} | i = 1, 2, . . . , t }.
Then the following 1-SAT formula describes distribution of true/false in
matrix R:
θ1 ∧ θ2 ∧ . . . ∧ θt, (10)
- where literals θi are
bi, zi = true
b̄i, zi = false
, i = 1, 2, . . . , t.
Thus, the compatibility matrices method reduces satisfiable formula (1) to
1-SAT formula (10).
In its turn, formula (10) can be rewritten as SAT of any dimension by
appropriate substitution of variables.
If use the simplified method of compatibility matrices, then matrix R is a
3× 3 Boolean matrix [6]. Let there be two clauses shorter than 3 in formula
(1). Let’s permute all clauses and make those shortest clauses to be the last
ones in formula (1). Then, result of the modified method [6] will be a matrix
R of size less than 3× 3. That proves the following theorem.
Theorem 1. Any SAT instance is reducible to a 1-SAT instance with 9
variables or less. A SAT instance is unsatisfiable iff its 1-SAT presentation
is “false” - there is not any variables in its 1-SAT presentation.
5 Conclusions
Formula (1) may be thought of as a “Business Requirements”. And any
appropriate computer program may be thought of as a solution of the SAT
instance. Then, theorem 1 can be an explanation of the remarkable efficiency
of the “natural programs”. From this point of view, the iterations of the
method of compatibility matrices may be thought of as a learning/modeling
of the business domain. In the artificial programming, the calculation of the
compatibility matrices - a virtual business domain - could be a conclusion of
the stage “Business Requirements Analysis/Mathematical Modeling”. That
would improve the programs’ performance. The resulting compatibility ma-
trices may be thought of as a fussy logic’s tables of rules for the domain.
The whole solution of formula (1) can be achieved, with one of the fol-
lowing approaches, for example. ANN approach is the applying of the com-
patibility matrices method backward, starting from matrix R. An example
of that can be found in [7]. DTM approach is the looping trough of the
following three steps: selection of any true-element from matrix R; substi-
tution of the appropriate true-assignments in formula (1); and repeating of
the compatibility matrices method. The last method is an implication of the
self-reducibility property of SAT [5].
In certain sense, theorem 1 may be seen as an answer to the Feasibility
Thesis [2].
References
[1] Stephen Cook. The complexity of theorem-proving procedures. In Con-
ference Record of Third Annual ACM Symposium on Theory of Com-
puting. p.151-158, 1971
[2] Stephen Cook. The P versus NP problem.
http://www.claymath.org/millennium/P_vs_NP/pvsnp.pdf
[3] Richard M. Karp. Reducibility Among Combinatorial Problems. In
Complexity of Computer Computations, Proc. Sympos. IBM Thomas
J. Watson Res. Center, Yorktown Heights, N.Y. New York: Plenum,
p.85-103, 1972.
[4] M.R. Garey and D.S. Johnson. Computers and Intractability, a Guide to
the Theory of NP-Completeness. W.H. Freeman and Co. San Francisco,
1979.
http://www.claymath.org/millennium/P_vs_NP/pvsnp.pdf
[5] Lane A. Hemaspaandra, Mitsunori Ogihara. The Complexity Theory
Companion. Springer-Verlag Berlin Heidelberg, 2002.
[6] Sergey Gubin. A Polynomial Time Algorithm for SAT.
http://www.arxiv.org/pdf/cs/0703146
[7] Sergey Gubin. A Polynomial Time Algorithm for 3-SAT. Examples of
use. http://www.arxiv.org/pdf/cs/0703098
[8] Sergey Gubin. A Polynomial Time Algorithm for 3-SAT.
http://www.arxiv.org/pdf/cs/0701023
[9] Sergey Gubin. A Polynomial Time Algorithm for The Traveling Sales-
man Problem. http://www.arxiv.org/pdf/cs/0610042
http://www.arxiv.org/pdf/cs/0703146
http://www.arxiv.org/pdf/cs/0703098
http://www.arxiv.org/pdf/cs/0701023
http://www.arxiv.org/pdf/cs/0610042
	Introduction
	Presenting SAT with XOR
	SAT vs. 2-SAT
	SAT vs. 1-SAT
	Conclusions
