New in Wolfram Mathematica 7: Industrial-Strength Boolean Computation ◄ previous | next ►
Solve a Large Boolean Satisfiability Problem
Solve a Boolean satisfiability problem with 100000 variables.
In[1]:=

Click for copyable input
vars = Array[x, 100000];

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

SeedRandom[1];

expr = And @@ Table[Or @@ RandomSample[lits, 3], {10000}];

Style[Short[Boole[sat = SatisfiabilityInstances[expr, vars]], 70], 6]
Out[1]=



In[2]:=

Click for copyable input
expr /. Dispatch[Thread[vars -> sat[[1]]]]
Out[2]=