# `Crux.Formula`
[🔗](https://github.com/ash-project/crux/blob/v0.1.3/lib/crux/formula.ex#L5)

A module for representing and manipulating satisfiability formulas in
Conjunctive Normal Form (CNF).

# `affirmed_literal`

```elixir
@type affirmed_literal() :: pos_integer()
```

An `affirmed_literal()` is a positive integer representing a variable that is
asserted to be true.

# `auxiliaries`

```elixir
@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`.

# `bindings`

```elixir
@type bindings() :: bindings(term())
```

See `bindings/1`.

# `bindings`

```elixir
@type bindings(variable) :: %{required(pos_integer()) => variable}
```

A `binding()` maps a positive integer (the variable) to its original value.

# `clause`

```elixir
@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.

# `cnf`

```elixir
@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.

# `definitions`

```elixir
@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.

# `literal`

```elixir
@type literal() :: affirmed_literal() | negated_literal()
```

A `literal()` is either an `affirmed_literal()` (a positive integer) or
a `negated_literal()` (a negative integer).

# `negated_literal`

```elixir
@type negated_literal() :: neg_integer()
```

A `negated_literal()` is a negative integer representing a variable that is
asserted to be false.

# `reverse_bindings`

```elixir
@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.

# `t`

```elixir
@type t() :: t(term())
```

See `t/1`.

# `t`

```elixir
@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.

# `from_expression`

```elixir
@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)

# `to_expression`

```elixir
@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)

# `to_picosat`

```elixir
@spec to_picosat(t()) :: String.t()
```

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"

---

*Consult [api-reference.md](api-reference.md) for complete listing*