Superresolution for MAX-SAT

October 24, 2006

We use N to denote a global variable which keeps the best assignment so far. N is assigned arbitrarily at the beginning.

1. Unit-Propagation:

M||F, C + k ⇒ Mk||F, C + k

if C + k is an unexplored superresolvent if there exists any, and M ⊧ ¬C, and k is undefined in M, and unsat(M!k; F, C + k) ≥ unsat(N; F, C + k).

2. Semi-Superresolution:

Mk^{∗}||F ⇒ Mk^{∗}||F, (the disjunction of the negated decision literals in (Mk^{∗}))

if k is undefined in M, and let R = Contradiction(M, k, F), then R ≠ ∅, and unsat(MkR; F) ≥ unsat(N; F).

Informal: Intuitively, since R is driven by (Mk^{∗}) through unit-propagation, thus, the fact that ”unsat(MkR; F) ≥ unsat(N; F)” implies that we have made a mistake by setting the partial interpretation to (Mk^{∗}), which is the reason why we add the negated literals in (Mk^{∗}) to F so that we won’t make the same mistake again.

Contradiction(M, k, F): there is a sequence of transitions from the state Mk||F by Unit-Propagation to a state MkR||F where some clause(s) is unsatisfied by (MkR). Contradiction returns R if there is a contradiction and ∅ otherwise.

3. Decide:

M||F ⇒ Mk ∗ ||F

if k is undefined in M, and k and !k occur in some clause(s) of F.

4. Restart:

M||F ⇒ ||F

5. Update:

Update(N; M): update N with the given assignment M.