SatisfiableQ

gives True if a combination of values of variables exists that makes the Boolean function bf yield True.

SatisfiableQ[expr,{a₁,a₂,…}]

gives True if a combination of values of the a_i exists that makes the Boolean expression expr yield True.

Examples

open allclose all

Test whether Boolean expressions are satisfiable:

Test whether pure Boolean functions are satisfiable:

An expression is satisfiable if it is true for some variable assignments:

An expression of variables is satisfiable if the SatisfiabilityCount is greater than 0:

Use SatisfiabilityInstances to get explicit instances:

SatisfiableQ[f] is equivalent to ¬TautologyQ[¬f]:

Top