Crux.Formula (crux v0.1.2)
View SourceA 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.
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.
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.
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 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{ bindings: bindings(variable), cnf: cnf(), 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).
Examples
iex> import Crux.Expression
...> expression = b(:a and :b)
...> Formula.from_expression(expression)
%Formula{
cnf: [[1], [2]],
bindings: %{1 => :a, 2 => :b},
reverse_bindings: %{a: 1, b: 2}
}
iex> expression = b(:x or not :y)
...> Formula.from_expression(expression)
%Formula{
cnf: [[1, -2]],
bindings: %{1 => :x, 2 => :y},
reverse_bindings: %{x: 1, y: 2}
}@spec to_expression(formula :: t(variable)) :: Crux.Expression.cnf(variable) when variable: term()
Converts a SAT formula back to a boolean expression.
Examples
iex> formula = %Formula{
...> cnf: [[1], [2]],
...> bindings: %{1 => :a, 2 => :b},
...> reverse_bindings: %{a: 1, b: 2}
...> }
...>
...> Formula.to_expression(formula)
b(:a and :b)
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.
Examples
iex> alias Crux.{Expression, Formula}
...> formula = Formula.from_expression(Expression.b(:a and :b))
...> Formula.to_picosat(formula)
"p cnf 2 2\n1 0\n2 0"