Struct AutomorphismIndex 

pub struct AutomorphismIndex { /* private fields */ }

An incrementally-maintained clause database for fast repeated automorphism checks.

A certified symmetry-breaking refutation re-verifies an automorphism σ against the current database once per step, but the database only grows by one clause each step. Rebuilding the membership set from scratch every call (as the stateless perm_is_automorphism must) makes the whole refutation O(n⁴); maintaining the set — and a variable→clause occurrence map — incrementally drops each check to O(support of σ), and the refutation to O(n³).

The verdict is identical to perm_is_automorphism (a differential fuzz proves it); this is a pure acceleration structure, sound by construction: σ is an automorphism iff σ(C) ∈ F for every clause C it moves, and a clause disjoint from σ’s support maps to itself.

Implementations

impl AutomorphismIndex

pub fn new(nv: usize) -> Self

An empty index over nv variables.

pub fn with_clauses(nv: usize, clauses: &[Vec<Lit>]) -> Self

An index pre-loaded with clauses.

pub fn insert(&mut self, clause: Vec<Lit>)

Add one clause, updating the membership set, the occurrence lists, and the persistent unit-propagation base (which may cascade) — all amortized over the life of the index.

pub fn is_automorphism(&mut self, sigma: &Perm) -> bool

Is sigma an automorphism of the indexed database? Inspects only the clauses sigma actually moves — the union of the occurrence lists of its moved variables — using a stamped visited mark instead of a fresh O(|db|) allocation each call.

pub fn propagate_to_conflict( &mut self, _num_vars: usize, assume: &[Lit], ) -> bool

Occurrence-driven unit propagation layered over the persistent base: assume every literal of assume, propagate, and report whether a conflict results. Visits only clauses sharing a variable with a newly-assigned literal, and starts from the already-derived standing units — so a call costs O(touched), the difference between an O(n⁴) and an O(n³) refutation.

Robust to duplicate literals (x ∨ x is the unit x) and tautologies (x ∨ ¬x), matching the trusted [crate::rup::propagate] verdict exactly (a differential fuzz proves it).