# Find the flaw in the 3SAT solver algorithm

I consider decision version of 3SAT problem. Main idea is to find congruent clauses and construct such maximum formula, which satisfiability/truth table won't be changed.

In case of unsatisfiable formula, this "maximum core" size equals to 8/6 * (n - 2) (n - 1) n, where n is maximum literal number.

Otherwise for satisfiable maxcore, size equals or less than 7/6 * (n - 2) (n - 1) n

Input: 3SAT CNF, Output: Satisfiability

Implementation:

# Maximum satisfiable formula size of N literals
def upperbound(N):
n = N - 2
return ((n * (n + 1) * (n + 2)) // 6) * 7

# Generate non-conflict clauses from pair. Function can return either 1, N + 2 (starting from N = 7) or 0 caluses
def children(p,p1,literals):
general = set(p | p1)
exclude = set()

for a,b in itertools.combinations(general,2):
if a == b * -1:
general.remove(a)
general.remove(b)

if len(exclude) == 2:
size = len(general)
if size == 3:
return { frozenset(general) }
elif size == 2:
for e in general:
options = set()
for l in literals - general - exclude:
general.remove(l)
return options

return frozenset()

def isat(formula,N):
lim = upperbound(N)
literals = set(range(-1 * N,N + 1)) - {0}
pairs = doubly_linked_list() # DS to get rid of duplicate combinations

for clause in formula: # Filling initial formula
pairs.push(clause)

while True:
pair = pairs.pop()
if pair != None:
p,p1 = pair
for child in children(p,p1,literals):
if child not in formula:
pairs.push(child)
if len(formula) > lim:
return False
else:
return True # No more combinations and maximum satisfiable size reached.
return True


Special list to escape clause pairs duplicates:

class Node:
def __init__(self, data):
self.data = data
self.next = None
self.prev = None
self.pair = None
self.completed = False

def __init__(self):
self.tail = None
self.cur = None

def push(self, data):
newNode = Node(data);
self.tail.next = None
else:
self.tail.next = newNode
self.tail.pair = newNode
newNode.previous = self.tail
self.tail = newNode
self.tail.next = None

def pop(self):
if self.cur == self.tail:
return None
elif self.cur.completed == True:
self.cur.pair = self.cur.pair.next
self.cur.completed = False
p = self.cur.data
p1 = self.cur.pair.data
if self.cur.pair != self.tail:
self.cur.pair = self.cur.pair.next
else:
self.cur.completed = True
self.cur = self.cur.next
return p, p1


Example unsat input:

{frozenset({1, 3, 5}), frozenset({1, 4, -3}), frozenset({3, -1, -2}), frozenset({2, 5, -3}), frozenset({-5, -1, -2}), frozenset({3, -4, -5}), frozenset({3, 4, -5}), frozenset({5, -3, -2}), frozenset({4, -3, -2}), frozenset({2, -4, -3}), frozenset({2, 4, -3}), frozenset({1, 3, 4}), frozenset({2, 5, -1}), frozenset({1, -3, -2}), frozenset({2, -5, -3}), frozenset({5, -1, -2}), frozenset({3, 5, -2}), frozenset({-5, 4, -2}), frozenset({-4, -3, -1}), frozenset({-5, -3, -1})}


And sat one:

{frozenset({2, -4, 5}), frozenset({2, -6, -3}), frozenset({-7, 3, -1}), frozenset({-8, 1, 7}), frozenset({-8, -5, -4}), frozenset({1, -3, -7}), frozenset({2, 4, 6}), frozenset({8, -7, -6}), frozenset({-7, -3, -2}), frozenset({-8, 4, 7}), frozenset({4, -3, -2}), frozenset({8, -7, 2}), frozenset({-7, 5, 6}), frozenset({-8, -4, -2}), frozenset({3, 4, -1}), frozenset({-4, 5, -2}), frozenset({2, -1, 7}), frozenset({-8, 2, -4}), frozenset({-7, 5, -3}), frozenset({3, 6, 7}), frozenset({2, 5, -1}), frozenset({-8, -1, 7}), frozenset({-7, 2, -3}), frozenset({-8, 5, 6}), frozenset({-8, 3, 4}), frozenset({-7, -3, 6}), frozenset({3, 5, -1}), frozenset({2, -4, -1}), frozenset({5, 6, 7}), frozenset({-7, 2, 6})}


I have a problem whether with complexity analysis or with valid counter examples. My guess that algorithm is O(n^7), but it should be impossible.

Empirical research of worst cases also shows polynomial growth.

Relationship of f(n) = k, where n is max literal, and k is basic iterations count (1 + size of children function result) or time.

ln(x) vs ln(y) shows straight line.

ln(y) vs x doesn't show straight line.

X (max literal) : [4,5,6,7,8,9,10,11,12,13,14]

Y (iterations) : [594, 3495, 12970, 37450, 91756, 199794, 397740, 737715, 1291950, 2157441, 3461094]

I need clarification that this is an exponential algorithm or some counter examples which will break it.

From the looks of it, you're taking every pair of 3-clauses and resolving them, keeping the implications. (If the result is a tautology or if there is no literal to resolve upon then nothing is kept.) The problem is that you are also discarding 4-clauses (i.e., size == 4), which makes your search implicationally incomplete.

One can demonstrate this with a direct transformation, though there are likely smaller explicit counter examples. Consider a single clause (x ∨ y ∨ z); taking three fresh variables a, b, and c we can replace this with the following set of clauses:

(x ∨ ¬a ∨ b)
(y ∨ ¬b ∨ c)
(z ∨ ¬c ∨ ¬a)
(x ∨ a ∨ ¬b)
(y ∨ b ∨ ¬c)
(z ∨ c ∨ a)


If (x ∨ y ∨ z) is false, then the above becomes unsatisfiable (it becomes two implication chains expressing a → ¬a and ¬a → a). If (x ∨ y ∨ z) is true, then the chains are broken and it becomes satisfiable.

Within this set of clauses, every resolvent is a 4-clause (or a tautology), so your algorithm derives no implications from them. Furthermore, since a, b, and c do not appear anywhere else in the formula, any resolvent produced by these clauses upon x, y, or z will also be a 4-clause.

The clause (x ∨ y ∨ z) is implied by the above, but it requires resolving two 4-clauses to get there (while also deriving two other 4-clauses along the way). Since you do not keep 4-clauses, this implication is missed and your algorithm incorrectly reports sat for unsat formulas.

Modifying your code a bit into:

def num_var(formula):
N = 0
for c in formula:
for l in c:
N = max(N, abs(l))
return N

def isat(formula):
N = num_var(formula)
# [...]


We can define a function which performs the above translation on every clause in the formula:

def obfuscate(formula):
next_var = num_var(formula) + 1
new_formula = set()

for (x, y, z) in formula:
a = next_var + 0
b = next_var + 1
c = next_var + 2
next_var += 3

new_formula |= {
frozenset({x, -a, b}),
frozenset({y, -b, c}),
frozenset({z, -c, -a}),
frozenset({x, a, -b}),
frozenset({y, b, -c}),
frozenset({z, c, a}),
}

return new_formula


Passing any unsat formula through this will produce another unsat formula, which your algorithm will claim is sat after producing zero new clauses during its search:

# 3-SAT form of (1) ∧ (-1):
unit_conflict_on_1 = {
frozenset({1, 2, 3}),
frozenset({1, -2, 3}),
frozenset({1, 2, -3}),
frozenset({1, -2, -3}),
frozenset({-1, 4, 5}),
frozenset({-1, -4, 5}),
frozenset({-1, 4, -5}),
frozenset({-1, -4, -5}),
}

print(isat(obfuscate(unit_conflict_on_1)))


If you correct this issue, you will lose your polynomial bound on the number of clauses you might derive.

In general, resolution (and things with the strength of resolution, like CDCL) have known exponential lower bounds for hard tautologies. Getting below this barrier requires techniques stronger than searching over the space of implications.