SatisfiabilityInstances
attempts to find a choice of variables that makes the Boolean function bf yield True.
SatisfiabilityInstances[expr,{a1,a2,…}]
attempts to find a choice of the ai that makes the Boolean expression expr be True.
SatisfiabilityInstances[…,…,m]
attempts to find m choices of variables that yield True.
Details and Options
- SatisfiabilityInstances[…] gives {} if no choice of variables yields True.
- SatisfiabilityInstances[…,…,All] gives all choices of variables that yield True.
- The following Method settings can be used:
-
"BDD" binary decision diagram method "SAT" a SAT solver "TREE" a branch-and-evaluate method
Examples
open all close allBasic Examples (3)
Generate a single instance where the Boolean expression is true:
SatisfiabilityInstances[Equivalent[a, b], {a, b}]Equivalent[False, False]Generate multiple instances; in this case only two instances exist:
SatisfiabilityInstances[Equivalent[a, b], {a, b}, 4]Equivalent@@@%Find 3 instances for a pure Boolean function:
SatisfiabilityInstances[BooleanFunction[30, 3], 3]When the input is not satisfiable, an empty list is returned:
SatisfiabilityInstances[¬Implies[Implies[a, b]∧a, b], {a, b}]SatisfiableQ[¬Implies[Implies[a, b]∧a, b], {a, b}]Scope (2)
Find all instances where the Boolean expression is true:
SatisfiabilityInstances[a || b, {a, b}, All]Find an instance where the Boolean function is true:
SatisfiabilityInstances[BooleanFunction[21, 3]]BooleanFunction[21, 3]@@First[%]Options (1)
Method (1)
By default, SatisfiabilityInstances automatically chooses the method to use:
SeedRandom[1234];
vars = x /@ Range[25];
form = And@@Or@@@RandomChoice[Join[vars, Not /@ vars], {200, 5}];SatisfiabilityInstances[form, vars]//AbsoluteTimingWith Method"SAT", the input is converted to a conjunction of disjunctions and a SAT solver is used:
SatisfiabilityInstances[form, vars, Method -> "SAT"]//AbsoluteTimingWith Method"BDD", a BDD representation of the input is computed:
SatisfiabilityInstances[form, vars, Method -> "BDD"]//AbsoluteTimingWith Method"TREE", a simple branch-and-evaluate search method is used:
SatisfiabilityInstances[form, vars, Method -> "TREE"]//AbsoluteTimingProperties & Relations (4)
A Boolean expression with n variables can have at most 2n instances:
SatisfiabilityInstances[Xor[a, b, c], {a, b, c}, 2 ^ 3]Use SatisfiabilityCount to get an exact count of instances:
SatisfiabilityCount[Xor[a, b, c], {a, b, c}]SatisfiabilityInstances corresponds to True entries in BooleanTable:
BooleanTable[{Xor[a, b, c], {a, b, c}}, {a, b, c}]Last /@ Select[%, First[#] == True&]SatisfiabilityInstances[Xor[a, b, c], {a, b, c}, 2 ^ 3]Use FindInstance to find solutions to equations and inequalities:
FindInstance[x ^ 2 + y ^ 2 + z ^ 2 == -1 && z ^ 2 == 2x - 5 y, {x, y, z}]FindInstance[x ^ 2 + y z == 1 && x + 2y ≤ 3z + 1 && x y z > 7, {x, y, z}, Reals]Neat Examples (1)
inst = SatisfiabilityInstances[BooleanCountingFunction[97, 100], 10 ^ 4];Table[ArrayPlot[1 - Boole@Take[inst, {i, i + 100}]], {i, 1000, 9000, 1000}]SatisfiabilityCount[BooleanCountingFunction[97, 100]]N[%]Text
Wolfram Research (2008), SatisfiabilityInstances, Wolfram Language function, https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html.
CMS
Wolfram Language. 2008. "SatisfiabilityInstances." Wolfram Language & System Documentation Center. Wolfram Research. https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html.
APA
Wolfram Language. (2008). SatisfiabilityInstances. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html