Research map / Learning theory and algorithms / Combinatorial and search optimization
Certifying Bounds Propagation for Integer Multiplication Constraints
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Extends pseudo-Boolean (VeriPB) proof logging to bounds-consistent propagation of integer multiplication and division constraints in constraint programming solvers, with a bespoke justification procedure.
Problem
Certifying (proof-logging) bounds-consistent propagation for ternary integer multiplication constraints in CP solvers, using a linear pseudo-Boolean proof system that only handles 0-1 variables.
Approach
Encodes CP integer variables as binary bit vectors with sign-bit/absolute-value channelling and derives bounds justifications for multiplication via cutting planes, RUP, and proof by contradiction, with step counts proportional to the product of bit-widths, instead of brute-force tabulation.
Key results
- On the n-fractions problem (n=2), the GCS solver with the new multiplication propagator produced a 428MB proof in 8.8s and VeriPB verified it in 4864.5s.
- Bounds-consistent proof logging was much faster than the auto-tabulation baseline on 1000 synthetic single-constraint instances, and the tabulation approach exceeded 2TB proof size on n-fractions.
- Derived justifications for bounds propagation take a number of proof steps proportional to the product of the bit-widths of the operand domains (O(n·m)).
Measured effects reported in the paper
| What was changed | Where | Measured | Effect |
|---|---|---|---|
| Use bounds-consistent justifications instead of auto-tabulation proofs | GCS multiplication constraint proof logging · Synthetic multiplication instances | solve time with proof logging | Helped |
| Use bounds-consistent justifications instead of auto-tabulation proofs | GCS multiplication constraint proof logging · Synthetic multiplication instances | VeriPB verification time | Helped |
| Use bounds-consistent justifications instead of auto-tabulation proofs | GCS multiplication constraint proof logging · n-fractions (n=2) | proof size: 428MB; >2TB | Helped |
Surprising findings
- Tabulation-based proofs exceeded 2TB on the n-fractions instance, whereas bespoke bounds justifications produced a 428MB proof.
Limitations
- Implementation details omitted; only indicative benchmarks on small/simple instances.
- Does not yet provide a comprehensive analysis on diverse benchmarks.
- Pure cutting-planes derivation for one upper-bound form is left as an open question.
Experimental setup
Datasets: synthetic ternary multiplication instances (1000, domains within [-200..200]) n-fractions problem from CSPLib (n=2)
Benchmarks: synthetic single-multiplication CSP instances n-fractions (CSPLib, n=2)
Metrics: solve time with proof logging VeriPB verification time proof file size
Baselines: auto-tabulation proof logging
Builds on: cutting planes proof system VeriPB pseudo-Boolean proof logging for CP (Gocht, McCreesh, Nordström 2022) Demirović et al. 2024 (RUP-based reification of derivations)
Closest papers by meaning
- Paths, Proofs, and Perfection: Developing a Human-Interpretable Proof System for Constrained Shortest Paths (AAAI 2024 · similarity 0.84)
- Finding Simple Proofs for First-Order Optimization (NeurIPS 2026 · similarity 0.83)
- The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.82)
- 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes (NeurIPS 2025 · similarity 0.82)
- Solving Inequality Proofs with Large Language Models (NeurIPS 2025 · similarity 0.82)
- MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curation (NeurIPS 2025 · similarity 0.82)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.