logicaffeine_proof/
complexity.rs

1//! Certified **complexity bounds** — a refutation that carries a checkable proof of its own size.
2//!
3//! A correctness certificate (the [`crate::pr`] refutation) answers "is this UNSAT?". A *complexity*
4//! certificate answers "and how big is the proof, provably?". The carrier is a **rank function**: a
5//! per-step natural-number measure that descends. If the measure is non-increasing and each of its
6//! levels contributes at most `w` steps, then a proof spanning `L` levels has at most `L · w` steps —
7//! a bound a checker confirms by reading the annotation, *without* trusting how the proof was built.
8//!
9//! This is a termination-proof-with-a-clock: the same descent that shows the construction halts also
10//! counts its steps. For the steered pigeonhole/coloring refutations the measure is "active items
11//! remaining," `L = O(n)` levels of `w = O(n)` steps each, so the certificate reads off a clean
12//! `O(n²)` bound — turning "we measured it polynomial" into "here is the proof it is."
13
14use crate::cdcl::Lit;
15use crate::proof::ProofStep;
16
17/// A refutation whose every step carries a rank (a progress/termination measure).
18#[derive(Clone, Debug)]
19pub struct RankedRefutation {
20    /// Whether the underlying refutation independently checked.
21    pub refuted: bool,
22    /// The proof steps, in order.
23    pub steps: Vec<ProofStep>,
24    /// `ranks[i]` is the measure value at step `i`. Must be non-increasing for a valid certificate.
25    pub ranks: Vec<u64>,
26}
27
28/// A certified upper bound on a refutation's size, read off a valid rank descent.
29#[derive(Clone, Copy, Debug, PartialEq, Eq)]
30pub struct SizeBound {
31    /// The number of distinct rank levels the measure passes through.
32    pub levels: u64,
33    /// The largest number of steps at any single rank level (the per-level "width").
34    pub max_width: u64,
35    /// The certified upper bound on the step count: `levels · max_width`.
36    pub bound: u64,
37    /// The actual step count (always `≤ bound`).
38    pub actual: u64,
39}
40
41/// Verify that `ranks` is a valid non-increasing measure and read off the [`SizeBound`] it
42/// certifies. Returns `None` if the measure ever *increases* (then it is not a termination measure
43/// and certifies nothing). The bound `levels · max_width` is a structural consequence of the
44/// annotation, so the checker never re-derives the proof — it only counts.
45pub fn certify_size_bound(ranks: &[u64]) -> Option<SizeBound> {
46    if ranks.is_empty() {
47        return Some(SizeBound {
48            levels: 0,
49            max_width: 0,
50            bound: 0,
51            actual: 0,
52        });
53    }
54    // The measure must never increase along the proof.
55    if ranks.windows(2).any(|w| w[1] > w[0]) {
56        return None;
57    }
58    // Count steps per rank level (the ranks are non-increasing, so equal ranks form contiguous runs;
59    // we still tally by value to be order-agnostic and robust).
60    let mut counts: std::collections::BTreeMap<u64, u64> = std::collections::BTreeMap::new();
61    for &r in ranks {
62        *counts.entry(r).or_insert(0) += 1;
63    }
64    let levels = counts.len() as u64;
65    let max_width = counts.values().copied().max().unwrap_or(0);
66    Some(SizeBound {
67        levels,
68        max_width,
69        bound: levels * max_width,
70        actual: ranks.len() as u64,
71    })
72}
73
74impl RankedRefutation {
75    /// Independently check BOTH facets against the original `formula`: the refutation is correct
76    /// (the PR checker accepts it) AND its size is bounded by its rank certificate. Returns the
77    /// certified [`SizeBound`] only if both hold.
78    pub fn certify(&self, num_vars: usize, formula: &[Vec<Lit>]) -> Option<SizeBound> {
79        if self.ranks.len() != self.steps.len() {
80            return None;
81        }
82        if !crate::pr::check_pr_refutation_fast(num_vars, formula, &self.steps) {
83            return None;
84        }
85        let bound = certify_size_bound(&self.ranks)?;
86        // The bound is an upper bound on the actual size by construction; assert the invariant.
87        (bound.actual <= bound.bound).then_some(bound)
88    }
89}
90
91#[cfg(test)]
92#[path = "../../logicaffeine_tests/unit/logicaffeine_proof/complexity/tests.rs"]
93mod tests;
logicaffeine_proof/complexity.rs

logicaffeine_proof/
complexity.rs
