WOLFRAM

Wolfram Language & System Documentation Center

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
Details and Options Details and Options
Examples  
Basic Examples  
Options  
Method  
Properties & Relations  
See Also
Related Guides
History
Cite this Page

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 all close all

Basic Examples  (2)

Test whether Boolean expressions are satisfiable:

Wolfram Language code: SatisfiableQ[(a || b) && (!a || !b), {a, b}]
Wolfram Language code: SatisfiableQ[(a && b) && (!a || !b), {a, b}]

Test whether pure Boolean functions are satisfiable:

Wolfram Language code: SatisfiableQ[BooleanFunction[110, 3]]
Wolfram Language code: SatisfiableQ[BooleanFunction[0, 20]]

Options  (1)

Method  (1)

By default, SatisfiableQ automatically chooses the method to use:

Wolfram Language code: SeedRandom[1234]; vars = x /@ Range[25]; form = And@@Or@@@RandomChoice[Join[vars, Not /@ vars], {200, 5}];
Wolfram Language code: SatisfiableQ[form, vars]//AbsoluteTiming

With Method"SAT", the input is converted to a conjunction of disjunctions and a SAT solver is used:

Wolfram Language code: SatisfiableQ[form, vars, Method -> "SAT"]//AbsoluteTiming

With Method"BDD", a BDD representation of the input is computed:

Wolfram Language code: SatisfiableQ[form, vars, Method -> "BDD"]//AbsoluteTiming

With Method"TREE", a simple branch-and-evaluate search method is used:

Wolfram Language code: SatisfiableQ[form, vars, Method -> "TREE"]//AbsoluteTiming

Properties & Relations  (4)

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

Wolfram Language code: BooleanTable[Xor[a, b], {a, b}]
Wolfram Language code: SatisfiableQ[Xor[a, b], {a, b}]

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

Wolfram Language code: SatisfiabilityCount[¬Implies[Implies[a, b]∧¬b, ¬a]]
Wolfram Language code: SatisfiableQ[¬Implies[Implies[a, b]∧¬b, ¬a]]

Use SatisfiabilityInstances to get explicit instances:

Wolfram Language code: SatisfiabilityInstances[Xor[a, b], {a, b}]

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

Wolfram Language code: ¬TautologyQ[¬Xor[a, b], {a, b}]
Wolfram Language code: SatisfiableQ[Xor[a, b], {a, b}]
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_2026_satisfiableq, author="Wolfram Research", title="{SatisfiableQ}", year="2008", howpublished="\url{https://reference.wolfram.com/language/ref/SatisfiableQ.html}", note=[Accessed: 12-June-2026]}

BibLaTeX

@online{reference.wolfram_2026_satisfiableq, organization={Wolfram Research}, title={SatisfiableQ}, year={2008}, url={https://reference.wolfram.com/language/ref/SatisfiableQ.html}, note=[Accessed: 12-June-2026]}