This is documentation for Mathematica 8, which was
based on an earlier version of the Wolfram Language.

# SatisfiabilityCount

 SatisfiabilityCount[bf]counts the number of possible combinations of variable values that yield True when supplied as arguments to the Boolean function bf. SatisfiabilityCount counts the number of possible combinations of the that make the Boolean expression expr be true.
Count the number of cases for which yields true:
This corresponds to the number of times True appears in the truth table:
Count the number of truth cases for a pure Boolean function:
The corresponding table:
Count the truth instances in an expression with 2000 variables:
Count the number of cases for which yields true:
 Out[1]=
This corresponds to the number of times True appears in the truth table:
 Out[2]=
 Out[3]=

Count the number of truth cases for a pure Boolean function:
 Out[1]=
The corresponding table:
 Out[2]=
 Out[3]=

Count the truth instances in an expression with 2000 variables:
 Out[1]=
 Out[2]=
 Applications   (1)
Compute the probability for an event as the ratio of true cases to total cases:
The probabilities for some events:
The probability that between 20 and 40 variables out of 100 are true:
Show that :
SatisfiabilityCount for a function of variables is always between and :
SatisfiabilityCount efficiently counts the number of True elements in BooleanTable:
In this case, the BooleanTable would have elements:
SatisfiableQ efficiently tests whether SatisfiabilityCount is greater than zero:
TautologyQ efficiently tests whether SatisfiabilityCount is for an n variable function:
The SatisfiabilityCount for primitives of n variables is simple; for And it is always :
For Or it is :
For Nand it is :
For Nor it is :
For Xor it is :
For Xnor it is :
For Equivalent it is :
For Majority it is for odd and for even :
The size of the truth set for BooleanCountingFunction is the length of Subsets:
The size of the truth set for BooleanCountingFunction can be given by a combinatorial sum:
SatisfiabilityCount for an indexed BooleanFunction is given by DigitCount:
For n variables the number is given by DigitCount of Mod:
SatisfiabilityCount for BooleanMinterms is given by the length of the index list:
For BooleanMaxterms it is given by minus the length of the index list:
Use SatisfiabilityInstances to find explicit instances:
Get three instances:
Use CountRoots to count the number of polynomial roots in a real interval:
Or a complex rectangle:
Count the number of truth instances for all Boolean functions of two variables:
Three variables:
Four variables:
New in 7