SatisfiableQ

SatisfiableQ[bf]

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

SatisfiableQ[expr,{a1,a2,…}]

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

Examples

open allclose all

Basic Examples  (2)

Test whether Boolean expressions are satisfiable:

Test whether pure Boolean functions are satisfiable:

Properties & Relations  (4)

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]:

Introduced in 2008
 (7.0)