bibkey: kullmann2011clausal authors: “Oliver Kullmann” year: 2011 title: “Constraint satisfaction problems in clausal form” doi: 10.48550/arXiv.1103.3693 url: https://arxiv.org/abs/1103.3693v1 claim: “Lemma 1.7.1 characterizes matching satisfiability by a bipartite matching covering every clause occurrence, with domain-size-minus-one copies of each variable.” strata_touched: [] license: citation-only triage: anchor

Matching capacity for finite non-Boolean clauses

The inspected primary text is arXiv:1103.3693v1, deposited 18 March 2011. Section 1.7.1, printed pages 30–31, constructs a bipartite graph with clause-occurrence vertices and (|D_v|-1) copies of every variable (v). Lemma 1.7.1 states that a multi-clause-set is matching satisfiable exactly when a matching covers all its clause vertices. Matching satisfiability is a sufficient special form of satisfiability; the lemma does not equate arbitrary satisfiability with this matching condition.

With one variable per prime-adic digit, avoiding an arithmetic cylinder is a clause of digit disequalities. The counting certificate in the covering report imposes the stronger requirement that an assigned prime’s first digit differs, while reserving capacity for pair conflicts. This is sufficient to avoid the original cylinder; it is not an equivalent translation of every full-height avoidance condition. The reservation and pure-power tail bound are separate arithmetic deductions. A height-dependent weighted assignment of whole prefixes is not the ordinary matching problem of Lemma 1.7.1: a clause cannot be split fractionally between primes without an additional argument.

No source text is vendored. No Lean declaration is attributed to this paper by this note.