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

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

Text

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

BibTeX

@misc{reference.wolfram_2020_satisfiableq, author="Wolfram Research", title="{SatisfiableQ}", year="2008", howpublished="\url{https://reference.wolfram.com/language/ref/SatisfiableQ.html}", note=[Accessed: 27-February-2021 ]}

BibLaTeX

@online{reference.wolfram_2020_satisfiableq, organization={Wolfram Research}, title={SatisfiableQ}, year={2008}, url={https://reference.wolfram.com/language/ref/SatisfiableQ.html}, note=[Accessed: 27-February-2021 ]}

CMS

Wolfram Language. 2008. "SatisfiableQ." Wolfram Language & System Documentation Center. Wolfram Research. https://reference.wolfram.com/language/ref/SatisfiableQ.html.

APA

Wolfram Language. (2008). SatisfiableQ. Wolfram Language & System Documentation Center. Retrieved from https://reference.wolfram.com/language/ref/SatisfiableQ.html