Cnf
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.
Subtopics
- 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.
