Variable Elimination for Prime-Implicate 0-1 Relaxations of Boolean Constraints
I study variable elimination for a canonical 0-1 relaxation of a finite Boolean constraint system. The relaxation is obtained from the prime implicates of the feasible predicate, or equivalently from the maximal subcubes of its excluded set. The main result concerns existential forgetting: after canonicalization, forgetting coordinates commutes with polyhedral projection. It follows that ideality is preserved. Universal forgetting behaves differently. A counterexample on four variables and an odd-cycle family show how integral hidden pieces can give a fractional visible relaxation. I also give a monotone single-coordinate condition under which universal forgetting preserves ideality. These statements concern the canonical prime-implicate relaxation. The exact finite censuses provide supporting examples and checks; the proof of the projection theorem does not depend on those computations. This preprint reproduces the manuscript body of the submitted paper. Computational verification records are available from me on request, as stated in the paper.
Authors
- Kuppusamy Ravindran (ORCID: https://orcid.org/0009-0006-3808-8863)
Institutions
- University of Limerick (IE)
Publication Details
- Journal
- Zenodo (CERN European Organization for Nuclear Research)
- Published
- 2026-09-17
- DOI
- https://doi.org/10.5281/zenodo.22809040
- Primary Topic
- Formal Methods in Verification
- Type
- preprint