Module sat 

Propositional SAT-discharge of a ProofExpr obligation — the engine behind in-browser, Z3-free hardware proving.

A bounded hardware property (an SVA assertion unrolled to discrete timesteps, or a Kripke-lowered FOL spec) reduces to a quantifier-free propositional formula over signal@t atoms. This module discharges two questions over that fragment, reusing the existing trust tiers (crate::cnf Tseitin → crate::cdcl CDCL → crate::rup RUP certification) so the answers are certified, not merely asserted:

• find_model — is the obligation satisfiable, and if so, a distinguishing assignment. This is ∃trace. φ, the core of bounded model checking and counterexample extraction.
• prove_equivalence — do two formulas denote the same Boolean function? F ≡ S iff F ↔ S is a tautology, certified via RUP; otherwise a concrete counterexample trace.

Everything here is pure Rust with no Z3 dependency, so it runs unchanged in the browser (wasm32) and in native tests where its verdicts are checked against Z3 as the oracle.

Enums

EquivOutcome

The result of an equivalence query between two formulas.

ModelOutcome

The result of a satisfiability query over a propositional obligation.

UnsatOutcome

The result of an unsatisfiability query — the shared primitive behind equivalence, bounded model checking, k-induction, and vacuity.

Functions

decode_model

Decode a SAT model back to (atom, value) bindings for every source atom appearing in exprs (Tseitin auxiliaries carry no source meaning and are skipped), sorted by name.

decode_model_from

Decode a SAT model from a pre-extracted atom→variable map (the table Cnf already holds), so a solve need not clone the whole clause database just to read its model back. Equivalent to decode_model for the propositional atoms collect_atoms gathers.

find_model

Is e satisfiable? Returns a witnessing model over its atoms if so.

prove_equivalence

Are a and b equivalent? F ≡ S iff F ↔ S is valid, i.e. ¬(F ↔ S) is UNSAT.

prove_unsat

core for equivalence, bounded model checking, k-induction, and vacuity.

prove_unsat_certified

Refute e with the certified recursive symmetry breaker and return the proof. Each round re-detects the residual automorphism group, certifies ONE lex-leader lead clause as a PR step (its generator a fresh automorphism of the current database), and re-detects — looping to a fixpoint that breaks the COMPLETE group, not just the adjacent positive-row swaps crate::symmetry::break_symmetries sees. The returned stream is the certified PR breaks followed by the closing RUP learned clauses, and it is already check_pr_refutation-verified against e’s CNF. None if e is not CNF-assertable, is satisfiable, or the breaker did not certify a refutation — the wired, checkable companion of prove_unsat’s coarse verdict.