New in Wolfram Mathematica 7: Industrial-Strength Boolean Computation ◄ previous | next ►
Solve a Boolean Satisfiability Problem
Find a truth vector satisfying a randomly generated expression in conjunctive normal form.
In[1]:=

Click for copyable input
vars = Array[Subscript[x, #] &, 12];

lits = Join[vars, Not /@ vars];

SeedRandom[0];

Style[TraditionalForm[

  expr = And @@ Table[Or @@ RandomSample[lits, 6], {100}]], 6]
Out[1]=



In[2]:=

Click for copyable input
sat = SatisfiabilityInstances[expr, vars]
Out[2]=



In[3]:=

Click for copyable input
expr /. Thread[vars -> First[sat]]
Out[3]=