Algorithms and Data Fall 2011

Homework 5

Using an algorithm based on the quantifier game to make us better algorithm designers

Due date: October 19, 2011. At beginning of lecture.

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):

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.


Alice claims: 1/2-CNF-ATLEAST(1) 

Bob sends Alice  the CNF:

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
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:
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:
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

What to turn in:

A formula for tau(k). A polynomial time algorithm that is guaranteed to achieve tau(k). Input: CNF in CNF-ATLEAST(k), i.e., with clauses of at least length k. Output: an assignment that satisfies the fraction tau(k) of the clauses. Provide an asymptotic analysis of your algorithm using the big O notation. Provide a proof for the correctness of your tau(k) function and provide the game history of your innovation game with your partner. The innovation game should give you the necessary feedback to help you invent tau(k) and the algorithm.

Summary of Playground Design


Instance: CNF Solution: assignment to CNF valid: all variables assigned quality: fraction of satisfied clauses

Claimset for Domain

There are positive claims: f-CNF-ATLEAST(k) and negative claims !f-CNF-ATLEAST(k). Definition of the strengthening relation: f1-CNF-ATLEAST(k) strengthens f2-CNF-ATLEAST(k) if f1 > f2. !f1-CNF-ATLEAST(k) strengthens f2-CNF-ATLEAST(k) if f1 < f2.

Playground Design for earlier homeworks

HSR, Landau, Graphs (diamater,apd).