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 { levels: 0, max_width: 0, bound: 0, actual: 0 });
48    }
49    // The measure must never increase along the proof.
50    if ranks.windows(2).any(|w| w[1] > w[0]) {
51        return None;
52    }
53    // Count steps per rank level (the ranks are non-increasing, so equal ranks form contiguous runs;
54    // we still tally by value to be order-agnostic and robust).
55    let mut counts: std::collections::BTreeMap<u64, u64> = std::collections::BTreeMap::new();
56    for &r in ranks {
57        *counts.entry(r).or_insert(0) += 1;
58    }
59    let levels = counts.len() as u64;
60    let max_width = counts.values().copied().max().unwrap_or(0);
61    Some(SizeBound { levels, max_width, bound: levels * max_width, actual: ranks.len() as u64 })
62}
63
64impl RankedRefutation {
65    /// Independently check BOTH facets against the original `formula`: the refutation is correct
66    /// (the PR checker accepts it) AND its size is bounded by its rank certificate. Returns the
67    /// certified [`SizeBound`] only if both hold.
68    pub fn certify(&self, num_vars: usize, formula: &[Vec<Lit>]) -> Option<SizeBound> {
69        if self.ranks.len() != self.steps.len() {
70            return None;
71        }
72        if !crate::pr::check_pr_refutation_fast(num_vars, formula, &self.steps) {
73            return None;
74        }
75        let bound = certify_size_bound(&self.ranks)?;
76        // The bound is an upper bound on the actual size by construction; assert the invariant.
77        (bound.actual <= bound.bound).then_some(bound)
78    }
79}
80
81#[cfg(test)]
82mod tests {
83    use super::*;
84
85    #[test]
86    fn a_valid_descent_certifies_its_size() {
87        // ranks 3,3,2,2,2,1 → 3 levels, max width 3 (the two-and-three runs), bound 9, actual 6.
88        let ranks = vec![3, 3, 2, 2, 2, 1];
89        let b = certify_size_bound(&ranks).expect("non-increasing ⇒ valid");
90        assert_eq!(b.levels, 3);
91        assert_eq!(b.max_width, 3);
92        assert_eq!(b.bound, 9);
93        assert_eq!(b.actual, 6);
94        assert!(b.actual <= b.bound);
95    }
96
97    #[test]
98    fn an_increasing_measure_certifies_nothing() {
99        // A measure that goes back up is not a termination measure — reject it.
100        assert!(certify_size_bound(&[3, 2, 3]).is_none());
101        assert!(certify_size_bound(&[1, 2]).is_none());
102    }
103
104    #[test]
105    fn empty_and_flat_measures() {
106        assert_eq!(certify_size_bound(&[]).unwrap().bound, 0);
107        let flat = certify_size_bound(&[5, 5, 5]).unwrap();
108        assert_eq!((flat.levels, flat.max_width, flat.bound, flat.actual), (1, 3, 3, 3));
109    }
110}
logicaffeine_proof/complexity.rs

logicaffeine_proof/
complexity.rs
