WOLFRAM

Wolfram Language & System Documentation Center
Wolfram Language Home Page »

SatisfiabilityInstances
✖
SatisfiabilityInstances

✖

attempts to find a choice of variables that makes the Boolean function bf yield True.

✖
SatisfiabilityInstances[expr,{a1,a2,…}]

attempts to find a choice of the ai that makes the Boolean expression expr be True.

✖

attempts to find m choices of variables that yield True.

Details and Options

Examples

open allclose all

Basic Examples  (3)Summary of the most common use cases

Generate a single instance where the Boolean expression is true:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-wli5i
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-i6wa10
Out[2]=2

Generate multiple instances; in this case only two instances exist:

In[3]:=3
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-bh696x
Out[3]=3
In[4]:=4
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-n1yqpe
Out[4]=4

Find 3 instances for a pure Boolean function:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-n2pccm
Out[1]=1

When the input is not satisfiable, an empty list is returned:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-fis4d
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-c4jbli
Out[2]=2

Scope  (1)Survey of the scope of standard use cases

Find all instances where the Boolean expression is true:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-mciq9v
Out[1]=1

Options  (1)Common values & functionality for each option

Method  (1)

By default, SatisfiabilityInstances automatically chooses the method to use:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-ckw1ug
In[4]:=4
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-7nxtwa
Out[4]=4

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

In[5]:=5
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-qbh361
Out[5]=5

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

In[6]:=6
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-dkc5v1
Out[6]=6

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

In[7]:=7
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-48kk67
Out[7]=7

Properties & Relations  (4)Properties of the function, and connections to other functions

A Boolean expression with n variables can have at most 2n instances:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-ovkkz7
Out[1]=1

Use SatisfiabilityCount to get an exact count of instances:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-guhkbk
Out[1]=1

SatisfiabilityInstances corresponds to True entries in BooleanTable:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-eorum
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-fa9xo6
Out[2]=2
In[3]:=3
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-z5tzj
Out[3]=3

Use FindInstance to find solutions to equations and inequalities:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-bn0ain
Out[1]=1
In[2]:=2
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-m4zsu
Out[2]=2

Neat Examples  (1)Surprising or curious use cases

A sampling of instances:

In[1]:=1
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-b3dirk
In[2]:=2
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-hj9s
Out[2]=2

The full list is longer:

In[3]:=3
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-bai8zj
Out[3]=3
In[4]:=4
✖
https://wolfram.com/xid/0bsv4c4bmsrrzvo2mt-bd3gap
Out[4]=4
Wolfram Research (2008), SatisfiabilityInstances, Wolfram Language function, https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html.
✖
Wolfram Research (2008), SatisfiabilityInstances, Wolfram Language function, https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html.

Text

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

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

CMS

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

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

APA

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

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

BibTeX

@misc{reference.wolfram_2025_satisfiabilityinstances, author="Wolfram Research", title="{SatisfiabilityInstances}", year="2008", howpublished="\url{https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html}", note=[Accessed: 29-March-2025 ]}

✖
@misc{reference.wolfram_2025_satisfiabilityinstances, author="Wolfram Research", title="{SatisfiabilityInstances}", year="2008", howpublished="\url{https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html}", note=[Accessed: 29-March-2025 ]}

BibLaTeX

@online{reference.wolfram_2025_satisfiabilityinstances, organization={Wolfram Research}, title={SatisfiabilityInstances}, year={2008}, url={https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html}, note=[Accessed: 29-March-2025 ]}

✖
@online{reference.wolfram_2025_satisfiabilityinstances, organization={Wolfram Research}, title={SatisfiabilityInstances}, year={2008}, url={https://reference.wolfram.com/language/ref/SatisfiabilityInstances.html}, note=[Accessed: 29-March-2025 ]}