logicaffeine_proof/

cnf.rs

//! Tseitin clausification: a grounded, quantifier-free `ProofExpr` → CNF over the CDCL
//! core's `Lit`s (Tseitin, 1968 — the standard linear-size equisatisfiable transform that
//! introduces one auxiliary variable per compound subformula). This is the bridge from the
//! logic-grid encoding (closures, at-most-one, of-pair, clue clauses) to the [`crate::cdcl`]
//! SAT engine, giving the **Untrusted** trust tier: solve `premises ∧ ¬goal`; UNSAT ⇒ the
//! goal is entailed. The same CNF feeds the RUP checker (the fast trust tier) and is the
//! input an AllDifferent GAC propagator filters.

use crate::cdcl::{Lit, SolveResult, Solver, Var};
use crate::{ProofExpr, ProofTerm};
use std::collections::{HashMap, HashSet};

// Tseitin operator tags for the structural-hashing cache key.
const OP_AND: u8 = 0;
const OP_OR: u8 = 1;
const OP_IMPL: u8 = 2;
const OP_IFF: u8 = 3;

/// Canonical ordering of two literals (by variable, then sign) — for commutative-operator
/// keys so `a∧b` and `b∧a` share one auxiliary variable.
#[inline]
fn order2(a: Lit, b: Lit) -> (Lit, Lit) {
    if (a.var(), a.is_positive()) <= (b.var(), b.is_positive()) {
        (a, b)
    } else {
        (b, a)
    }
}

/// A CNF formula under construction: a variable table (atoms canonicalised so `a = b` and
/// `b = a` share a variable) plus the accumulating clause set. `Clone` so a prepared
/// premise CNF can be reused per goal — the of-pair Tseitin work is done once, then each
/// cell only adds its `¬goal` unit (incremental solving, the IPASIR pattern).
#[derive(Clone, Default)]
pub struct Cnf {
    atom_of: HashMap<String, Var>,
    num_vars: usize,
    clauses: Vec<Vec<Lit>>,
    /// Structural-hashing cache: `(op, lit, lit) → aux literal`, so a subformula encoded
    /// twice reuses ONE auxiliary variable (and its defining clauses) instead of minting a
    /// fresh one. This is hash-consing of the Tseitin encoding.
    expr_cache: HashMap<(u8, Lit, Lit), Lit>,
    /// Canonicalised (sorted) clauses already added, so a clause produced twice by grounding
    /// is stored once.
    clause_seen: HashSet<Vec<Lit>>,
}

impl Cnf {
    pub fn new() -> Self {
        Self::default()
    }

    /// Clausify a fixed premise set ONCE (the expensive of-pair Tseitin work), so many
    /// goals can be checked against it by cloning + adding `¬goal`. `None` if any premise is
    /// not encodable. This is the incremental entry for solving a whole puzzle (16+ cells)
    /// without re-grounding or re-clausifying the shared premises every time.
    pub fn from_premises(premises: &[ProofExpr]) -> Option<Cnf> {
        let mut cnf = Cnf::new();
        for p in premises {
            cnf.assert(p)?;
        }
        Some(cnf)
    }

    /// Number of CDCL variables allocated (atoms + Tseitin auxiliaries).
    pub fn num_vars(&self) -> usize {
        self.num_vars
    }

    /// Number of distinct ATOM variables (the rest are Tseitin auxiliaries).
    pub fn num_atoms(&self) -> usize {
        self.atom_of.len()
    }

    /// The accumulated clauses.
    pub fn clauses(&self) -> &[Vec<Lit>] {
        &self.clauses
    }

    /// The Boolean value of atom `e` under a SAT `model` (a [`crate::cdcl::SolveResult::Sat`]
    /// assignment, indexed by variable), or `None` if `e` is not a recognised atom or was
    /// never encoded into this CNF. This decodes a model back to source atoms (e.g.
    /// `signal@t`), skipping the Tseitin auxiliaries that carry no source meaning.
    pub fn atom_value(&self, e: &ProofExpr, model: &[bool]) -> Option<bool> {
        let key = atom_key(e)?;
        let v = *self.atom_of.get(&key)?;
        model.get(v as usize).copied()
    }

    fn fresh(&mut self) -> Var {
        let v = self.num_vars as Var;
        self.num_vars += 1;
        v
    }

    /// The variable for an atom, allocating one the first time it is seen.
    fn atom_var(&mut self, key: String) -> Var {
        if let Some(&v) = self.atom_of.get(&key) {
            return v;
        }
        let v = self.fresh();
        self.atom_of.insert(key, v);
        v
    }

    /// Add a clause, canonicalised (sorted + within-clause dedup), dropping tautologies and
    /// EXACT duplicates. Grid grounding emits the same clause many times (≈13% were dups);
    /// storing each once shrinks the solve and the RUP replay for free.
    fn push_clause(&mut self, mut lits: Vec<Lit>) {
        lits.sort_by_key(|l| (l.var(), l.is_positive()));
        lits.dedup();
        // Sorted ⇒ both polarities of a variable are adjacent: that is a tautology, drop it.
        if lits.windows(2).any(|w| w[0].var() == w[1].var()) {
            return;
        }
        if self.clause_seen.insert(lits.clone()) {
            self.clauses.push(lits);
        }
    }

    /// Add a clause verbatim (canonicalised exactly as the Tseitin encoder's own clauses are).
    /// The seam a caller that builds its clause literals itself — a bit-blaster asserting the
    /// negation of a gate DAG, say — pushes through, so it shares this table's canonicalisation
    /// and duplicate suppression instead of reimplementing them.
    pub fn add_clause(&mut self, lits: Vec<Lit>) {
        self.push_clause(lits);
    }

    /// The literal of a named Boolean atom, allocating its variable the first time it is seen.
    /// Same table [`encode`](Self::encode) uses for `ProofExpr::Atom`, so the two agree on
    /// variable numbering.
    pub fn atom_lit(&mut self, name: &str) -> Lit {
        Lit::pos(self.atom_var(name.to_string()))
    }

    /// Tseitin-define `x ↔ (a ∧ b)` and return `x`, reusing the cached auxiliary when this
    /// conjunction has been encoded before. The primitive behind `encode(And(..))`, exposed so a
    /// caller holding a gate DAG can encode it WITHOUT first materialising the `ProofExpr` tree
    /// (which is exponentially larger than the DAG for a reconvergent datapath).
    pub fn encode_and(&mut self, a: Lit, b: Lit) -> Lit {
        let (a, b) = order2(a, b);
        if let Some(&x) = self.expr_cache.get(&(OP_AND, a, b)) {
            return x;
        }
        let x = Lit::pos(self.fresh());
        self.push_clause(vec![x.negated(), a]);
        self.push_clause(vec![x.negated(), b]);
        self.push_clause(vec![x, a.negated(), b.negated()]);
        self.expr_cache.insert((OP_AND, a, b), x);
        x
    }

    /// Tseitin-define `x ↔ (a ∨ b)` and return `x`. See [`encode_and`](Self::encode_and).
    pub fn encode_or(&mut self, a: Lit, b: Lit) -> Lit {
        let (a, b) = order2(a, b);
        if let Some(&x) = self.expr_cache.get(&(OP_OR, a, b)) {
            return x;
        }
        let x = Lit::pos(self.fresh());
        self.push_clause(vec![x.negated(), a, b]);
        self.push_clause(vec![x, a.negated()]);
        self.push_clause(vec![x, b.negated()]);
        self.expr_cache.insert((OP_OR, a, b), x);
        x
    }

    /// Tseitin-define `x ↔ (¬a ∨ b)` and return `x`. See [`encode_and`](Self::encode_and).
    pub fn encode_implies(&mut self, a: Lit, b: Lit) -> Lit {
        if let Some(&x) = self.expr_cache.get(&(OP_IMPL, a, b)) {
            return x;
        }
        let x = Lit::pos(self.fresh());
        self.push_clause(vec![x.negated(), a.negated(), b]);
        self.push_clause(vec![x, a]);
        self.push_clause(vec![x, b.negated()]);
        self.expr_cache.insert((OP_IMPL, a, b), x);
        x
    }

    /// Tseitin-define `x ↔ (a ↔ b)` and return `x`. See [`encode_and`](Self::encode_and).
    pub fn encode_iff(&mut self, a: Lit, b: Lit) -> Lit {
        let (a, b) = order2(a, b);
        if let Some(&x) = self.expr_cache.get(&(OP_IFF, a, b)) {
            return x;
        }
        let x = Lit::pos(self.fresh());
        self.push_clause(vec![x.negated(), a.negated(), b]);
        self.push_clause(vec![x.negated(), a, b.negated()]);
        self.push_clause(vec![x, a, b]);
        self.push_clause(vec![x, a.negated(), b.negated()]);
        self.expr_cache.insert((OP_IFF, a, b), x);
        x
    }

    /// Tseitin-encode `e`, returning a literal whose truth equals `e`'s, and emitting the
    /// defining clauses for any auxiliary variables. Returns `None` if `e` is not a
    /// quantifier-free propositional formula over recognisable atoms (so the caller can
    /// fall back to another engine rather than silently mis-encode).
    pub fn encode(&mut self, e: &ProofExpr) -> Option<Lit> {
        match e {
            ProofExpr::Not(p) => Some(self.encode(p)?.negated()),
            ProofExpr::And(p, q) => {
                let (a, b) = (self.encode(p)?, self.encode(q)?);
                Some(self.encode_and(a, b))
            }
            ProofExpr::Or(p, q) => {
                let (a, b) = (self.encode(p)?, self.encode(q)?);
                Some(self.encode_or(a, b))
            }
            ProofExpr::Implies(p, q) => {
                // p → q  ≡  ¬p ∨ q (NOT commutative, so no `order2`).
                let a = self.encode(p)?;
                let b = self.encode(q)?;
                Some(self.encode_implies(a, b))
            }
            ProofExpr::Iff(p, q) => {
                let (a, b) = (self.encode(p)?, self.encode(q)?);
                Some(self.encode_iff(a, b))
            }
            _ => {
                // An atom (Predicate / Identity / Atom): a single Boolean variable.
                let key = atom_key(e)?;
                Some(Lit::pos(self.atom_var(key)))
            }
        }
    }

    /// Assert `e` as CNF, introducing auxiliary variables ONLY for genuinely non-clausal
    /// structure (a disjunct that is itself a conjunction — e.g. an of-pair disjunct). A
    /// top-level conjunction splits into separate clauses; a disjunction or implication
    /// flattens into ONE clause; a literal stays a literal. So a closure `A∨B∨C∨D` becomes a
    /// single clause with ZERO aux variables instead of a Tseitin spine. This structure-aware
    /// clausification (Plaisted & Greenbaum, 1986) is what keeps the CNF — and therefore the
    /// solve and the RUP replay — small. `None` if `e` is not encodable.
    pub fn assert(&mut self, e: &ProofExpr) -> Option<()> {
        match e {
            ProofExpr::And(a, b) => {
                self.assert(a)?;
                self.assert(b)
            }
            ProofExpr::Implies(a, b) => {
                // ¬a ∨ b, flattened into one clause.
                let mut lits = self.clause_lits(&negate_expr(a))?;
                lits.extend(self.clause_lits(b)?);
                self.push_clause(lits);
                Some(())
            }
            _ => {
                let lits = self.clause_lits(e)?;
                self.push_clause(lits);
                Some(())
            }
        }
    }

    /// Assert the NEGATION of `e` (used to refute the goal). A literal goal becomes a unit
    /// clause; a compound goal asserts its De-Morgan dual, clause by clause.
    pub fn assert_neg(&mut self, e: &ProofExpr) -> Option<()> {
        self.assert(&negate_expr(e))
    }

    /// The literals of `e` viewed as ONE clause: flatten `∨` and `→`, literalise atoms and
    /// negated atoms, and Tseitin any other (non-literal) disjunct into a single auxiliary
    /// literal.
    fn clause_lits(&mut self, e: &ProofExpr) -> Option<Vec<Lit>> {
        if let Some(l) = self.lit_of_atom(e) {
            return Some(vec![l]);
        }
        match e {
            ProofExpr::Or(a, b) => {
                let mut v = self.clause_lits(a)?;
                v.extend(self.clause_lits(b)?);
                Some(v)
            }
            ProofExpr::Implies(a, b) => {
                let mut v = self.clause_lits(&negate_expr(a))?;
                v.extend(self.clause_lits(b)?);
                Some(v)
            }
            // De Morgan keeps a negated subformula a single clause with NO auxiliary:
            // ¬(a ∧ b) ≡ ¬a ∨ ¬b, and ¬¬x ≡ x. (¬(a ∨ b) is a conjunction, not a clause, so it
            // still falls through to one auxiliary below.) Every at-most-one pair is `¬(a ∧ b)`,
            // so this collapses hundreds of Tseitin spines into plain binary clauses.
            ProofExpr::Not(inner) => match inner.as_ref() {
                ProofExpr::And(a, b) => {
                    let mut v = self.clause_lits(&negate_expr(a))?;
                    v.extend(self.clause_lits(&negate_expr(b))?);
                    Some(v)
                }
                ProofExpr::Not(x) => self.clause_lits(x),
                _ => Some(vec![self.encode(e)?]),
            },
            // A non-clausal subformula (typically a conjunction): one auxiliary variable.
            _ => Some(vec![self.encode(e)?]),
        }
    }

    /// A literal for `e` if it is an atom or a negated atom, else `None`.
    fn lit_of_atom(&mut self, e: &ProofExpr) -> Option<Lit> {
        match e {
            ProofExpr::Not(p) => {
                let key = atom_key(p)?;
                Some(Lit::pos(self.atom_var(key)).negated())
            }
            ProofExpr::Predicate { .. } | ProofExpr::Identity(..) | ProofExpr::Atom(_) => {
                let key = atom_key(e)?;
                Some(Lit::pos(self.atom_var(key)))
            }
            _ => None,
        }
    }

    /// Hand the accumulated CNF to a fresh CDCL solver.
    pub fn into_solver(self) -> Solver {
        self.into_solver_with_atoms().0
    }

    /// Like [`into_solver`](Self::into_solver) but also hands back the atom→variable map (moved,
    /// not cloned). Callers that need to decode a SAT model can do so from this small map instead
    /// of cloning the entire clause database just to keep the table alive.
    pub fn into_solver_with_atoms(self) -> (Solver, HashMap<String, Var>) {
        let mut s = Solver::new(self.num_vars);
        for c in self.clauses {
            s.add_clause(c);
        }
        (s, self.atom_of)
    }
}

/// Does `premises ⊨ goal` (propositionally)? Encodes `premises ∧ ¬goal` to CNF and runs
/// CDCL: UNSAT ⇒ entailed. `None` if the problem is not purely propositional over
/// recognisable atoms (caller falls back). This is the **Untrusted** tier — the verdict
/// with no emitted proof, for the raw-speed comparison against Z3.
pub fn cdcl_entails(premises: &[ProofExpr], goal: &ProofExpr) -> Option<bool> {
    let mut cnf = Cnf::new();
    for p in premises {
        cnf.assert(p)?;
    }
    cnf.assert_neg(goal)?;
    let mut solver = cnf.into_solver();
    Some(solver.solve() == SolveResult::Unsat)
}

/// `¬e`, pushing the negation no further than one `Not` (clausification handles the rest).
fn negate_expr(e: &ProofExpr) -> ProofExpr {
    match e {
        ProofExpr::Not(p) => (**p).clone(),
        _ => ProofExpr::Not(Box::new(e.clone())),
    }
}

/// Canonical string key for an atom, so the same proposition always maps to one variable.
/// Identity is symmetric (`a = b` ≡ `b = a`), so its operands are ordered.
fn atom_key(e: &ProofExpr) -> Option<String> {
    match e {
        ProofExpr::Predicate { name, args, .. } => {
            let mut s = String::new();
            s.push_str(name);
            s.push('(');
            for (i, a) in args.iter().enumerate() {
                if i > 0 {
                    s.push(',');
                }
                s.push_str(&term_key(a));
            }
            s.push(')');
            Some(s)
        }
        ProofExpr::Identity(a, b) => {
            let (ka, kb) = (term_key(a), term_key(b));
            let (lo, hi) = if ka <= kb { (ka, kb) } else { (kb, ka) };
            Some(format!("={}={}", lo, hi))
        }
        ProofExpr::Atom(name) => Some(format!("atom:{name}")),
        _ => None,
    }
}

fn term_key(t: &ProofTerm) -> String {
    match t {
        ProofTerm::Constant(s) => s.clone(),
        ProofTerm::Variable(s) | ProofTerm::BoundVarRef(s) => format!("?{s}"),
        ProofTerm::Function(n, args) => {
            let inner: Vec<String> = args.iter().map(term_key).collect();
            format!("{n}({})", inner.join(","))
        }
        ProofTerm::Group(_) => "<group>".to_string(),
    }
}

#[cfg(test)]
#[path = "../../logicaffeine_tests/unit/logicaffeine_proof/cnf/tests.rs"]
mod tests;

#[cfg(test)]
#[path = "../../logicaffeine_tests/unit/logicaffeine_proof/cnf/cnf_more_tests.rs"]
mod cnf_more_tests;

#[cfg(test)]
#[path = "../../logicaffeine_tests/unit/logicaffeine_proof/cnf/cnf_differential_tests.rs"]
mod cnf_differential_tests;