Independent Set (IS) is a decision problem that asks, given a graph, G(V,E), does G() have an independent set of size k? A set of vertices is independent if there are no edges joining any two vertices in the set.
IS is known to be NP-Complete. This can be proven by showing that 3SAT can be converted into an IS problem. There is a well known method for converting 3SAT to IS. This is one of many descriptions of the proof that can be found on the internet:
http://www.csie.ntu.edu.tw/~lyuu/complexity/2004/c_20041027.pdf
I describe how exclusive 3SAT (X3SAT) can be transformed into an IS problem. It turns out that X3SAT can be converted into a smaller graph than 3SAT.
Assume we have an X3SAT instance with n literals and m clauses. Assign a vertex to each literal. If literal a appears in a clause with literal b then create an edge between vertex a and b. If the literals a and ~a both occur in the instance then create an edge between them.
We will assign a weight to each vertex. Count the number of times a literal occurs in the X3SAT instance. This count is the weight we assign to the vertex.
Consider the set of vertices not in the IS. This set forms a vertex cover (VC). The X3SAT instance is satisfiable if and only if the resulting graph has an independent set whose weights sum to the number of clauses, m, and the VC does not contain a literal and its inverse. The sum of weights of the VC must be 2*m.
I describe a method to solve X3SAT instances by finding the IS of a graph.
Example problem instance with 5 clauses and 11 literals:
(a1,b0,c0) (a0,d1,e1) (b1,d0,f1) (c1,e1,f1) (a1,f1,g1)
Count the number of times each literal appears in the instance.
Literal Count
a0(1)
a1(2)
b0(1)
b1(1)
c0(1)
c1(1)
d0(1)
d1(1)
e1(2)
f1(3)
g1(1)
Create a table with a row for each vertex, v.
This table has two columns, one for the vertex set of v, V(v),
and one for the neighbor set of v, NS(v).
Initialize the vertex set by putting the vertex for that row into the set. Place the neighbors of vertex v into NS(v). This would include ~v, if ~v exists in the X3SAT instance, and any literal that appears in a clause with v.
We keep track of the sum of the literal counts for both V(v) and NS(v).
| Vertex Set (Count) | Neighbor Set (Count) |
|---|---|
| a0(1) | a1 d1 e1 (5) |
| a1(2) | a0 b0 c0 f1 g1 (7) |
| b0(1) | a1 b1 c0 (3) |
| b1(1) | b0 d0 f1 (4) |
| c0(1) | a1 b0 c1 (3) |
| c1(1) | c0 e1 f1 (6) |
| d0(1) | b1 d1 f1 (4) |
| d1(1) | a0 d0 e1 (6) |
| e1(2) | a0 c1 d1 f1 (6) |
| f1(3) | a1 b1 c1 d0 e1 g1 (8) |
| g1(1) | a1 f1 (5) |
We use the following Reduction Rules, RR(), to add vertices to the V() and NS() columns or remove rows from the table.
| Reduction Rules | |
|---|---|
| 0) | The instance is unsolvable if all rows are removed. |
| 1) | If the sum of counts in V(v) > m then v can't be in IS. Remove row v and add v to all remaining NS. If V(~v) exists then add V(~v) to all remaining VS and NS(~v) to all remaining NS. |
| 2) | If the sum of counts in NS(v) > 2m then v can't be in IS. Remove row v and add v to all remaining NS. If V(~v) exists then add V(~v) to all remaining VS and NS(~v) to all remaining NS. |
| 3) | If V(v) or NS(v) contains a literal and its inverse then v can't be in IS. Remove row v and add v to all remaining NS. If V(~v) exists then add V(~v) to all remaining VS and NS(~v) to all remaining NS. |
| 4) | If V(S) contains two members of a clause then v can't be in IS. Remove row v and add v to all remaining NS. If V(~v) exists then add V(~v) to all remaining VS and NS(~v) to all remaining NS. |
| 5) | If NS(v) contains three members of a clause then v can't be in IS. Remove row v and add v to all remaining NS. If V(~v) exists then add V(~v) to all remaining VS and NS(~v) to all remaining NS. |
| 6) | If V(v) and NS(v) contain the same literal then v can't be in IS. Remove row v and add v to all remaining NS. If V(~v) exists then add V(~v) to all remaining VS and NS(~v) to all remaining NS. |
| 7) | If NS(v) contains two members of a clause then the third member of the clause, w, must be in IS if v is in IS. Add V(w) to V(v) and NS(w) to NS(v). |
| 8) | If NS(v) contains w and ~w exists in the instance then ~w must be in the IS if v is in the IS. Add V(~w) to V(v) and add NS(~w) to NS(v). |
| 9) | If NS(v) contains every member of NS(w) then w must be in the IS if v is in IS. Add V(w) to V(v). |
These reduction rules can remove rows. If the row for vertex v is removed then literal v does not appear in any satisfying assignment.
RR(7) is the unit clause rule often used in SAT solvers. As far as I know, RR(1), RR(2), and RR(8) are new reduction rules for X3SAT.
Because this problem has 5 clauses, we want to find a set of vertices that form an independent set and the sum of the literal counts in this set must equal 5. This IS will contain the literals that are true and the VC will contain the literals that are false.
We will choose one or more vertex sets, V(), to be in the IS, and the corresponding NS() will be in the VC.
Start with the first row, a0:
| v | V(v) | NS(v) |
|---|---|---|
| a0 | a0 (1) | a1 d1 e1 (5) |
Apply the reduction rules, RR(), to this row in numeric order. Continue applying the RR() until no more apply, then move to the next row. Continue this process until the RR() can no longer be applied to any row or a solution is found.
RR(8) is the first rule that applies to row a0. NS(a0) contains d1 and e1 (we can ignore a1). e0 doesn't exist in this instance, but d0 does.
Apply RR(8): V(a0)+V(d0), NS(a0)+NS(d0)
| v | V(v) | NS(v) |
|---|---|---|
| a0 | a0 d0 (2) | a1 b1 d1 e1 f1 (9) |
Start from the beginning of the RR(). The first rule that applies now is RR(7). NS(a0) contains two members of clauses (c1,e1,f1) and (a1,f1,g1). We can ignore clauses with a0 and d0.
Apply RR(7): V(a0)+V(c1)+V(g1), NS(a0)+NS(c1)+NS(g1)
| v | V(v) | NS(v) |
|---|---|---|
| a0 | a0 c1 d0 g1 (4) | a1 b1 c0 d1 e1 f1 (10) |
Now, the lowest numbered rule that applies is again RR(7). NS(a0) contains two members of (a1,b0,c0).
Apply RR(7): V(a0)+V(b0), NS(a0)+NS(b0)
| v | V(v) | NS(v) |
|---|---|---|
| a0 | a0 b0 c1 d0 g1 (5) | a1 b1 c0 d1 e1 f1 (10) |
We have found a solution:
a0 b0 c1 d0 g1
Since row a0 converged to a solution, the literal a0 appears in exactly one solution. If a0 were to appear in more than one solution, we would have to add V(a0) to some other row to get a satisfying IS.
We can determine if literal a1 appears in any solutions.
| v | V(v) | NS(v) |
|---|---|---|
| a1 | a1 (2) | a0 b0 c0 f1 g1 (7) |
NS(a1) contains b0 and c0.
Apply RR(8): V(a1)+V(b1)+V(c1), NS(a1)+NS(b1)+NS(c1)
| v | V(v) | NS(v) |
|---|---|---|
| a1 | a1 b1 c1 (4) | a0 b0 c0 d0 e1 f1 g1 (10) |
NS(a1) contains two members of (a0,d1,e1).
Apply RR(7): V(a1)+V(d1), NS(a1)+NS(d1)
| v | V(v) | NS(v) |
|---|---|---|
| a1 | a1 b1 c1 d1 (5) | a0 b0 c0 d0 e1 f1 g1 (10) |
We have found another solution.
a1 b1 c1 d1
Since this row converged, a1 appears in only one solution. Since a0 and a1 both only appear in one solution, this X3SAT instance can't have more than two solutions.
Solutions to the X3SAT instance:
(a1,b0,c0) (a0,d1,e1) (b1,d0,f1) (c1,e1,f1) (a1,f1,g1)
a0 b0 c1 d0 g1 (5)
a1 b1 c1 d1 (5)
Notice that c0 doesn't appear in either solution.
| v | V(v) | NS(v) |
|---|---|---|
| c0 | c0 (1) | a1 b0 c1 (3) |
NS(c0) contains a1 and b0.
Apply RR(8): V(c0)+V(a0)+V(b1), NS(c0)+NS(a0)+NS(b1)
| v | V(v) | NS(v) |
|---|---|---|
| c0 | a0 b1 c0 (3) | a1 b0 c1 d0 d1 e1 (7) |
NS(c0) now contains d0 and d1.
RR(3) allows us to remove row c0. We add c0 to all of the remaining NS. Since V(c1) exists, we add V(c1) to all remaining VS and NS(c1) to all remaining NS.
Row c1 won't converge to a solution.
| v | V(v) | NS(v) |
|---|---|---|
| c1 | c1 (1) | c0 e1 f1 (6) |
None of the reduction rules apply to this row. We will have to add V(c1) to the VS of some other row to find a solution.
Completing the entire table (and removing all rows not in any solution) we get:
| v | V(v) | NS(v) |
|---|---|---|
| a0 | a0 b0 c1 d0 g1 (5) | a1 b1 c0 d1 e1 f1 (10) |
| a1 | a1 b1 c1 d1 (5) | a0 b0 c0 d0 e1 f1 g1 (10) |
| b0 | a0 b0 c1 d0 g1 (5) | a1 b1 c0 d1 e1 f1 (10) |
| b1 | a1 b1 c1 d1 (5) | a0 b0 c0 d0 e1 f1 g1 (10) |
| c1 | c1 (1) | c0 e1 f1 (6) |
| d1 | a1 b1 c1 d1 (5) | a0 b0 c0 d0 e1 f1 g1 (10) |
| g1 | a0 b0 c1 d0 g1 (5) | a1 b1 c0 d1 e1 f1 (10) |
The worst case for this method is when every literal appears in at least two satisfying assignments. In the worst case, this becomes a subset sum problem which is known to be NP-Complete.