In class we saw that if we had a black box for solving the YES/NO Clique problem, we could use that to solve the Optimization Clique problem to actually find the largest clique. We now want to do a similar thing for SAT.

Suppose you had a black-box for solving the BOOLEANSAT problem i.e. this BOOLEANSAT() black box took as input a conjunctive normal form formula (a CNF formula is written as AND of ORs) F and produced as output a YES/NO answer i.e. BOOLEANSAT(F) would return YES if F has some satisfying assignment, and NO if F has no satisfying assignment. Note that what we are calling BOOLEANSAT here is the same as what we have just been calling SAT earlier. Now we look at a slightly different problem GET SAT(). In this problem, we get as input a CNF formula G which we know is satisfiable. The output should be a satisfying assignment i.e. an assignment which assigns either true or false to every variable of G such that G as a whole becomes true.

GET SAT() is clearly a NP-hard problem. However, if you had a black box for BOOLEANSAT(), then this problem can be solved in polynomial time - you have to describe how to do this. Your job is to clearly describe an algorithm which will take as input a satisfiable CNF formula G and (using the BOOLEANSAT() black box) find an assignment which satisfies the formula G. Trace the execution of your algorithm on a small example.

Hint:

Your algorithm for GET SAT will make many calls to the BOOLEANSAT blackbox.

Remember that BOOLEANSAT just gives YES/NO answers and does not actually produce a satisfying assignment.

Think of this as an iterative algorithm, where in a single iteration you try to find the truth value of one single boolean variable. You have to figure out what question you can ask BOOLEANSAT so as to get the truth value of one boolean variable.