Boolean abstraction and SAT integration

Boolean abstraction and SAT integration#

Primo’s SMT layer translates Boolean terms into clauses and remembers what the SAT literals mean. The SAT layer owns propositional search through CaDiCaL; it receives no core terms or SMT-LIB syntax. This chapter follows that boundary from an assertion to a SAT answer. The architecture overview places it in a query, and the core chapter explains term identity. The DPLL(T) chapter continues through theory callbacks and the checks needed before that SAT answer becomes an SMT answer.

The owning implementation is BooleanClausifier. The separately named Abstraction is an empty scaffold; it does not own the working term-to-literal map.

Representation and ownership#

Object and code	Representation	Ownership and validity
sat::Lit	Signed 32-bit integer: `v` or `-v` for positive variable ID `v`	Contains no term, backend identity, or lifetime guard. Zero is not a clause literal.
sat::Clause	Vector of literals, interpreted as a disjunction	`add_clause` submits it to the backend; an empty clause is false.
BooleanClausifier::Implementation	Dense term-indexed literal/registry-index/polarity arrays, atom vector, and Boolean-domain bookkeeping	Owns the maps; borrows one backend and one term manager, which must outlive it.
TheoryAtom	Literal, `TermId`, syntactic polarity flags, and a both-polarities relevance flag	Entry in an SMT-owned vector; its name does not imply that every entry requires theory reasoning.
CadicalBackend	CaDiCaL solver, callback adapters, variable accounting, last result, and counters	Owns the solver and adapters; adapters borrow the connected propagator and terminator.

The mapping is local to a clausifier/backend pair. Repeated encoding of a term reuses its literal. Negation can reuse the same variable with the opposite sign, so the relationship is not one fresh SAT variable per TermId. A SAT variable is not a TermId and must not be interpreted as one.

ensure_term_index grows the dense arrays as new terms appear. Atom registration can grow the atom vector; references returned by ensure_theory_atom and elements obtained through theory_atoms() must not be kept across operations that can append entries. Copy the IDs/literals needed, then reacquire entries. The core term-reference invalidation rules also apply to any helper that creates terms.

Literal range and exhaustion#

Lit uses a signed 32-bit value. Positive variable IDs therefore have a representational upper bound of 2³¹ − 1 (2,147,483,647); negation changes the sign, not the variable ID. Zero is reserved, and INT32_MIN cannot be a valid literal because its positive counterpart is not representable. This bounds variable IDs, not the number of clauses or literal occurrences.

The installed CaDiCaL API also requires 32-bit literals and excludes INT_MIN. The representational bound is not a promise that the backend can allocate that many variables. Widening only Primo’s Lit would not widen that API.

There is a concrete hardening gap: new_observed_var computes max(max_var_, solver_->vars()) + 1 in signed arithmetic without an explicit capacity check. The fallback branches of new_var also increment unchecked; the current preferred branch delegates allocation to CaDiCaL. Signed overflow is not a valid wraparound strategy. Allocation exhaustion should produce a controlled resource-limit failure before arithmetic or backend mutation.

Open lead: literal-capacity checks (low priority). The capacity review records no observed overflow. The expected likelihood is low at ordinary workload sizes, but this is not protected by a guarantee that memory runs out first. Long-lived incremental sessions can keep allocating auxiliaries and scope selectors; deleting clauses does not by itself give Primo permission to reuse their IDs. Audit allocation, invalid externally supplied literals, and derived index/size arithmetic before declaring a supported limit. Boundary tests should use a testable capacity check or small artificial limit, rather than allocating billions of variables. The contributor should preserve 32-bit storage unless a separate backend/API design establishes a need for wider IDs.

From terms to clauses#

The input is a Boolean root in the borrowed term manager. In the solving pipeline, frontend translation and lowering have already given Boolean equality, xor, and extended operators their supported representation. The clausifier does not type-check arbitrary SMT-LIB or supply semantics for an unlowered operator merely because it has an atom case in a switch.

assert_formula checks the root sort, collects atom polarities, and asserts the root positively. Each call adds to the same clause database, so an assertion vector denotes a conjunction. The output is permanent clauses in the backend plus the retained abstraction maps; this operation does not itself search or decide theory consistency.

Asserted roots and reusable definitions#

assert_positive uses an explicit worklist with a visited set local to the call:

Asserted root	Clauses emitted
`true` / `false`	Nothing / an empty clause.
`And`	Assert its children; no variable is needed just for this root.
`Or`, with `top_level_or_tseitin=false`	One clause over the encoded children.
`Implies(a, b)`	One clause `¬lit(a) ∨ lit(b)`.
Other supported roots, or `Or` with `top_level_or_tseitin=true`	Encode the root and assert its literal as a unit clause.

Primo currently gives nested connectives a literal whose meaning survives use under either polarity. encode walks the DAG iteratively, caches literals, and emits full definitions. Writing xᵢ for a child literal and v for the new output literal, the implemented templates are:

Definition	Required clauses	Owning operation
`v ↔ And(x₁, …, xₙ)`	`¬v ∨ xᵢ` for each child; `v ∨ ¬x₁ ∨ … ∨ ¬xₙ`	encode_and
`v ↔ Or(x₁, …, xₙ)`	`¬xᵢ ∨ v` for each child; `¬v ∨ x₁ ∨ … ∨ xₙ`	encode_or
`v ↔ (a → b)`	`a ∨ v`; `¬b ∨ v`; `¬v ∨ ¬a ∨ b`	encode_implies

Not(t) uses -lit(t) without a new definition. When an encoded constant needs a literal, true_lit creates a shared unit-constrained variable; false uses its negation.

The option defaults select direct root-OR clauses, but a formula-shape policy can enable root-OR definitions for a selected goal. The worked example below fixes the constructor flag explicitly; preprocessing and strategy selection can change the clause counts in a full solve.

Each encoded And or Or with n children contributes n + 1 clauses and 3n + 1 literal occurrences. Definitions are cached across calls, and their size is linear in the encoded DAG’s nodes and direct child edges. Root walks may revisit shared structure across separate assertions; their visited set is not shared across calls. Dense arrays also consume space for term indices outside the encoded Boolean DAG. These bounds describe translation, not SAT search time or total solver memory.

Polarity-aware definitions: an open lead#

Full equivalence is sufficient, but is not always necessary. With a fresh auxiliary v for subformula F, Plaisted–Greenbaum conversion needs v → F for positive-only occurrences and F → v for negative-only occurrences. Both directions are required when one shared auxiliary serves both polarities. The root requirement is still asserted.

In the example below, q ∧ ¬r occurs only positively, so a directional encoder could omit v ∨ ¬q ∨ r, reducing four clauses to three. Primo currently emits all four. Its atom-polarity metadata does not perform this optimization.

The literature note includes direct SMT references and an implementation checklist. General PG encoding remains an open lead: incremental opposite-polarity uses require completing definitions, and a one-direction auxiliary cannot automatically stand for the exact value of a Boolean term in a model or function argument. The earlier rejected root-polarity prototype did not evaluate general PG conversion.

Atom registry and polarity#

theory_atom_for_term reuses an existing term/literal association or appends a registry entry. Boolean constants and predicates are registered as well as equality and arithmetic atoms. Quantified roots are opaque atoms for their separate solver route; their bodies are not traversed as ordinary ground Boolean structure.

collect_theory_atom_polarities tracks positive/negative occurrence through connectives: Not reverses the sign and an implication reverses it for the antecedent. These flags describe syntax, not the current SAT assignment. They accumulate in the retained clausifier and are not undone by scope pop. They support downstream policies; they do not turn the full definitions above into a polarity-only encoding.

ensure_generated_theory_atom_with_lit records a caller-supplied literal and rejects a conflicting existing mapping. The caller still owns the obligation to allocate/observe the variable and establish the generated atom’s semantics. Registration alone does not prove a theory lemma.

Boolean arguments to uninterpreted functions need additional care: Bool has two values, so a propositional assignment must agree with the EUF value of an argument. Boolean-argument registration marks the relevant Boolean constants for both-polarity theory relevance. This reuses their existing literal when present; an argument not previously encoded still needs its first SAT variable. Registration adds no equality atoms or linking clauses. The shared register_euf_boolean_arguments entry point completes this preparation for ground and quantified EUF recipes. The EUF chapter follows the registered literal into an explained equality with true or false.

Worked example: one nested conjunction#

Construct Boolean constants p, q, and r, then assert p ∨ (q ∧ ¬r) with direct root-OR clauses. Let v name q ∧ ¬r. The nested definition and asserted root give:

¬v ∨ q
¬v ∨ ¬r
 v ∨ ¬q ∨ r
 p ∨ v

There are four SAT variables and four submitted clauses. If p is false, the last clause forces v, hence q and ¬r. If p is true, the definition still makes v agree with q ∧ ¬r, without constraining q or r otherwise. Existentially eliminating v therefore recovers exactly the asserted formula.

The executable example constructs these terms directly, calls the real clausifier and CaDiCaL adapter, checks the clause counters before search, and checks all eight assignments to p, q, and r. It also checks the guarded version described next. Using the internal API here isolates clausification from parser and preprocessing effects. The review guide gives the build/run commands.

Permanent clauses, assumptions, and scope guards#

add_clause and assume have different lifetimes. A submitted clause persists; an assumption applies to the next solve. Repeated queries must resubmit their active assumptions. An empty clause makes the permanent database inconsistent, while contradictory assumptions can make only the current query UNSAT.

assert_guarded_formula emits full, unconditional definitions for the formula and only guards its root:

definitions of F
¬s ∨ lit(F)

Assuming selector s activates F. Setting s false disables the root requirement, while the definitions remain satisfiable extensions of any assignment to the original atoms. Full definitions also make the auxiliary literal safe to reuse under either polarity; a one-way implication alone would not guarantee that equivalence.

The opt-in assumptions engines implement scopes on top of this SAT interface. For example, IncrementalUfEngine creates a selector when a scope first gains an assertion and permanently adds ¬s when that scope is popped. Its query loop resubmits active selectors on every solve, including theory-refinement retries. No clause or term deletion follows from this scheme. Default rebuild sessions have a different owner lifetime, as explained in the architecture chapter.

The backend and callback contract#

The Yices literature note explains how a requested theory explanation can also become a reusable SAT clause. Reason storage in a propagator, deferred construction, and retention by the backend are separate mechanisms; their remaining policy questions are recorded as open leads.

CadicalBackend::new_var uses the available dependency API to declare ordinary variables between solves. new_observed_var is the separate path for fresh variables during callbacks. It accounts for variables already created inside CaDiCaL and observes the new variable. The capability flags describe what this backend supports; a caller must not assume another adapter supports it.

The ExternalPropagator interface provides the following exchanges. The connected SMT propagator owns the term mapping and theory state behind them.

Exchange	Contract at the boundary
`notify_assignment`, `notify_new_decision_level`, `notify_backtrack`	Maintain theory state for the notified SAT trail and undo changes above the reported backtrack level.
`cb_propagate`	Return an observed literal, or zero when there is no propagation; retain a valid explanation.
`cb_add_reason_clause_lit`	Stream the requested propagation’s reason clause, ending with zero.
`cb_has_external_clause`, `cb_add_external_clause_lit`	Announce and stream a theory conflict/lemma clause, ending with zero.
`cb_check_found_model`	Check the candidate Boolean assignment against the external constraints; a rejection needs a valid continuation such as a new lemma.
`cb_decide`	Optionally suggest a decision literal; zero leaves the choice to SAT.

Zero is a callback sentinel or clause-stream terminator, not an ordinary sat::Lit to put in a Clause. A reason such as ¬a ∨ b must actually justify propagating b from a; the SAT adapter cannot establish that theory fact. Theories must preserve explanations for the backend’s reason requests.

Only one external propagator connects to a backend at a time. A theory dispatcher handles multiple components behind that connection. Relevant variables must be observed after connection; callback propagation and external clauses must respect the observed-variable contract. The adapter exposes no operation for removing individual observed variables.

The callback adapter forwards to borrowed Primo objects. Disconnect before destroying those objects, including on cancellation or exceptions. Between queries, reconnect_external_propagator disconnects, connects the new callback, and re-observes variables. The old callback must remain alive through disconnection; the new one must handle replayed root assignments. Connection is not ownership transfer. The terminator guard supplies scoped disconnection for cancellation callbacks.

Results and limits#

solve, value, and failed separate SAT, UNSAT, unknown/interrupted, and a build without the backend. value(v) is queried after SAT using a positive variable ID; the caller applies the sign of its literal. failed(lit) concerns an assumption after UNSAT. Query these in the appropriate backend state, before changing the formula or assumptions; the wrapper’s last-result field is not a full state-machine guard.

The Boolean-only solve path shows the complete composition, including cancellation, counters, and typed model reconstruction. A Boolean assignment is not an SMT interpretation; the theory engines have further obligations before returning a solver answer. Builds without CaDiCaL return Unsupported from the adapter, not a fallback SAT search. Proof-producing integration is not implemented by this interface.

The backend reference covers CaDiCaL overrides, factoring, separate version builds, and SAT search counters. Statistics distinguishes backend work from theory work.

Sources and implementation status#

G. S. Tseitin, “On the Complexity of Derivation in Propositional Calculus” (1968; English reprint in Automation of Reasoning, 1983, pp. 466–483), §1, p. 467. Primary text. The relevant construction assigns variables to subformulas and constrains their meanings. Primo implements ordinary definitional clauses for its Boolean DAG, with n-ary connective templates and direct positive-root rules. The paper’s validity reduction negates its root; Primo asserts the desired formula positively for satisfiability.
Plaisted–Greenbaum conversion and SMT: the dedicated note records Masina, Spallitta, and Sebastiani (JAIR 2025), §§2.1 and 3.2, and SMTInterpol’s primary documentation. General directional encoding is an open lead; Primo emits the full definitions described above.
K. Fazekas, A. Niemetz, M. Preiner, M. Kirchweger, S. Szeider, and A. Biere, “IPASIR-UP: User Propagators for CDCL,” SAT 2023, §§2.1–2.4. Primary text and publication record. Primo implements the callback boundary through its own interfaces and a CaDiCaL C++ adapter. Its assignment notification is vector-shaped; the compatibility branch wraps a scalar notification and discards its fixed flag. Primo omits the paper’s remove_observed_var, is_decision, and unphase operations and proof-producing applications.

Obligation	Implemented owner and verification
Definitions preserve Boolean meaning and sharing with linear clause output	`BooleanClausifier` caches, worklists, and templates above; the worked truth table and reconvergent DAG regression.
Popped roots cease constraining the problem while definitions remain valid	Guarded-root construction and selectors; UF scope tests and LRA scope tests.
Bool-valued arguments have only their two semantic values	Boolean-argument registration contract; Boolean-domain regressions.
Trail changes, reason lifetime, cancellation, and fresh observation respect the backend protocol	backend regressions and component explanation tests. Callback costs depend on the chosen theory; the interface promises no constant-time theory operation.

Original Primo notes explain the guarded-scope design and Boolean sharing contract. The root-polarity prototype was rejected; its signed root worklist is not current behavior. The review ledger records the chapter’s checks.