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.

Details and Options

  • The following Method settings can be used:
  • "BDD"binary decision diagram method
    "SAT"a SAT solver
    "TREE"a branch-and-evaluate method

Examples

open allclose all

Basic Examples  (2)

Test whether Boolean expressions are satisfiable:

Test whether pure Boolean functions are satisfiable:

Options  (1)

Method  (1)

By default, SatisfiableQ 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)

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.

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

BibTeX

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

BibLaTeX

@online{reference.wolfram_2023_satisfiableq, organization={Wolfram Research}, title={SatisfiableQ}, year={2008}, url={https://reference.wolfram.com/language/ref/SatisfiableQ.html}, note=[Accessed: 02-December-2023 ]}