In class, we have shown an m-to-1 reduction from 3SAT to IDSET. hence,
it provides an algorithm to decide satis ability for a 3SAT Boolean formula
through IDSET. In this project, you shall implement the algorithm using any
high level programming language that you are comfortable with. Here are a
number of steps that you need to implement.
1. You will start with a 3SAT Boolean formula F over m Boolean vari-
ables, for some m, and with k clauses, for some k. Here, you need choose a
good data structure for the formula. You may use the following example to
test your code:
F1^F2^F3^F4^F5
with F1 = x1_ x2_x3, F2 = x1_ x4_x2, F3 = x4_ x2_ x3, F4 = x2_ x3_x1,
and F5 = x1 _ x3 _x4. For this example formula, we have m = 4 (four
variables) and k = 5 ( ve clauses F1; ;F5).
2. Using the m-to-1 reduction from 3SAT to IDSET presented in class,
you will end up with a graph G with 3k nodes. Now, F is satis able i G
has IDSET of size k. You will in this step implement a function that takes
F as input and returns the resulting G. For the example formula in step 1,
the G will have 15 nodes.
3. To decide whether the G may have an IDSET of size k, you need
implement a function that takes G and k as input, and returns an IDSET
of size k if exists. To do this, you may enumerate all subsets of k distinct
nodes in G and check whether there is a subset in the enumeration that
form. an IDSET (look carefully on the de nition of IDSET). Of course, the
implementation can be improved a little by not enumerating all the subsets.
In fact, you need only enumerating all the k nodes where each belongs to a
triangle (see the detail of the reduction). You must incorporate this optimized
step in your implementation.
4. You need also implement a function that takes the IDSET of size k
(if exists) returned from the function in step 3, and translates the IDSET
into a Boolean assignment to the 3SAT Boolean formula F and veri es that
the assignment indeed satis es F.
5. Making use of all these functions that are implemented, you can write
a main program to check whether a 3SAT Boolean formula is satis able or
not. If it is satis able, print out a satisfying assignment.