3
$\begingroup$

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)
       exclude.add(a)
       exclude.add(b)

  if len(exclude) == 2:
   size = len(general)
   if size == 3:
    return { frozenset(general) }
   elif size == 2:
    for e in general:
     exclude.add(e * -1)
    options = set()
    for l in literals - general - exclude:
     general.add(l)
     options.add(frozenset(general))
     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)
         formula.add(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

class doubly_linked_list:
   def __init__(self):
      self.head = None
      self.tail = None
      self.cur = None

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

   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.

enter image description here

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

enter image description here

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.

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.