Thursday, January 27, 2011

Using SAT solver to find independent sets

Here's a simple graph and all of its independent vertex sets



You can use SatisfiabilityInstances to get them as follows

gg = GridGraph[{2, 3}];
edge2clause[e_] := ! (e[[1]] && e[[2]]);
clauses = edge2clause /@ EdgeList[gg];
formula = And @@ clauses;
vars = VertexList[gg];
instances = SatisfiabilityInstances[formula, vars, 1000];
independentSets = Extract[vars, Position[#, True]] & /@ instances


Notebook

1 comment: