Boolean Computation

Building on its core symbolic architecture, the Wolfram Language gives immediate access to the latest in industrial-strength Boolean computation. With highly general symbolic representations of Boolean functions, with full support for "don't-care" arguments and values, the Wolfram Language provides state-of-the-art Boolean function transformation, minimization, elimination, satisfiability, and analysis, making possible verification, testing, and other applications involving hundreds to hundreds of thousands of variables.

Basic Boolean Operators

(RefLink[True, paclet:ref/True]), (RefLink[False, paclet:ref/False]) — symbolic truth values

(RefLink[Boole, paclet:ref/Boole]) — convert symbolic truth values to 0 and 1

Special Boolean Functions

(RefLink[BooleanCountingFunction, paclet:ref/BooleanCountingFunction]) — k out of n variables true

(RefLink[BooleanConsecutiveFunction, paclet:ref/BooleanConsecutiveFunction]) — consecutive k out of n variables true

General Boolean Functions

(RefLink[BooleanFunction, paclet:ref/BooleanFunction]) — general Boolean function (from IDs, mappings with "don't cares", ...)

(RefLink[BooleanMinterms, paclet:ref/BooleanMinterms]), (RefLink[BooleanMaxterms, paclet:ref/BooleanMaxterms]) — combinations of minterms, maxterms

(RefLink[Conjunction, paclet:ref/Conjunction]), (RefLink[Disjunction, paclet:ref/Disjunction]) — AND, OR with respect to a list of variables (cf. ∑, ∏)

Predicates on Lists

Boolean Structure

(RefLink[BooleanTable, paclet:ref/BooleanTable]) — create a truth vector or general truth table

(RefLink[BooleanVariables, paclet:ref/BooleanVariables]) — find the variables in a Boolean expression

(RefLink[UnateQ, paclet:ref/UnateQ]) — test whether a Boolean expression is unate (monotone)

Visualization

(RefLink[RulePlot, paclet:ref/RulePlot]) — visualize a Boolean function

Conversion & Minimization

(RefLink[BooleanConvert, paclet:ref/BooleanConvert]) — convert to a specified format (CNF, DNF, ESOP, NOR, BFF, ...)

(RefLink[BooleanMinimize, paclet:ref/BooleanMinimize]) — find a minimal Boolean form

Boolean Function Testing

(RefLink[SatisfiableQ, paclet:ref/SatisfiableQ]) — test whether any input to a function can give (RefLink[True, paclet:ref/True])

(RefLink[SatisfiabilityCount, paclet:ref/SatisfiabilityCount]) — count how many possible inputs give (RefLink[True, paclet:ref/True])

(RefLink[SatisfiabilityInstances, paclet:ref/SatisfiabilityInstances]) — find instances of inputs that give (RefLink[True, paclet:ref/True])

(RefLink[TautologyQ, paclet:ref/TautologyQ]) — test whether all possible inputs give (RefLink[True, paclet:ref/True])

Predicate Calculus

(RefLink[ForAll, paclet:ref/ForAll]) ((RefLink[∀, paclet:ref/ForAll])), (RefLink[Exists, paclet:ref/Exists]) ((RefLink[∃, paclet:ref/Exists])) — quantify over Boolean variables

(RefLink[Resolve, paclet:ref/Resolve]) — eliminate quantified variables from a Boolean expression

(RefLink[LogicalExpand, paclet:ref/LogicalExpand]) — expand expressions involving Boolean operators and equations

(OrangeLink[Iterated Boolean Systems », paclet:guide/ComputationalSystemsAndDiscovery])

(OrangeLink[Bit Vector Operations », paclet:guide/BitwiseOperations])

Numerical Boolean Computation

(RefLink[Nearest, paclet:ref/Nearest]), (RefLink[FindClusters, paclet:ref/FindClusters]) — operate on Boolean vectors

(RefLink[Minimize, paclet:ref/Minimize]), (RefLink[Maximize, paclet:ref/Maximize]) — Boolean optimization