SatisfiabilityInstances

SatisfiabilityInstances[bf]

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

Examples

open allclose all

Basic Examples  (3)

Generate a single instance where the Boolean expression is true:

Generate multiple instances; in this case only two instances exist:

Find 3 instances for a pure Boolean function:

When the input is not satisfiable, an empty list is returned:

Scope  (1)

Find all instances where the Boolean expression is true:

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:

Neat Examples  (1)

A sampling of instances:

The full list is longer:

Wolfram Research (2008), SatisfiabilityInstances, Wolfram Language function, https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html.

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

BibTeX

@misc{reference.wolfram_2024_satisfiabilityinstances, author="Wolfram Research", title="{SatisfiabilityInstances}", year="2008", howpublished="\url{https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html}", note=[Accessed: 21-November-2024 ]}

BibLaTeX

@online{reference.wolfram_2024_satisfiabilityinstances, organization={Wolfram Research}, title={SatisfiabilityInstances}, year={2008}, url={https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html}, note=[Accessed: 21-November-2024 ]}