SAT solvers have become an important tool to solve hard computational problems. They are used in Eclipse etc. This homework deals with CNFs which are the input format to SAT solvers. We study algorithms for approximately solving SAT problems. This homework has many connections to homework one. A greedy algorithm will do the job.
Reading: Read section 13.4, pages 724, 725 to the middle of page 726. Refresh your memory about Satisfiability (SAT and 3SAT). See the index in the text book to find the relevant sections to read.
We define the Johnson-CNF-Approximation-Playground (named after David Johnson): http://www2.research.att.com/~dsj/index.php
Claim f-CNF-ATLEAST(k): For all CNFs S with clauses of at least length k (abbreviated CNF-ATLEAST(k)) there exists an assignment J for S that satisfies the fraction sat(S,J) >= f of all clauses. sat(S,J) = fraction of satisfied clauses in CNF S under assignment J.
Connections to homework 1:
homework 1 this homework x information about CNF S in ATLEAST[k] y assignment J to variables of S min x max y f(x,y) >= f min S max J sat(S,J) >= tau[k]
The quantifier game implies the refutation protocol: Bob sends Alice a CNF S in CNF-ATLEAST(k) and Alice sends an assignment J for S. refute(S,J) = sat(S,J) < f (Note that because Alice claims the existence of an assignment of a certain quality, it is important that she must produce it in the protocol.)
Note that the game requires us to actually construct assignments that we claim to exist. Therefore, we look for a fast algorithm to find such assignments. It turns out that random assignments do a pretty good job because the average assignment has a pretty high satisfaction ratio.
Example:
Alice claims: 1/2-CNF-ATLEAST(1)
Bob sends Alice the CNF:
A
!A
!B
B
C
D
Alice sends back the assignment J =(A,B,C,!D)
satisfying 3/6 clauses. Therefore, Alice wins.
Now we close the set of claims under negation by adding:
Claim !f-CNF-ATLEAST(k): There exists a CNF S in CNF-ATLEAST(k) so that for all assignments J for S: sat(S,J) <= f.
We want to invent a game, based on the above refutation protocol, that helps Alice and Bob to determine the optimum value for f so that claim f-CNF-ATLEAST(k) can be neither strengthened nor refuted. We call this optimum value tau(k).
We engage the following use of the protocol: Although Alice and Bob behave egoistically (they maximize their points through refuting and avoiding refuting), they create useful upper and lower bounds along with algorithms achieving the upper bounds.
The scholars (Alice and Bob) play in rounds. They must propose and oppose/agree in each round. Opposing means either strengthening or refuting. Strengthening is proposing a stronger claim. The agreement protocol is simple: Both scholars have to defend the claim against the other and both players have to refute the negated claim against the other.
We note that we have two trivial starting points: 0-CNF-ATLEAST(k) ) (increasing bound) !1-CNF-ATLEAST(k) (decreasing bound) which are trivially true. Hopefully the increasing bound and the decreasing bound will meet soon.
If Alice would be perfect, she would claim the optimal answer between 0 and 1 in her first try. She would make the optimal claim that cannot be refuted nor strengthened. The only rational action would be to agree. If Bob is perfect too, he would recognize this and the game would end with the optimum result immediately.
In reality, Alice and Bob are not perfect. There is opportunity for refuting and strengthening. If a claim is s successfully refuted, we ask the refuter to propose a strengthening of the negation of the refuted claim. P stands for player (e.g., Alice); OP for oponent player (e.g., Bob).
P proposes C
OP opposes C
refutes C yes: -> OP proposes !C (or a stronger claim)
no: P proposes C''(C'' => C) or P agrees with C,
strengthens C: OP proposes C' (C' => C)
OP agrees: tie if optimum reached
Example:
The innovation algorithm in operation.
Alice claims: 0-CNF-ATLEAST(1)
Bob opposes/strengthens: new claim: 0.25-CNF-ATLEAST(1)
Alice refutes
Alice provides:
A
!A
B
Bob solves: J = (A,B) and satisfies 0.66 and Bob wins
Bob claims 0.66-CNF-ATLEAST(1)
Alice tries to refute
Alice provides:
A
!A
Bob provides(solves): J = {A} and satisfies 0.5 and Alice wins (refutes successfully)
Alice claims !1-CNF-LEAST(0.5)
Bob agrees
Bob claims 1-CNF-LEAST(0.5)
Alice agrees