Our representation (syntax and semantics) for conjunctive normal form formulas.

To express what it means to call a SAT solver, we need a representation and a semantics for Boolean formulas in conjunctive normal form. Our syntax is as follows:

- A
**variable**is a natural number. To help keep variables separate from literals, we represent them varps, instead of natps. - A
**literal**represents either a variable or a negated variable. We represent these using a typical numeric encoding: the least significant bit is the negated bit, and the remaining bits are the variable. See litp. - A
**clause**is a disjunction of literals. We represent these as ordinary lists of literals. See lit-listp. - A
**formula**is a conjunction of clauses. We represent these using lit-list-listp.

The semantics of these formulas are given by eval-formula.

- Litp
- Representation of a literal (a Boolean variable or its negation).
- Varp
- Representation of a Boolean variable.
- Env$
- A bit array that serves as the environment for eval-formula.
- Eval-formula
- Semantics of CNF formulas.
- Max-index-formula
- Maximum index of any identifier used anywhere in a formula.
- Max-index-clause
- Maximum index of any identifier used anywhere in a clause.
- Formula-indices
- Collect indices of all identifiers used throughout a formula.
- Clause-indices
- Collect indices of all identifiers used throughout a clause.