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)
Options (1)
Method (1)
By default, SatisfiabilityInstances automatically chooses the method to use:
With Method"SAT", the input is converted to a conjunction of disjunctions and a SAT solver is used:
With Method"BDD", a BDD representation of the input is computed:
With Method"TREE", a simple branch-and-evaluate search method is used:
Properties & Relations (4)
A Boolean expression with n variables can have at most 2n instances:
Use SatisfiabilityCount to get an exact count of instances:
SatisfiabilityInstances corresponds to True entries in BooleanTable:
Use FindInstance to find solutions to equations and inequalities:
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