logicaffeine_proof/
proof.rs

1//! Shared proof-step vocabulary for the certified checkers.
2//!
3//! A refutation is an ordered stream of clause *additions*, each carrying a justification a
4//! tiny independent checker can replay:
5//!
6//! - [`ProofStep::Rup`] — the clause follows by reverse unit propagation (the DRAT/RUP unit).
7//! - [`ProofStep::Pr`] — the clause is **propagation-redundant** with an explicit [`Witness`]
8//!   (Heule, Kiesl & Biere, *Short Proofs Without New Variables*, CADE 2017). This is the only
9//!   form that can certify a *model-removing* addition — exactly what a symmetry-breaking
10//!   predicate is — so it is the seam through which certified symmetry breaking flows.
11//!
12//! The witness may be an explicit partial [`Witness::Assignment`] or a literal
13//! [`Witness::Substitution`] (a permutation / automorphism). The substitution form is mere
14//! sugar: against a clause `C` whose falsifying assignment is `α = ¬C`, the substitution `σ`
15//! denotes the assignment witness `ω = { ¬σ(l) : l ∈ C }` — the image of the "bad" corner of
16//! the cube under the symmetry, which is the canonical PR witness for a lex-leader SBP. The
17//! checker ([`crate::pr`]) reduces every substitution to that assignment, so there is a single
18//! well-specified propagation-redundancy criterion to trust.
19
20use crate::cdcl::{Lit, Var};
21
22/// A literal permutation that respects negation: `σ(¬l) = ¬σ(l)`. Represented by the image of
23/// each variable's positive literal, so the negation invariant holds by construction.
24#[derive(Clone, Debug, PartialEq, Eq, Hash)]
25pub struct Perm {
26    /// `pos_image[v] = σ(+v)`. The negative literal's image is its negation.
27    pos_image: Vec<Lit>,
28}
29
30impl Perm {
31    /// The identity permutation over `num_vars` variables.
32    pub fn identity(num_vars: usize) -> Perm {
33        Perm { pos_image: (0..num_vars as Var).map(Lit::pos).collect() }
34    }
35
36    /// Build from the image of each positive literal: `images[v] = σ(+v)`.
37    pub fn from_images(images: Vec<Lit>) -> Perm {
38        Perm { pos_image: images }
39    }
40
41    /// Apply `σ` to a literal, respecting sign: `σ(¬l) = ¬σ(l)`.
42    pub fn apply(&self, l: Lit) -> Lit {
43        let img = self.pos_image[l.var() as usize];
44        if l.is_positive() {
45            img
46        } else {
47            img.negated()
48        }
49    }
50
51    /// Apply `σ` to every literal of a clause.
52    pub fn apply_clause(&self, clause: &[Lit]) -> Vec<Lit> {
53        clause.iter().map(|&l| self.apply(l)).collect()
54    }
55
56    /// The number of variables the permutation is defined over.
57    pub fn num_vars(&self) -> usize {
58        self.pos_image.len()
59    }
60
61    /// Whether this is the identity permutation.
62    pub fn is_identity(&self) -> bool {
63        self.pos_image.iter().enumerate().all(|(v, &img)| img == Lit::pos(v as Var))
64    }
65
66    /// Extend to `nv` variables, acting as the identity on the new (higher-indexed) variables.
67    /// Used to lift a base-formula symmetry over auxiliary variables it does not touch.
68    pub fn extended(&self, nv: usize) -> Perm {
69        let mut pos_image = self.pos_image.clone();
70        for v in pos_image.len()..nv {
71            pos_image.push(Lit::pos(v as Var));
72        }
73        Perm { pos_image }
74    }
75
76    /// Compose: `(self ∘ other)(l) = self(other(l))` — apply `other` first, then `self`.
77    pub fn compose(&self, other: &Perm) -> Perm {
78        Perm {
79            pos_image: (0..self.pos_image.len() as Var)
80                .map(|v| self.apply(other.apply(Lit::pos(v))))
81                .collect(),
82        }
83    }
84}
85
86/// A redundancy witness for a [`ProofStep::Pr`] clause.
87#[derive(Clone, Debug, PartialEq, Eq)]
88pub enum Witness {
89    /// An explicit partial assignment (the set of literals it sets true) — the classic PR
90    /// witness.
91    Assignment(Vec<Lit>),
92    /// A literal permutation / automorphism. Against the clause `C` it certifies, it denotes
93    /// the assignment `ω = { ¬σ(l) : l ∈ C }`.
94    Substitution(Perm),
95}
96
97/// One step of a refutation: add a clause with the justification a checker replays, or delete a
98/// clause from the working database (the DRAT deletion that inprocessing — vivification, BVE —
99/// relies on; deletions are unchecked, only additions carry a redundancy obligation).
100#[derive(Clone, Debug, PartialEq, Eq)]
101pub enum ProofStep {
102    /// Add a clause that is RUP w.r.t. the current database.
103    Rup(Vec<Lit>),
104    /// Add a clause that is propagation-redundant w.r.t. the current database, certified by
105    /// `witness`. May remove models; preserves satisfiability.
106    Pr { clause: Vec<Lit>, witness: Witness },
107    /// Remove a clause from the working database (a sound DRAT deletion).
108    Delete(Vec<Lit>),
109}
110
111impl ProofStep {
112    /// The clause this step adds or deletes.
113    pub fn clause(&self) -> &[Lit] {
114        match self {
115            ProofStep::Rup(c) | ProofStep::Delete(c) => c,
116            ProofStep::Pr { clause, .. } => clause,
117        }
118    }
119}
logicaffeine_proof/proof.rs

logicaffeine_proof/
proof.rs
