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.
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.
Claim k-SAT(f): For all CNFs S with clauses of exactly length k (abbreviated CNF(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.
Refutation protocol: Bob sends Alice a CNF S in k-SAT 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 we use <= because f could be optimal.)
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-SAT(1/2)
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 !k-SAT(f): There exists a CNF S in CNF(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 k-SAT(f) 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 in each round. Oppose means either strengthening or refuting. Strengthening is proposing a stronger claim.
We note that we have two trivial starting points: k-SAT(0) ) (increasing bound) !k-SAT(1) (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. 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) and holds C-kind ball or P finishes with C,
P wins if optimum reached
strengthens C: OP proposes C' (C' => C)
OP finishes: tie if optimum reached
Example:
The innovation algorithm in operation.
Alice claims: 1-SAT(0)
Bob opposes/strengthens: new claim: 1-SAT(0.25)
Alice refutes
Alice provides:
A
!A
B
Bob provides(solves): J = (A,B) and satisfies 0.66 and Bob wins
Bob claims 1-SAT(0.66)
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-SAT(0.5)
Bob finishes
Bob claims 1-SAT(0.5)
Alice finishes
What to turn in:
The solution for k-SAT(tau(k)), i.e.,
the function tau(k) so that claim
k-SAT(tau(k)) can be neither refuted nor strengthened.
It is optimal.