Module pseudo_boolean 

Pseudo-Boolean constraints + cutting planes — a proof system STRICTLY STRONGER than resolution.

Resolution (and therefore CDCL — ours and Z3’s) needs EXPONENTIALLY long refutations of the pigeonhole principle and of many counting/cardinality problems. Cutting planes refutes them in POLYNOMIAL size by reasoning about linear 0/1 inequalities directly: it p-simulates resolution and has short proofs where resolution provably cannot.

This is the certified core: a normalized PB constraint Σ aᵢ·ℓᵢ ≥ d (coeffs > 0, each variable once, ℓ a literal x or ¬x) and the four sound cutting-plane rules — addition (with literal cancellation via x + ¬x = 1), multiplication, division-with-rounding (the Gomory–Chvátal cut, sound only because variables are integral), and saturation — each of which is implied by its premises, so deriving the trivially-false 0 ≥ 1 refutes the inputs. Every rule is pinned against a brute-force oracle. The headline is php_refutation: the classic Cook–Coullard–Turán linear-size refutation of PHP — pure algebra where resolution explodes.

Structs

CardinalityTheory

A live cardinality theory for the CDCL engine (crate::cdcl::Theory) — the trail-driven twin of the static cutting-plane refuter refute_clausal. It propagates and conflicts on unit-coefficient cardinality constraints (Σ ℓ ≥ k, covering clauses, at-least-k, and at-most-k) directly on the solver’s trail (stateless: it rebuilds the partial assignment each call, so it can never desync), so it FUSES with a GF(2) parity theory (crate::xor_engine::XorEngine) under one crate::cdcl::Solver::solve_with: parity and counting reason together on the shared trail. That is exactly the structure that defeats either alone — e.g. minimal-disagreement parity, a parity core plus a residual cardinality core, where Gaussian elimination handles the parity and cardinality propagation handles the counting, but neither is a refutation by itself.

PbConstraint

A normalized pseudo-Boolean constraint Σ coeff·lit ≥ degree: every coeff > 0, every variable appears at most once, and the literal sign rides the entry — (coeff, positive) with positive == false meaning the literal ¬x. degree may be ≤ 0 (then the constraint is trivially true) or exceed the coefficient sum (then it is a contradiction).

Functions

coeff_symmetry_generators

The coefficient-symmetry generators of a pseudo-Boolean system: adjacent transpositions of variables that share a coefficient profile — the same (coeff, sign) (or absence) in every constraint. Such variables are interchangeable because each constraint is a weighted sum, blind to which equal-weight variable carries which value. Each generator is a genuine symmetry (is_pb_symmetry); together they generate the full product of symmetric groups on the profile classes. Variables in no constraint are excluded (free, not a constraint symmetry).

is_pb_symmetry

Does the variable permutation perm preserve every constraint? (term(perm[v]) == term(v) for all v — a relabelling that fixes each constraint’s coefficient/sign structure, hence its solution set.)

php_refutation

Refute the pigeonhole principle PHP(n, n−1) with the classic Cook–Coullard–Turán cutting- plane proof: sum all n “each pigeon in ≥1 hole” constraints with all n−1 “each hole holds ≤1 pigeon” constraints. Every x meets its ¬x and cancels, collapsing the whole system to the trivially-false 0 ≥ 1 in just 2n−1 additions — linear size, where resolution needs exponentially many steps. Returns the final derived constraint (a contradiction).

refute_clausal

Refute e by CUTTING PLANES when it is a cardinality/pigeonhole-shaped CNF. The pairwise encoding loses the cardinality structure, so we RECOVER it: the binary exclusions ¬(a∧b) form conflict cliques, each a genuine “at most one” group; summing those at_most(group,1) cardinality constraints with the positive “at least one” clauses cancels every literal against its negation and collapses a pigeonhole-shaped system to 0 ≥ 1 — POLYNOMIAL, where resolution/CDCL explode.