Wolfram Language Paclet Repository
Community-contributed installable additions to the Wolfram Language
SAT
Definition of a SAT solver implemented in Pi-machine.
PiSAT | make a term that checks satisfiability of a given reversible boolean combinator |
XXXX.
Import paclet context and predefined SAT program with examples:
In[29]:=
Needs["WolframInstitute`PiMachine`"]
In[28]:=
Needs["WolframInstitute`PiMachine`SAT`"]
Verify that formula is not satisfiable:
a∧b⊻a∧b
In[15]:=
SatisfiableQ[a∧b⊻a∧b]
Out[15]=
False
Check that is computes :
Ex1
{,a,b}{a∧b⊻a∧b,a,b}
In[21]:=
AssociationMap[Ex1,Drop[PiBoolTerms[3],4]]
Out[21]=
⊗⊗⊗⊗,⊗⊗⊗⊗,⊗⊗⊗⊗,⊗⊗⊗⊗
The type of SAT solver program is :
In[31]:=
PiSAT[Ex1]["Type"]
Out[31]=
Evaluating non-satisfiable example results in exception:
In[11]:=
 | PiEval |
 | PiTerm |
| PiOne |
Out[11]=
error
The is satisfiable:
a∧b⊻a∨b
In[16]:=
SatisfiableQ[a∧b⊻a∨b]
Out[16]=
True
In[22]:=
AssociationMap[Ex2,Drop[PiBoolTerms[3],4]]
Out[22]=
⊗⊗⊗⊗,⊗⊗⊗⊗,⊗⊗⊗⊗,⊗⊗⊗⊗
In[12]:=
| PiEval |
| PiTerm |
| PiOne |
Out[12]=
1
⊳
Two more examples:
In[18]:=
SatisfiableQ[(a∧b)∧(a⊻b)]
Out[18]=
False
In[23]:=
AssociationMap[Ex3,Drop[PiBoolTerms[3],4]]
Out[23]=
⊗⊗⊗⊗,⊗⊗⊗⊗,⊗⊗⊗⊗,⊗⊗⊗⊗
In[14]:=
| PiEval |
| PiTerm |
| PiOne |
Out[14]=
error
In[19]:=
SatisfiableQ[(a∨b)∧(a⊻b)]
Out[19]=
True
In[24]:=
AssociationMap[Ex4,Drop[PiBoolTerms[3],4]]
Out[24]=
⊗⊗⊗⊗,⊗⊗⊗⊗,⊗⊗⊗⊗,⊗⊗⊗⊗
In[10]:=
| PiEval |
| PiTerm |
| PiOne |
Out[10]=
1
⊳
""