1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
//! Fast refuter for the **modular counting principle** `Count_q(n)`: partition an `n`-element set into
//! blocks of size `q`. Encoded as: one Boolean per `q`-subset (block); a coverage clause per element
//! (the incident blocks, at least one chosen); and a disjointness clause for every pair of overlapping
//! blocks. It is unsatisfiable exactly when `q ∤ n`.
//!
//! The refutation is a one-line counting argument: coverage + disjointness force each element into
//! EXACTLY one chosen block, and every block covers exactly `q` elements, so summing over the elements
//! gives `n = q · (#chosen blocks)` — impossible when `q ∤ n`. Recognizing the structure and checking
//! `n mod q ≠ 0` is `O(clauses)`; the certificate is the triple `(n, q, n mod q)`.
//!
//! **Soundness:** the detector fires only when the clauses faithfully form `Count_q(n)` — every coverage
//! clause's incident blocks are pairwise disjoint (a full at-most-one clique, so each element is covered
//! at most once), every block covers exactly `q` elements, and `q ∤ n`. Then the counting argument makes
//! the formula unsatisfiable. Any deviation returns `None`; never a false refutation.
use crate::cdcl::Lit;
use std::collections::{HashMap, HashSet};
/// A modular-counting refutation: an `n`-element set cannot split into blocks of size `q` because
/// `q ∤ n` (the remainder is non-zero). Re-checkable in O(1): `n % q == remainder != 0`.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct CountingCert {
pub n: u64,
pub q: u64,
pub remainder: u64,
}
impl CountingCert {
/// Re-check from scratch: the certificate witnesses UNSAT iff `n mod q` is the stated non-zero
/// remainder.
pub fn check(&self) -> bool {
self.q >= 2 && self.remainder != 0 && self.n % self.q == self.remainder
}
pub fn byte_len(&self) -> usize {
24
}
}
/// Recover a `Count_q(n)` core from `clauses` and refute it by the `q ∤ n` counting argument, or `None`
/// if there is no such core. Conservative / fail-closed — see the module docs.
pub fn counting_certificate(num_vars: usize, clauses: &[Vec<Lit>]) -> Option<CountingCert> {
if num_vars < 2 {
return None;
}
let key2 = |x: u32, y: u32| if x < y { (x, y) } else { (y, x) };
// Coverage clauses = all-positive clauses (one per element, its incident blocks). Disjointness =
// binary all-negative clauses (overlapping blocks are mutually exclusive).
let mut coverage: Vec<Vec<u32>> = Vec::new();
let mut disjoint: HashSet<(u32, u32)> = HashSet::new();
for c in clauses {
if c.iter().all(|l| l.is_positive()) {
if c.is_empty() {
return None;
}
coverage.push(c.iter().map(|l| l.var()).collect());
} else if c.len() == 2 && !c[0].is_positive() && !c[1].is_positive() {
disjoint.insert(key2(c[0].var(), c[1].var()));
} else {
return None; // a clause that is neither coverage nor disjointness — not a clean Count_q
}
}
let n = coverage.len();
if n < 2 {
return None;
}
// Each element's incident blocks must be pairwise disjoint (a full at-most-one clique), so the
// element is covered at most once; with coverage that is exactly once.
let mut degree: HashMap<u32, usize> = HashMap::new();
for cov in &coverage {
let set: HashSet<u32> = cov.iter().copied().collect();
if set.len() != cov.len() {
return None; // a repeated block in one coverage clause
}
for i in 0..cov.len() {
*degree.entry(cov[i]).or_insert(0) += 1;
for j in (i + 1)..cov.len() {
if !disjoint.contains(&key2(cov[i], cov[j])) {
return None; // two blocks share this element but are not mutually exclusive
}
}
}
}
// Every block must cover the SAME number of elements q ≥ 2 (a uniform block size).
let q = *degree.values().next()?;
if q < 2 || degree.values().any(|&d| d != q) {
return None;
}
let (n, q) = (n as u64, q as u64);
let remainder = n % q;
if remainder == 0 {
return None; // q | n — a partition can exist, so this is not a refutation
}
Some(CountingCert { n, q, remainder })
}
/// Refute a `Count_q(n)` core (`q ∤ n`). `true` iff a certificate is recovered. Never a false refutation.
pub fn refute_counting(num_vars: usize, clauses: &[Vec<Lit>]) -> bool {
counting_certificate(num_vars, clauses).is_some_and(|c| c.check())
}