A module for representing and manipulating satisfiability formulas in Conjunctive Normal Form (CNF).
Summary
Types
An affirmed_literal() is a positive integer representing a variable that is
asserted to be true.
The set of variable ids introduced by Tseitin encoding.
See bindings/1.
A binding() maps a positive integer (the variable) to its original value.
A clause is a disjunction of literal()s.
A formula in Conjunctive Normal Form (CNF) is a conjunction of clauses,
where each clause() is a disjunction of literal()s.
Auxiliary definition clauses produced by Tseitin encoding.
A literal() is either an affirmed_literal() (a positive integer) or
a negated_literal() (a negative integer).
A negated_literal() is a negative integer representing a variable that is
asserted to be false.
A reverse binding maps a variable to its positive integer representation. This provides O(log n) lookup for variable-to-integer mappings.
See t/1.
A satisfiability formula in Conjunctive Normal Form (CNF) along with bindings that map the integers used in the CNF back to their original values.
Functions
Converts a boolean expression to a SAT formula in Conjunctive Normal Form (CNF).
Converts a SAT formula back to a boolean expression.
Formats a CNF formula to PicoSAT DIMACS format.
Types
@type affirmed_literal() :: pos_integer()
An affirmed_literal() is a positive integer representing a variable that is
asserted to be true.
@type auxiliaries() :: MapSet.t(pos_integer())
The set of variable ids introduced by Tseitin encoding.
Auxiliary ids appear in cnf/0 but never in bindings/1.
See bindings/1.
@type bindings(variable) :: %{required(pos_integer()) => variable}
A binding() maps a positive integer (the variable) to its original value.
@type clause() :: [literal(), ...]
A clause is a disjunction of literal()s.
A clause is satisfied if at least one of its literal()s is satisfied.
@type cnf() :: [clause()]
A formula in Conjunctive Normal Form (CNF) is a conjunction of clauses,
where each clause() is a disjunction of literal()s.
All clause()s of a CNF formula must be satisfied for the formula to be satisfied.
@type definitions() :: [clause()]
Auxiliary definition clauses produced by Tseitin encoding.
These clauses bind each auxiliary variable to the truth value of the
sub-expression it represents. They are a subset of cnf/0 and must
always hold; consumers performing implication tests must not negate
them.
@type literal() :: affirmed_literal() | negated_literal()
A literal() is either an affirmed_literal() (a positive integer) or
a negated_literal() (a negative integer).
@type negated_literal() :: neg_integer()
A negated_literal() is a negative integer representing a variable that is
asserted to be false.
@type reverse_bindings(variable) :: %{required(variable) => pos_integer()}
A reverse binding maps a variable to its positive integer representation. This provides O(log n) lookup for variable-to-integer mappings.
See t/1.
@type t(variable) :: %Crux.Formula{ auxiliaries: auxiliaries(), bindings: bindings(variable), cnf: cnf(), definitions: definitions(), reverse_bindings: reverse_bindings(variable) }
A satisfiability formula in Conjunctive Normal Form (CNF) along with bindings that map the integers used in the CNF back to their original values.
Functions
@spec from_expression(Crux.Expression.t(variable)) :: t(variable) when variable: term()
Converts a boolean expression to a SAT formula in Conjunctive Normal Form (CNF).
The CNF is produced via the Tseitin transformation: each compound
sub-expression gets a fresh auxiliary variable and a small set of
"definition" clauses that bind the auxiliary to the sub-expression's
truth value. The resulting CNF grows linearly with the size of the
input — the naive distributive-law approach can blow up
exponentially. Auxiliary variables never appear in :bindings or in
scenarios returned by Crux.solve/1 and Crux.satisfying_scenarios/2.
to_expression/1 reverses the encoding by substituting each auxiliary
with its definition and simplifying.
Examples
iex> import Crux.Expression
...> formula = Formula.from_expression(b(:a and :b))
...> formula.bindings
%{1 => :a, 2 => :b}
iex> Formula.to_expression(formula)
b(:a and :b)
iex> import Crux.Expression
...> formula = Formula.from_expression(b(:x or not :y))
...> formula.bindings
%{1 => :x, 2 => :y}
iex> Formula.to_expression(formula)
b(:x or not :y)@spec to_expression(formula :: t(variable)) :: Crux.Expression.t(variable) when variable: term()
Converts a SAT formula back to a boolean expression.
For Tseitin-encoded formulas (the output of from_expression/1), this
substitutes each auxiliary variable with its definition and simplifies
— recovering an expression equivalent to the original source.
Formulas constructed manually with no auxiliaries are walked
clause-by-clause, mapping each literal back through :bindings.
Examples
iex> import Crux.Expression
...> Formula.to_expression(Formula.from_expression(b(:a and :b)))
b(:a and :b)
iex> import Crux.Expression
...> Formula.to_expression(Formula.from_expression(b(:x or not :y)))
b(:x or not :y)
iex> formula = %Formula{
...> cnf: [[1, -2]],
...> bindings: %{1 => :x, 2 => :y},
...> reverse_bindings: %{x: 1, y: 2}
...> }
...>
...> Formula.to_expression(formula)
b(:x or not :y)Formats a CNF formula to PicoSAT DIMACS format.
Takes a formula struct and returns a string in the DIMACS CNF format that can be consumed by SAT solvers like PicoSAT.
The header reports the highest variable id used in the CNF, which includes Tseitin auxiliary variables.
Examples
iex> alias Crux.{Expression, Formula}
...> formula = Formula.from_expression(Expression.b(:a))
...> Formula.to_picosat(formula)
"p cnf 1 1\n1 0"