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-CNF(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 CNF(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 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-CNF(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-CNF(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-CNF(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-CNF(0) ) (increasing bound) !k-CNF(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) or P finishes with C, strengthens C: OP proposes C' (C' => C) OP finishes: tie if optimum reachedExample:

The innovation algorithm in operation. Alice claims: 1-CNF(0) Bob opposes/strengthens: new claim: 1-CNF(0.25) Alice refutes Alice provides: A !A B Bob solves: J = (A,B) and satisfies 0.66 and Bob wins Bob claims 1-CNF(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-CNF(0.5) Bob finishes Bob claims 1-CNF(0.5) Alice finishes