Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Incremental Selection of Most-Filtering Conjectures and Proofs of the Selected Conjectures

Jovial Cheukam Ngouonou, Ramiz Gindullin, Claude-Guy Quimper, Nicolas Beldiceanu, Remi Douence

TL;DR

This work presents an effective incremental algorithm for selecting the most-filtering conjectures and provides formal proofs for a comprehensive set of bounds related to Partition and BinSeq constraints. The method incrementally posts candidate bounds, avoids re-scanning all solutions, and uses a labeling-based backtracking metric to guide bound selection, enabling faster, non-redundant discovery of tight conjectures. It establishes a threefold contribution: (i) three selected Partition-bound conjectures (one on the sum of squares and two on range bounds) with tight combinatorial proofs; (ii) seventeen BinSeq conjectures addressing $N_1$, $G$, $GS$, and $DS$ relationships; and (iii) a cohesive incremental framework that can improve bound filtering and search efficiency in constraint solving. Together, these results enhance both the theoretical understanding of bound quality and the practical efficiency of constraint programming tools in handling Partition and BinSeq constraints.

Abstract

We present an improved incremental selection algorithm of the selection algorithm presented in [1] and prove all the selected conjectures.

Incremental Selection of Most-Filtering Conjectures and Proofs of the Selected Conjectures

TL;DR

This work presents an effective incremental algorithm for selecting the most-filtering conjectures and provides formal proofs for a comprehensive set of bounds related to Partition and BinSeq constraints. The method incrementally posts candidate bounds, avoids re-scanning all solutions, and uses a labeling-based backtracking metric to guide bound selection, enabling faster, non-redundant discovery of tight conjectures. It establishes a threefold contribution: (i) three selected Partition-bound conjectures (one on the sum of squares and two on range bounds) with tight combinatorial proofs; (ii) seventeen BinSeq conjectures addressing , , , and relationships; and (iii) a cohesive incremental framework that can improve bound filtering and search efficiency in constraint solving. Together, these results enhance both the theoretical understanding of bound quality and the practical efficiency of constraint programming tools in handling Partition and BinSeq constraints.

Abstract

We present an improved incremental selection algorithm of the selection algorithm presented in [1] and prove all the selected conjectures.

Paper Structure

This paper contains 24 sections, 6 theorems, 49 equations, 7 algorithms.

Table of Contents

  1. Introduction
  2. An Incremental Selection Algorithm
  3. Proofs for the Conjectures of the Partition Constraint
  4. Conjecture \ref{['eqn::upper_bound_sum_squares']}
  5. Conjecture \ref{['eqn::upper_bound_range1']}
  6. Conjecture \ref{['eqn::upper_bound_range2']}
  7. Proofs for the Conjectures of the BinSeq Constraint
  8. Conjecture \ref{['eqn::upper_bound_nv']}
  9. Conjecture \ref{['eqn::lower_bound_smax']}
  10. Conjecture \ref{['eqn::upper_bound_smax']}
  11. Conjecture \ref{['eqn::upper_bound_dmin']}
  12. Conjecture \ref{['eqn::upper_bound_dmax']}
  13. Conjecture \ref{['eqn::lower_bound_ssquare']}
  14. Conjecture \ref{['eqn::lower_bound_ssquare2']}
  15. Conjecture \ref{['eqn::lower_bound_ssquare3']}
  16. ...and 9 more sections

Key Result

lemma thmcounterlemma

If there exist at least two partitions whose sizes are strictly between $\underline{M}$ and $\overline{M}$, in other words, if their sizes are $\underline{M} + r_1$ and $\underline{M} + r_2$ such that $1\leq r_1\leq r_2 < \underline{\overline{M}}$, then $S$ is not maximal.

Theorems & Definitions (35)

  • definition thmcounterdefinition
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • proof
  • lemma thmcounterlemma
  • ...and 25 more