Acquiring Maps of Interrelated Conjectures
on Sharp Bounds
Nicolas Beldiceanu
IMT Atlantique, LS2N (TASC), Nantes, France

Jovial Cheukam-Ngouonou
IMT Atlantique, LS2N (TASC), Nantes, France, and Université Laval, Québec, Canada

Rémi Douence
IMT Atlantique, LS2N, Inria, (Gallinette), Nantes, France

Ramiz Gindullin
IMT Atlantique, LS2N (TASC), Nantes, France

Claude-Guy Quimper
Université Laval, Québec, Canada

Abstract
To automate the discovery of conjectures on combinatorial objects, we introduce the concept of amap of sharp bounds on characteristics of combinatorial objects, that provides a set of interrelated
sharp bounds for these combinatorial objects. We then describe a Bound Seeker, a CP-based system,that gradually acquires maps of conjectures. The system was tested for searching conjectures onbounds on characteristics of digraphs: it constructs sixteen maps involving 431 conjectures on sharp
lower and upper-bounds on eight digraph characteristics.
2012 ACM Subject Classification Computing methodologies → Heuristic function construction;
Mathematics of computing → Combinatorial optimization
Keywords and phrases Acquisition of conjectures, digraphs, bounds
Digital Object Identifier 10.4230/LIPIcs.CP.2022.22
Funding Nicolas Beldiceanu: partially founded by the EU-funded ASSISTANT project no. 101000165.
Jovial Cheukam-Ngouonou: founded by the ANR AI@IMT project and by Laval University.
Ramiz Gindullin: founded by the EU-funded ASSISTANT project
Acknowledgements Thanks to Hervé Grall for his participation in the definition of the map concept,
and to Samir Loudni and Helmut Simonis for their comments on a preliminary version of this paper.

1

Introduction

Research on conjectures making systems in the context of discrete mathematics is a topic that
goes back to the late 1950s and the 1980s [8, 14, 32] and got renewed interest [20, 21, 29, 31].
Within CP, some initial research on the generation of implied constraints was done by Charley
et al. [11] and the most recent work focuses on model and constraint acquisition [4, 7, 10, 19,
27, 28] rather than on conjecture making. Within OR, Hansen’s AutoGraphiX system [1, 17]focuses on finding unrelated bounds using Variable Neighbourhood Search.
Four reasons motivate our work: (i) to highlight that CP can contribute to the automatic
discovery of conjectures, (ii) to systematically search sharp bounds on characteristics ofobjects that show up in combinatorial problems, (iii) to stress the need to develop conjecture
discovery programs that build up a body of strongly interrelated knowledge rather thanunrelated conjectures as it has been the case so far, (iv) by the fact that bounds are an essential
feature of branch-and-bound methods in optimisation but also a weakness of CP [16, 22]:the development of sharp bounds that consider several interrelated characteristics is still a© Nicolas Horia Beldiceanu, Jovial Cheukam-Ngouonou, Rémi Douence, Ramiz Gindullin and
Claude-Guy Quimper;
licensed under Creative Commons License CC-BY 4.0
28th International Conference on Principles and Practice of Constraint Programming (CP 2022).
Editor: Christine Solnon; Article No. 22; pp. 22:1–22:19
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

22:2

Acquiring Maps of Interrelated Conjectures on Sharp Bounds

manual process [3, 6]. Our approach is unique among all works for conjectures generation, as
the result is not a set, but rather a graph of conjectures, linked by projection (i.e. variable
elimination) operators. Our contributions are:We introduce the concept of map of sharp bounds as a set of interrelated conjectures
providing sharp lower and upper-bounds wrt the characteristic of a combinatorial object.
For each conjecture on a sharp bound, the map gives some extremal characteristics i.e.,the characteristic values common to all combinatorial objects achieving the bound.
By introducing secondary characteristics and by permitting the use of common sub-expressions in a polynomial, as well as simple Boolean and conditional formulae, we tend to
produce explainable conjectures. This also reveals unified conjectures across different
subsets of characteristics.
We demonstrate the usefulness of CP for acquiring such maps: using digraphs as combinatorial objects, the system produces 431 conjectures distributed in 16 maps obtained
from 8 characteristics combined with lower and upper bounds. It retrieves a set of known
results, enhances some known bounds, and comes up with new conjectures, some of which
we proved to be true.
The significance of maps is twofold. Beyond sharp bounds, a map brings together the relations
between several sharp bounds and the structure of combinatorial objects reaching each boundunder the same edifice. A map can be used to test the mutual consistency of independently
acquired bounds by verifying that one bound can be derived from another bound.
In Sect. 2, we introduce the concept of a map that presents a set of conjectures for sharpbounds and their logical relations. In Sect. 3.1, we provide the workflow of our acquisition
system. We introduce, in Sect. 3.2, a parameterised CP conjecture generator. We evaluate
the produced conjectures in Sect. 4, discuss related work in Sect. 5, and conclude in Sect. 6.

2

Conjectures map as a symbolic piece of knowledge

After providing an informal overview of maps of conjectures, and a first example of amap, we motivate, define and illustrate the map concept. Then we show how the use of
secondary characteristics permits both acquiring formulae sharing common sub-expressions,and sometimes come up with the same bound for different subsets of input characteristics.
Informal overview of maps Consider digraphs as an example of combinatorial objects. It
is well known that any digraph G satisfies the following invariant: the number of arcs a of G
is less than or equal to the square of the number of vertices v 2 of G, and the maximum value
v 2 is only reached when the number of vertices of the smallest connected component of G isequal to v, i.e. G consists of a single connected component of v vertices.
We are interested in systematically generating such candidate invariants, a.k.a. conjectures,for a richer set of characteristics, e.g. the number of connected components c of G, thenumber c of vertices of the smallest connected component of G.
Our conjectures have one of the following forms: (i) sharp bounds of a digraph characteristic wrt other digraph characteristics, e.g. a ≤ v 2 , or (ii) implication showing that, when asharp bound is reached, some characteristics are fixed or functionally determined by someother characteristics, e.g. a = v 2 ⇒ c = 1, and a = v 2 ⇒ c = v.
Finally, we are interested in connecting sharp bounds, revealing that the right-hand sideof an implication of type (ii) can be used to eliminate a characteristic of a sharp bound andretrieve a sharp bound with one less characteristic. For instance, replacing c by v in the

N. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

22:3

sharp bound a ≤ c2 + (v − c)2 , we retrieve the sharp bound a ≤ v 2 . We call these different
conjectures and the links connecting sharp bounds “map”.
A first example of map As an example of combinatorial objects, we use in this paper
digraphs with these characteristics: the number v of vertices, the number a of arcs, thenumber c (resp. s) of connected components (resp. strongly connected components), thenumber c (resp. c) of vertices of the smallest (resp. largest) connected component, the numbers (resp. s) of vertices of the smallest (resp. largest) strongly connected component. To
compare the bounds obtained by the Bound Seeker with the database of invariants of the
global constraint catalogue, see Sect.4.3 of [2], we assume that each vertex of a digraph has
at least one incoming or outgoing arc.
I Example 1. Fig. 1 illustrates the map concept with a map containing three conjectureslabelled as ¶, ·, and ®:Two conjectures about the sharp bounds ¶ a ≤ (v − (c − 1))2 + (c − 1), and · a ≤ v 2
on the maximum number of arcs a in a digraph G wrt the number of vertices v, and thenumber of connected components c of G.
The conjecture ® of node (B) indicates that the bound v 2 is reached only when c = 1.
The arrow going from node (A) to node (B) is labelled by ® as the bound v 2 is obtained byreplacing c by 1 in the bound (v − (c − 1))2 + (c − 1). The leftmost and rightmost parts ofFig. 1 show, in brown, two digraphs achieving these bounds.
Node (A)
v=3
c =2
a=5

{v, c}¶ a ≤ (v − (c − 1))2 + (c − 1)®

Node (B)· a ≤ v2
®c=1

{v}
v=3
c =1
a=9

Figure 1 Map of two sharp bounds on the maximum number of arcs of a digraphIn this paper, all maps of conjectures are presented in the same way as the map in Fig. 1:(i) the upper left corner of a node gives a node label in black, (ii) the upper right cornerprovides the parameters used in the sharp bound of this node in red, (iii) a dark label of theform ¶ refers to the sharp bound itself, (iv) a light label of the form ¬ designates an equation
which must hold to reach the sharp bound given in (iii), (v) a brown illustration shows awitness to the sharpness of the bound. Finally, an arrow from a first node to a second node
indicates which equation(s) in the second node should be used to substitute some parameters
used in the first node’s bound to retrieve the bound given in the second node. For spacereasons, some large maps, e.g. Fig 4, may omit the elements (i) and (v).
Motivating and defining the concept of map We introduce the concept of a map ofconjectures as a way to reveal the links between a set of conjectures related to sharp bounds
for a characteristic of a combinatorial object. Our goal is to describe conjectures on sharpbounds of characteristics of a combinatorial object, e.g. a digraph, a tree, and to organise
these conjectures into a single structure, a map of sharp bounds, which (i) systematicallyinterconnects these conjectures, and which (ii) describes the structure of the combinatorial
objects for which the bounds are reached. In the map in Fig. 1, we consider for digraphs threecharacteristics, a, v and c for the number of arcs, of vertices, and of connected components.

CP 202222:4

Acquiring Maps of Interrelated Conjectures on Sharp Bounds

I Definition 2. Given a finite set of input characteristics P and an output characteristico∈/ P, a map of sharp upper bounds MoP≤ is defined as a digraph where:
Each node of the map is associated with a subset P ⊆ P of input characteristics andcorresponds to a maximum conjecture of the form o ≤ f (P ). This inequality is tight, i.e.
there exist values that can be given to the parameters P in order to reach the equality.
In addition, a node contains maximality conjectures, at most one per characteristic q
in the complement of P wrt P, represented by the symbolic equality q = gq (P ), where
gq is a function defined over realisable parameters values of P and called a maximum
characterisation, and expressing the following property: for any combination of parameters
P reaching the maximum f (P ), the characteristic q is equal to gq (P ).
Each arc from conjecture o ≤ fi (Pi ) to conjecture o ≤ fj (Pj ) corresponds to a projection
from a subset Pi of input characteristics to a subset Pj of input characteristics, byeliminating a characteristic qi,j , i.e. Pj = Pi \ {qi,j }. The arc is labelled with an equality
qi,j = gqi,j (Pj ) where gqi,j (Pj ) is the value given to qi,j to reach the equality in the
conjecture o ≤ fj (Pj ). The equality qi,j = gqi,j (Pj ) is called a maximality conjecture.
In a map, there is a single output characteristic that we bound using the other characteristics called input characteristics. The output characteristic is the bounded characteristic, while
the input characteristics are the bounding characteristics. While the maximum conjecture
provides a bound on the output characteristic wrt the characteristics in P , the maximality
conjectures indicate the values taken by the characteristics not in P when the bound isreached. Similarly to MoP≤ , a map MoP≥ provides a collection of sharp lower bounds as aset of minimum conjectures of the form o ≥ fj (Pj ), and a set of minimality conjectures.
°

K K K

2
2
3
Node (A)v = 7, c = 3, c = 2, a = 17
¶ a ≤ (c − 1) · c2 + (v − (c − 1) · c)2{v, c}
Node (B)· a ≤ c2 + (v − c)2
2 K5° c = (v = c) ? 1 : 2 v = 7, K
c = 2, a = 29²{v, c, c}±{v, c}
Node (C)¸ a ≤ (c − 1) + (v − (c − 1))2
1 K1 K5± c = (c = 1) ? v : 1 v = 7, K
c = 3, a = 27{v}
Node (D)2¹a≤v
K7² c = v ³ c = 1 v = 7,³

a = 49≤Figure 2 Map Ma{v,c,c}with the sharp upper-bounds ¶, ·, ¸, ¹ for the number of arcs in adigraph; each node presents an example in brown: given a value for the characteristics attached to
the node, a graph reaching the maximum is described, as a union of cliques Ki , with i vertices, e.g.
in node (B), given the assignments v = 7 and c = 2, the digraph with 2 cliques K2 , K5 reaches the
maximum 29 for the number a of arcs; cond ? x : y denotes x if condition cond holds, y otherwise.

≤
I Example 3 (Extending Ex. 1 to a map of four nodes). Fig. 2 presents Map Ma{v,c,c}, wherewe consider the following characteristics of digraphs: as input characteristics, the number v ofvertices, the number c of connected components, and the number c of vertices of the smallest≤
connected component; as output characteristic, the number a of arcs. In Map Ma{v,c,c},there are four nodes, corresponding to the subsets {v, c, c}, {v, c}, {v, c} and {v}, shown inred, whereas the power set of {v, c, c} contains eight subsets. For the four other subsets,
namely {c, c}, {c}, {c} and ∅, no conjecture can be found, as the number of arcs is not upper

N. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

22:5

bounded wrt these characteristics. In the nodes (A), (B), (C) and (D), the items labelledwith ¶, ·, ¸ and ¹ indicate a maximum conjecture wrt the number a of arcs, while theelements marked with °, ±, ² and ³ show maximality conjectures wrt c and c. For instance,
in Node (B), the maximum conjecture · a ≤ c2 + (v − c)2 really means: among all digraphswith v nodes and whose smallest component contains c nodes, the digraph with most arcs
has exactly c2 + (v − c)2 arcs. Each arc is labelled with a maximality conjecture giving thevalue of the characteristic that is eliminated. For instance, from Node (A) to Node (B), thecharacteristic c that is eliminated from ¶ satisfies this maximality conjecture °: when the
maximum of number of arcs is reached, the value of c is 1 if v = c, 2 otherwise.
Capturing more bounds with secondary characteristics As the number of input characteristics grows, the bound formulae can get rather complicated. Consequently, we introduce
a set A of auxiliary characteristics to obtain simpler formulae. Examples of such auxiliary
characteristics are, for instance, (i) c>1 , (ii) s>1 , and (iii) c∈{2,3} which correspond to (i) the
number of connected components with more than one vertex, (ii) to the number of strongly
connected components with more than one vertex, and (iii) to the number of connectedcomponents with two or three vertices and for which all strongly connected components have
only one vertex. Also initially introduced when searching for lower bounds on the number ofarcs, such characteristics have proved useful for many other bounds. We introduce the notionof secondary characteristics of the node of a map, which will be illustrated in Ex. 5 and 6.
I Definition 4. Given a node of a map that is associated to a subset P ⊆ P of input
characteristics, to an output characteristics o, to a maximum conjecture of the form o ≤ f (P ),and a set of auxiliary characteristics A, the set of secondary characteristics of the node isdefined as the characteristics of the set A ∪ (P − P − {o}) which are functionally determinedby the set P when o = f (P ).
To test that a secondary characteristic is functionally determined by P , we check for eachgenerated combination of values for P that the value of the secondary characteristic is unique.
This test is performed while generating our dataset used for acquiring conjectures.
To find bounds that exploit these secondary characteristics, we use a multi-level approach:(i) first, we look for a formula for each secondary characteristic; (ii) then we try to catcha sharp bound also considering the secondary characteristics for which we could find aformula. Both in (i) and (ii) a formula can either use input characteristics and secondary
characteristics for which we already found a formula. As a result, we obtain formulae thatare easier to interpret, as we can associate a straightforward meaning to the sub-terms thatappear in a bound. Ex. 5 illustrates this point.
I Example 5 (Bound expressed wrt several secondary characteristics). This example shows the
only lower bound found by the Bound Seeker on the number of arcs a of a digraph G wrt thesize c of its largest connected component and the size s of its smallest strongly connectedcomponent. We have P = {v, a, c, c, c, s, s, s}, the bound parameters P = {c, s}, the output
characteristic o = a, and the auxiliary characteristics A = {c>1 , s>1 }. All potential secondary
characteristics A ∪ (P − P − {o}) = {v, c, c, s, s, c>1 , s>1 } are functionally determined by cand s. The lower bound found by the Bound Seeker is a ≥ s>1 − c>1 + v with:• s>1 = min(−s + c + 1, 2 · (s ≥ 2)),
• c>1 = (c = c ? 0 : c),where c = 1 + (((c − 2 · s) ≤ 0) ∧ ((c mod s) ≥ 1)),
• v = ((c − c) = 0 ? c : c + c),
where c = ((2 · s − c) ≤ 0 ? c : s),where a Boolean expression such as (s ≥ 2) is used as an integer, i.e. either 0 for false or 1
for true. While the main formula s>1 − c>1 + v is simple, it uses a secondary characteristic

CP 202222:6

Acquiring Maps of Interrelated Conjectures on Sharp Boundss>1 which is expressed directly wrt c and s, and two other secondary characteristics c>1 andv which mention the two extra secondary characteristics c and c for which two formulae
involving only c and s could be found. The occurrence of Boolean expressions reflects slightvariations in the structure of witness digraphs, i.e. digraphs reaching a sharp bound, as shownin Table 1.
c

s

a

v

c

c

c>1 s>1

6

1

5

6

1

6

1

0

6

3

7

6

1

6

1

2

6

4

10

10

2

4

2

2

6

6

6

6

1

6

1

1

witness digraph

.
.
. . .
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
.
.

.
.
. . .
.

s>1 − c>1 + v
0−1+6
2−1+6
2 − 2 + 10
1−1+6

Table 1 Digraphs minimising the number of arcs for four values of the bound parameters c and s

Within a same map, expressing bounds in terms of secondary characteristics may reveal asame bound formula for several subsets of input characteristics. We observed this phenomenon
in the majority of the acquired maps. Ex. 6 illustrates this for the acquired map giving theupper bound on the number of vertices of the largest connected component of a digraph.
I Example 6 (Map example illustrating how bounds can be unified by using secondary characteristics). In the appendix, Fig. 4 depicts the maximum and maximality conjectures of≤the map Mc{v,c,c,s,s,s}found by the Bound Seeker for the upper-bound on the size of thelargest connected component c with the related links. Note that v needs to be an input
characteristic, as otherwise the upper-bound of c is unbounded. Part (A) shows the 16
bounds found when using only the input characteristics: these bounds are defined by 5
maximum conjectures Ê,. . . ,Î and 4 maximality conjectures ±,. . . ,´. Each link illustrates
how a maximum conjecture is projected onto an other maximum conjecture via a maximality²
conjecture: e.g., the link Î −→ Ê shows how the bound Î c ≤ s − c · s + v is rewritten asÊ c ≤ v as we have ² c = 1. Part (B) shows the bounds found when also using the secondary
characteristics r and c, where r is a secondary characteristic corresponding to v − c · c. We
only have 2 maximum conjectures Ê c ≤ v and Ë c ≤ r + c, where r and c are defined by the
5 maximality conjectures ®,. . . ,² shown on Part (B). The natural upper-bound of c is thenumber of vertices of the digraph (see Ê), unless c or c are part of the input characteristics(see Ë), which requires to consider the feasibility conditions induced by the use of such
inputs.
Missing arcs are due to the lack of functional dependencies. For instance, in Part (A), we
have no arc from {v, s} to {v}, as the number of strongly connected components s is not
functionally determined by the number of vertices v when the sharp bound ¶ is reached, i.e.
. .
when c = v: e.g., for c = v = 2 we both have s = 2 and s = 1 as shown by . . and.

3

A Bound Seeker

3.1

Overview of the map acquisition system

Parts (A) and (B) of Fig. 3 gives the different phases for generating a map: software components are shown in cyan and labelled with capital letters, while data is displayed in orange.
We now detail the phases (A1), (A2), (A3), (B1), (B2), and (B3). To illustrate each phase,a≤
we use the bound table T{v,c},3
provided in Part (C1) of Fig. 3.

each column is an input, a bound,or a secondary characteristic fordigraphs whose number of vertices
does not exceed a given limit.
(A2) Metadata Generationo≤
Metadata (DP,i, P ⊆P, i∈[2,n]):(A3) Meta Metadata Generationo≤Selected Tables (TP,k, P ⊆P ):selected size for each subset ofbound tables from which acquire conjectures.

Candidate Formulae:(B2) CP Model Generation

Candidate Conjectures(B3) Test Conjectures

Selected Conjectureslargest size ncolumns information, row constraints, functional dependencies for each bound table.

(B1) Candidate Generation

select formula type, used functions, and used functional dependency to generate a maximum conjecture of the formo ≤ f (P ) and maximality conjectures for the bound tableo≤TP,k .

22:7(C1) boundtablea≤T{v,c},3

Bound Tables(C) Bound table exampleo≤Bound Tables (TP,i, P ⊆P, i∈[2,n]):Metadata

selected size k(A) Data acquisition for a map MoP≤

(A1) Data Generation (domain dependent)o≤(B) Conjectures acquisition for each table TP,kN. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

v
1
2
2
3
3
3

c
1
1
2
1
2
3

a
1
4
2
9
5
3

c
1
2
1
3
2
1

G
1 K1
2 K2
3 K1 , K1
4 K3
5 K2 , K1
6 K1 , K1 , K1

(C2) corresponding
digraphs

Figure 3 Workflow in the Bound Seeker: (A) data and (B) conjecture acquisition phases;
Phase (A1) with a red background depends on the combinatorial objects we consider (digraphs in ourcase), while Phases (A2), (A3), . . . , (B3) are domain independent; (C1) example of an upper-boundtable for digraphs of at most 3 vertices with the input characteristic v, c, the output characteristics a,and the secondary characteristic c corresponding to the number of vertices of the largest connectedcomponent; (C2) digraphs corresponding to each entry of the bound table shown in (C1).

(A1) Generating data To learn valid conjectures for any digraph of at most k vertices, we
produce all parameter combinations of interest for digraphs up to a maximum number n ofvertices. An exhaustive generation of such data is not a problem, as a program is used forthis purpose. However, the issue is to select the appropriate value of k, neither too small
to create invalid conjectures for digraphs with more than k vertices, nor too large to limit
the number of generated constraints to acquire the conjectures in Phase (B2). To this end,
Phase (A1) produces a table T with the characteristics values for digraphs of at most nvertices in such a way that the size of the table T does not exceed a given memory limit.
With this table T , Phase (A1) extracts for each i between 2 and n, for each subset of inputo≤characteristics P of P, and each output characteristic o, a bound table TP,ibased only on
the entries of T corresponding to digraphs with at most i vertices. Each row of a boundtable represents a feasible combination of values for P , with the corresponding bound value
for o, and the values of the secondary characteristics.
Unlike all the next steps, Phase (A1) depends on the type of combinatorial objects forwhich we generate conjectures. For digraphs, our data generation phase uses a CP model
to produce a set of bound tables that is used by the acquisition process. As illustrated ina≤Part (C1) of Fig. 3, the bound table T{v,c},3
provides a sharp upper bound of the output
characteristic a wrt the input characteristics v and c. A bound table may also mentiona≤secondary characteristics, e.g. c in T{v,c},3, which are functionally determined by the inputa≤characteristics. Each column of the table T{v,c},3
refers to a characteristic, i.e. v, c, a, c,
while each row corresponds to a combination of parameter values for v, c with the associatedmaximum number of arcs a and the value of the secondary characteristic c.
o≤(A2) Generating metadata For each bound table TP,i(with P ⊆ P and i ∈ [2, n]),CP 202222:8

Acquiring Maps of Interrelated Conjectures on Sharp Boundso≤with nrows rows, where TP,i[r, j] denotes the value of the r-th row and the j-th column,o≤Phase (A2) calculates the aggregated information DP,i(with P ⊆ P and i ∈ [2, n]) used to
select the size k employed when searching for the conjectures of the subset P and the output
characteristics o, such as:

The minimum/maximum values of each column and the number of distinct values.
o≤The minimal functional dependencies [24] that determine in the table TP,kthe output
characteristic and the secondary characteristics. Each functional dependency gives a
subset of characteristics that functionally determine another characteristic. For instance,a≤in the bound table T{v,c},3, columns a and c are functionally determined by columns v
and c. But column a is also functionally determined by columns v and c.
o≤Binary constraints between two distinct columns i and j of the table TP,k
, i.e. constraintso≤o≤a≤of the form ∀r ∈ [1, nrows], TP,k [r, i] op TP,k [r, j] (with op ∈ {≤, <, >, ≥}). In T{v,c},3
wehave for each row that the number of vertices is greater than or equal to the number ofconnected components, i.e. v ≥ c, and similarly v ≥ c, a ≥ v, a ≥ c, a ≥ c.
Such knowledge is used to focus the search for conjectures: first by selecting promising
subsets of input parameters for a formula, and second by providing information that avoids
producing meaningless formulae. For instance, we do not generate a formula with a termmin(v, c) as v ≥ c is true. The generated metadata is also the input of the next phase.
(A3) Generating meta metadata to find the relevant size of the training dataset Basedon the information computed by Phase (A2), Phase (A3) determines for the subset P and
the output characteristic o, the size k used when searching for conjectures. To select the sizeo≤k in the datasets TP,i(with i ∈ [2, n]) from which we acquire the conjectures, we operateo≤as follows. As a functional dependency or a binary constraint of a table TP,imay becomeo≤invalid for a table TP,j with j > i, we identify the smallest size k from which the set ofo≤o≤minimal functional dependencies and the set of binary constraints of the tables TP,k
, . . . , TP,nremain identical. In practice, for space reason, we generated digraphs with up to n = 26o≤vertices. To avoid overfitting when the number of rows of table TP,kis too small, we selectthe smallest size corresponding to the table with at least 200 rows: on average, conjectures
were produced using digraphs with up to 18 vertices.
o≤(B1) Generating candidate formulae This phase generates for a bound table TP,k
, partiallyinstantiated candidate formulae to acquire the corresponding maximal and maximality
conjectures. Given the parameters P , the output characteristic o, the set of secondaryo≤characteristics of the selected bound table TP,k
, Phase (B1) produces on request the next
candidate formula to find a conjecture. The set of potential characteristics that the formula
may mention, and the formula itself, are restricted by the functional dependencies and thebinary constraints that were identified by the metadata generation phase. Table 2 showsa≤some candidates formulae that are successively produced for table T{v,c},3.
(B2) Generating a CP model linking a parameterised formula with the data This
phase uses a candidate formula generated by Phase (B1) to post an equational constrainto≤for each entry in a bound table TP,kto obtain a formula where all input parameters andcoefficients are fixed and thus produce a conjecture. Phase (B2) queries Phase (B1) for
the next candidate parameterised formula, tries to instantiate it, and asks again for a next
candidate formula. To find a value for each coefficient of a candidate formula, we use aconstraint model to link a candidate formula to (i) the functional dependencies and binary
constraints identified by the metadata generation phase, and (ii) all the bound table entriesof the selected size. Many constraints break different symmetry types and force all sub-terms

N. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

Candidate formulae generated by Phase (B1)

22:9

Formulae found by Phase (B2)polynomial of degree 1 parameterised by v and c to determine c

c=v−c+1

polynomial of degree 1 parameterised by v and c to determine anonepolynomial of degree 2 parameterised by v and c to determine aa = c2 − 2 · v · c + v 2 − c + 2 · v

polynomial of degree 1 parameterised by v and c to determine anonepolynomial of degree 2 parameterised by v and c to determine aa = c2 − c + v

Table 2 Examples of candidates formulae and corresponding generated formulae for the bounda≤in Part (C1) of Fig 3table T{v,c},3of a formula to be meaningful. The second column of Table 2 shows for each candidate
formula the corresponding concrete formula found by the CP model.
(B3) Testing the candidate conjectures This last phase tests the validity of the conjectureso≤against the largest bound table TP,n
, i.e. against the largest available generated dataset.

3.2

A constraint approach for acquiring symbolic equations

The search for sharp bounds leads to the identification of equations in which the left-handside is an output or a secondary characteristic, and the right-hand side is a formula involving
input and secondary characteristics. As already noted in the introduction of [9] and in
the conclusion of [18], the space of candidate formulae constitutes a major challenge forequation discovery methods. Rather than applying a bottom-up approach that generates
formulae of increasing complexity, we adopt the following strategy. As we aim at finding
simple formulae, we use three complementary classes of formulae that turned out to appear
concomitantly in a map: (1) Boolean formulae involving k arithmetic conditions linked bya single commutative logical operator or by a sum, (2) simple conditional formulae, and(3) formulae over polynomials that can share common sub-expressions. A first attempt touse only polynomials without common sub-expressions missed some formulae, e.g. see Ex. 5,
and quite often provided too complicated formulae, as illustrated in Ex. 8. Based on themetadata introduced in Sect. 3.1, we will present a CP approach for restricting the space of
formulae: for space reasons, we focus on polynomials sharing common sub-expressions.

3.2.1

A parameterised candidate formulae generator for Phase (B1)

Formula syntax All conjectures we generate have the form characteristic op formula, where
op is one of the comparison operators ≤, =, ≥, and formula is a formula involving a setof characteristics. Consequently, formulae are described by the following set of simplified
grammar rules, where “Small Capitals” indicates a non-terminal symbol, “Roman” denotes
a function or a known constant, “Italic” highlights a (digraph) characteristics, “Bold” denotes
an unknown integer constant. Within these rules, polynomial(Params, degree) denotes apolynomial whose maximum degree is fixed (with degree > 0) on a non-empty subsetof parameters of its potential parameters Params, and the functions geq0(x), geq(x, y),sum_consec(x), cmod(x, y), dmod(x, y) resp. stand for 1 if x ≥ 0 otherwise 0, 1 if x ≥ yotherwise 0, x·(x+1), x − (y mod x), x − (x mod y).
2
Formula::= cst | Bool | cst + Bool | Cond | Pol | PolBinary | PolUnary

Bool::= BoolOp(BoolConds)

BoolOp ::= ∧| ∨ | = |+BoolConds ::= BoolCond, BoolConds | BoolCond
BoolCond ::= Param Cmp cst

Cmp ::= ≤ | = | ≥ | 6=

CP 202222:10Acquiring Maps of Interrelated Conjectures on Sharp Bounds

Cond::= (BoolCond ? ParamCst : ParamCst) ParamCst ::= Param|cst

Pol::= polynomial(Params, degree)

PolBinary ::= Bf(Pol, Pol)Bf ::= min | max | floor | mod | cmod | dmod | prod

PolUnary ::= Uf1(Pol) | Uf2(Pol, cst)
Uf1::= geq0 | sum_consec

Params::= Param∗ Param ::= Char|BTerm|UTerm Char ::= v|c|c|c|s|s|s

Uf2 ::= min | max | floor | mod | power

BTerm::= Bt(Char, Char)UTerm::= sum_consec(Char) | Ut(Char, cst) | Char ∈ [cst, cst]

Bt::= min | max | floor | ceil | mod | cmod | dmod | prod

Ut::= min | max | floor | ceil | mod | geq | power

I Example 7 (Examples of generated Boolean, conditional, polynomial formulae).
• (s = 1) ∧ (c ∈ [2, 3]) and (v = c) = (c = 1), where the 2nd formula denotes a condition
that is satisfied only if both conditions (v = c) and (c = 1) are true, or both false.
• (s = 1 ? d v2 e : v) and ((c − c) = 0 ? c : c + c), where (cond ? x : y) denotes x if thecondition cond holds, y otherwise.
c• (v mod c)2 −c·(v mod c)+v·c where v mod c is a shared binary term BTerm, b (s≥2)+s+v
2
where (s ≥ 2) is a unary term UTerm of the form geq(s, 2).
I Example 8 (Finding simpler bounds using Boolean and conditional formulae). We illustratewith an example generated by the system on the lower bound of the number of arcs a wrt thesize of the smallest and largest connected components c and c, and the size s of the largest
strongly connected component, how using Boolean and conditional formulae often leads tosimpler conjectures. Without using Boolean and conditionals, we get a ≥ s>1 − c>1 + v withs>1 = min(s−1, 1), c>1 = min(min(c, 2), min(c, 2)+c−c−1), and v = min(c+c, c·c−c2 +c);
enabling Boolean and conditional formulae, we get the simpler bound: a ≥ s>1 − c>1 + v
with s>1 = (s ≥ 2), c>1 = (c ≥ 2) + ((c − c) ≥ 1), and v = ((c − c) = 0 ? c : c + c).
Candidate formulae generator Since we want to try out a variety of formulae, we createa parameterised candidate formulae generator, which, upon backtracking, proposes a new
candidate formula with non-fixed coefficients; these are variables for the constants and for the
input characteristics that will be used in a candidate formula. In this generator we specify:
The structure of the formula, that is whether we use (1) a Boolean formula, (2) a simple
conditional formula, or (3) a formula over polynomials; in this later case we also specify
how many unary and binary terms occur in each polynomial.
The arithmetic functions we may use in the terms.
The complexity of a polynomial, that is its potential maximum degree, its maximum
number of non-zero coefficients, the ranges of its coefficients.
The list of possible combinations of characteristics that the candidate formula can use in
its parameters. Such combinations correspond to functional dependencies identified by
the metadata generation phase, i.e. Phase (A2).
We use more than one generator to design a formula generation policy where the simplest
candidate formulae are tried first.

3.2.2

Constraint model for acquiring a conjecture for formulae overpolynomials for Phase (B2)

Given a candidate formula F, (corresponding either to Pol, to PolBinary, or to PolUnary
as described in the set of grammar rules in Sect. 3.2.1), for which the set of used parameters

N. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

22:11

is partially determined, and for which the coefficients are not yet fixed, we create a constraint
model that relates these unknowns to all rows in a bound table. Our model includes four typesof constraints, namely (i) structural constraints on the input and secondary characteristics
that will be used in F, (ii) symmetry-breaking constraints, (iii) constraints preventing thegeneration of formulae in which a term could be simplified, and (iv) equational constraints
on each row of a bound table. We describe the model variables, the constraints on thecharacteristics used in F, the constraints on the unary/binary terms and binary functionof F, and the equational constraints on the table entries. The number of variables andconstraints of the model is linear wrt the number of table entries as it is dominated by
the equational constraints. For reasons of space, concerning the constraints of the type (ii)and (iii), we will only detail the constraints related to the min function.

Variables used in the model Table 3 introduces the variables used to represent a nonconstant formula F involving at most nc characteristics (i.e. input and secondary characteristics), nu unary terms, nb binary terms, and np polynomials, wrt a bound table T ofnrows rows. We use n as a shortcut for nc + nu + nb . For the binary term Bi , the variables
B_IND1 i , B_IND2 i , B_O i designate a term with the arguments (CB_IND1 i , CB_IND2 i )when B_O i = 0, and (CB_IND2 i , CB_IND1 i ) otherwise. When the binary term is commutative, e.g. min, the order of the arguments is irrelevant and B_O i will be set to 0 (seeconstraint (4.c) in Table 4), but otherwise, e.g. mod, the order matters.

Objects
Characteristics Cj(j ∈ [1, nc ])Unary term Ui(i ∈ [1, nu ])Variables
Cj ∈ {0, 1}

U _VALi,rBinary term Bi

Bi,j ∈ {0, 1}(j ∈ [1, nc ])B_IND1 i ∈ [1, nc ]B_IND2 i ∈ [1, nc ]B_O i ∈ {0, 1}(r ∈ [1, nrows])
Polynomial Piof degree di(i ∈ [1, np ])(r ∈ [1, nrows])

Cj = 1 iff Cj used by formula F

Ui,j ∈ {0, 1}(j ∈ [1, nc ])U _IND i ∈ [1, nc ]U _MIN i
U _MAX i
U _CST i(r ∈ [1, nrows])(i ∈ [1, nb ])Comments

Ui,j = 1 iff Cj used by Ui
index of the used characteristics
minimum value of the used characteristics
maximum value of the used characteristics
constant used in Uivalue of term Ui wrt r-th row and thej-th column (with Ui,j = 1 ) of table T
Bi,j = 1 iff Cj used by Bi
index of first used characteristic
index of second used characteristic
order of used characteristics in arguments
value of term Bi wrt r-th row, the B_IND1 i -th,and the B_IND2 i -th columns of table T

B_VALi,rPi,j ∈ {0, 1}
with j ∈ [1, n] andn = nc + nu + nb
Mi,k 
i(k ∈ [1, n+d])di
P_VALi,r(Pi,j = 1, j ∈ [1, nc ]⇒ Cjused by Pi
Pi,j = 1, j ∈ [nc + 1, ncu ] ⇒ Uj−nc
used by Pi
Pi,j = 1, j ∈ [ncu + 1, n] ⇒ Bj−nc −nu used by Pi
Mi,k is the k-th coefficient of Pi , thecoefficient with the largest k is the constantvalue of polynomial Pi wrt r-th row of table T

Table 3 Variables of the model, where ncu is an abbreviation of the term nc + nu

Constraints on the structure of the formula The upper part of Table 4 lists the con-

CP 202222:12Acquiring Maps of Interrelated Conjectures on Sharp Bounds

straints, (i) specifying which characteristics the formula F uses, i.e. see (1a), (ii) forcing aunary term, a binary term, and a polynomial to use the appropriate number of characteristics,
i.e. see (2a), (3a) and (4a), (iii) connecting the characteristics used by the unary and binary
terms with the characteristics used in the polynomials and the formula, i.e. see (5a), (6a),(iv) restricting non-zero coefficients of polynomials, i.e. see (7a), (8a).

Constraints on unary/binary terms and on a binary function Within Table 4, constraint (1b) (resp. (1c), (2c)), links the 0-1 variables Ui,j (resp. Bi,j ) to the index of
the characteristic involved in the term. To avoid generating unary terms of the formmin(Characteristic, Cst) which could just be rewritten as Characteristic or as Cst, constraint (4b) restricts the minimum and maximum values of the constant. When using the minfunction in a binary term, constraint (4c) avoids generating equivalent binary terms whose arguments are permuted. Constraint (5c) prevents generating a binary term when the min could
be simplified, e.g. avoids generating min(c, c) as the metadata information found in Phase (A2)indicates that c is always smaller than or equal to c. Finally, when the candidate formula F
is a binary function corresponding to min, that uses the polynomials P1 and P2 of degree d,we post the lexicographic ordering constraint hM1,1 , . . . , M1,(n+d) i <lex hM2,1 , . . . , M2,(n+d) idd
between the monomial coefficients of P1 and P2 . Note that, for space reason, besides constraints (4b), (4c), and (5c), we omit in Table 4 the symmetry and simplification constraints
related to functions that are different from min.
Equational constraints For each row r of the bound table T we post some constraints
linking the selected characteristics Cj with (i) the value variable U _VALi,r of each unaryterm Ui , (ii) the value variable B_VALi,r of each binary term Bi , and (iii) the value variable
P_VALi,r of each polynomial Pi . For each row r we also post an equality constraint linking
the value of the candidate formula F on row r with the corresponding bound value on thesame row. Finally, for a binary function min between two polynomial P1 and P2 , we imposethat for at least one of the entries of the bound table the value of P1 is strictly less than thevalue of P2 on the same entry, and that the converse applies for another entry of the table.
To avoid unnecessarily complex formulae, we minimise the sum of the absolute values of thecoefficients of a candidate formula F.

4

Evaluation of the Bound Seeker

We focus on constructing 16 maps on the lower and upper-bounds of the number of vertices,
the number of arcs, the number of connected (resp. strongly connected) components, and theirminimum and maximum sizes. The components of the system are written in SICStus Prolog
and consist of 10000 lines of code for the Data Generation, the Metadata Generation, theMeta Metadata Generation, the Candidate Formulae Generation, the CP Model Generation,and the Test phase. The Data Generation phase generates a total of 1944 bound tables(occupying 2 Gb) for each maximum number of digraph vertices ranging from 2 to 26; eachbound table gives the lower or upper-bound of a characteristic wrt different subsets of input
characteristics. We evaluate the Bound Seeker from several standpoints:
The percentage of conjectures that, while acquired from the size selected by the Meta
Metadata, still hold for all entries of the largest generated bound tables, i.e. the tables ofdigraphs containing up to 26 vertices.
The percentage of bounds from the database of invariants in [2] that was retrieved (resp.
not found).

N. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

Constraints

Comments(1a) table(hC1 , . . . , Cc i, fd_table)(3a) ∀i ∈ [1, nb ] :Pj=nc
Ui,j = 1
j=1
Pj=n
c

(4a) ∀i ∈ [1, np ] :P(2a) ∀i ∈ [1, nu ] :restrict the char. used in F
Ui uses 1 char.
Bi uses 2 char.
Pi uses at least one char., orat least one unary or binary term

Bi,j = 2

j=1

Pi,j ≥ 1j∈[1,n]W∀j ∈ [1, nc ] : Cj = i∈[1,nu ] Ui,j ∨WW(5a)i∈[1,nb ]22:13

Bi,j ∨(6a) ∀j ∈ [nc + 1, n] :i∈[1,np ]Pi∈[1,np ]i
Pk<(n+ddi )(7a) ∀i ∈ [1, np ] : (k=1

iPk≤(n+ddi )(8a) ∀i ∈ [1, np ] : (k=1

link Ui,j , Bi,j , and Pi,j to Cj

Pi,jforce each unary/binary term to
be used by at least 1 polynomial

Pi,j > 0[Mi,k 6= 0]) > 0

polynomials are not constanteach polynomial has a maximum
number of non-zeros coefficients[Mi,k 6= 0]) ≤ maxz(1b) element(U _IND i , hUi,1 , . . . , Ui,nc i, 1)

get index of used char.

(2b) element(U _IND i , hmin 1 , . . . , min nc i, U _MIN i )get min. value of used char.

(3b) element(U _IND i , hmax 1 , . . . , max nc i, U _MAX i )get max. value of used char.

(4b) ufi ∈ {min} ⇒U _CST i > U _MIN i
U _CST i < U _MAX icannot simplify unary term Ui ,as otherwise could remove Ui(1c) element(B_IND1 i , hBi,1 , . . . , Bi,nc i, 1)

get index of first used char.

(2c) element(B_IND2 i , hBi,1 , . . . , Bi,nc i, 1)

get index of second used char.

(3c) B_IND1 i < B_IND2 i

indexes are ordered
fix order of the 2 arguments as
min is a commutative function
assign two char.whose
values are not ordered(4c) bfi ∈ {min} ⇒ B_O i = 0(5c) bfi ∈ {min} ⇒ table

hB_IND1 i , B_IND2 i i,
table_unordered

Table 4 (Top) Constraints on the structure of a formula F; fd_table is the list of characteristics
combinations that may be used by F, created by the candidate formulae generator, while maxz isthe maximum number of non-zero coefficients of a polynomial. (Mid) Constraints on a unary termUi (with i ∈ [1, nu ]), where ufi is the function assigned to Ui , min j (with j ∈ [1, nc ]), is the smallest
value of the j-th characteristic. (Bottom) Constraints on a binary term Bi (with i ∈ [1, nb ]), wherebfi is the function assigned to Bi , and table_unordered is the set of pairs of characteristics
indices such that the 1st characteristic is not always smaller, or greater, than 2nd characteristic;
char. is an abbreviation for characteristic.

Besides the conjectures retrieved from the global constraint catalogue database, we manually proved ten new conjectures. Using WolframAlpha, we also checked the consistencyof 105 projections of a sharp bound B1 onto a sharp bound B0 involving one less input
characteristic, by substituting in B1 the input characteristic to be eliminated, by theexpression defined by the corresponding maximality conjecture.
As the complexity of a formula increases with the number of input characteristics, we limit
our evaluation to up to 3 input characteristics. All experiments to acquire the conjectures forthe 16 maps were done using the same system parameters, i.e. none of the components havebeen tuned manually to behave differently depending on the considered map. Out of 350(resp. 202) combinations of input characteristics for which the Bound Seeker tried to find a
sharp lower (resp. upper) bound, using only polynomials, it got at least one sharp boundfor 279 (resp. 149) combinations of characteristics, as well as 1236 (resp. 975) minimality(resp. maximality) conjectures. Using also Boolean and conditional expressions it found 3
extra lower bounds and 93 new maximality/minimality conjectures. Table 5 provides the

CP 202222:14

Acquiring Maps of Interrelated Conjectures on Sharp Bounds

Maps

only Poly

Bool/Cond/Poly

Maps#P1 Time #B2 #C2 #P2 Time
McP≥
McP≥
MsP≥
MaP≥
c≥
MP
s≥
MP
MsP≥
MvP≥

259 257
129 230
97 130367 1248
63 1674354
263 474
294 368

47
0
0
38
10
0
37
30

25
13
8
102
27
18
31
75

194 533
120 476
90 306
255 3180
27 38825 226
198 813205 1570

only Poly

Bool/Cond/Poly#P1 Time #B2 #C2 #P2 Time
McP≤
McP≤
MsP≤
MaP≤
c≤
MP
s≤
MP
MsP≤
MvP≤

100 218153 193
102 392384 2505
130 223
48 17193 100
14
7

9
32
15
46
16
1
5
0

17
31
31
84
14
8
17
2

77 43994 54260 999264 5939
102 457
40 36573 267
12
90

Table 5 Number of minimum/maximum and minimality/maximality conjectures found for eachof the 16 maps and time in min. using only polynomials (see only Poly), and using Booleans,conditionals and polynomials (see Bool/Cond/Poly)

3

Total

Percentage

14

4

40

66,66%

3

0

4

6,66%

6

0

6

10%

1

1

1

3

5%

Number of bounds in the GCC not retrieved by BS

0

0

7

7

11,66%

Total bounds of the GCC per column

24

24

12

60

Number of input characteristics

1

Number of equivalent sharp bounds retrieved by BS

22

Number of sharper bounds than the GCC found by BS

1

Number of generalised sharp bounds found by BS

0

Number of erroneous bounds found in the GCC by BS

2

Table 6 Comparing the conjectures on the bounds found by the Bound Seeker (BS) with the
database of invariants of the global constraint catalogue (GCC)

results for the 16 maps using SICStus 4.6.0 on a 2015 iMac with a 4 GHz Core i7 and 32Gbof memory: for each map, we give the number of formulae found using only polynomials(see col. #P1), then using Boolean, conditional, and polynomial (see col. #B2, #C2 and#P2). Using Boolean and conditional expressions generates 3.8% new formulae compared
to when using polynomials alone; moreover, 31.07% of the formulae that use polynomials
are replaced by simpler formulae that use Boolean or conditionals expressions. The timespent is explained by a significant number of candidate formulae tested, as it comes from the
combination of minimal functional dependencies and grammar rules. Moreover, arithmetic
constraints like div and mod with multiple occurrences of the same variable are handledpoorly by CP solvers. The datasets used in the experiments and the sixteen maps found will
be available for download in a technical report.

Evaluation of the acquired conjectures wrt the largest data sets Of the 3625 conjecturesacquired when only using polynomials, we found 5 invalid conjectures when tested against
all samples of the largest data set, i.e. all digraphs up to 26 vertices. Of the 3264 conjecturesacquired when also using Boolean and conditional expressions, we found 16 invalid conjectures.
Note that in this setting the Bound Seeker does not try to find polynomial formulae if italready found a Boolean or a conditional formula.
Comparing the conjectures founds with proved bounds of the constraint catalogue As
shown in Table 6, the Bound Seeker retrieves 66.66% of the bounds of the constraint catalogue,even if the resulting formulae have sometimes a different form: e.g., the upper-bound on the

N. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

22:15

number of arcs a wrt the number of vertices v, connected components c, and strongly connectedcomponents s in the catalogue is expressed as a ≤ c−1+(v −s+1)·(v −c+1)+b (s−c+1)·(s−c)
c,2r 2 +s2 +v·c+r−s+v

while the Bound Seeker finds the equivalent inequality a ≤ bc, with c =2max(2 · v − v · c, 1), s = v − s + 1 and r = v · [c ≥ 2] − c · [c ≥ 2]; r is a secondary characteristic
corresponding to v −c·c. Unlike the bound given by [2], the bound found by the Bound Seeker
defines the size c of the smallest connected component, and the size s of the largest strongly
connected component of those extreme digraphs for which the upper-bound is reached.
An example of a generalised bound found by the Bound Seeker is the lower bounda ≥ ((v − c) ≤ 1 ? max(v − 1, 1) : v − 2), with v = (c = c ? c : c + c) which extends thecatalogue bound c 6= c ⇒ a ≥ c + c − 2 + (c = 1). An example of correct bound foundby the Bound Seeker replacing the erroneous bound (i) a ≥ v − b s−1
2 c of the catalogue isc):(ii) a ≥ v − c∈{2,3} with c∈{2,3} = (v = s ? b v2 c : b s−1
for
the
edge
conditionv = s = 2, (i)2returns 2, rather than 1 as (ii) does. Bound (ii) a ≥ v − c∈{2,3} can be interpreted as follows:
to minimise the number of arcs, one has to maximise the number of connected componentsof the form . ., . . ., . . . or . . . . The missing bounds of the catalogue are partiallyexplained by the limited complexity of the common subexpressions (see BTerm, UTerm in
Sect. 3.2.1) of our polynomials, and by the lack of some secondary characteristics.

5

Related work

While there exist several discovery programs in the context of mathematics devoted to set
theory, number theory, finite algebra and knot theory [12, 23, 13], only a few systems focus
on finding bounds between characteristics of a combinatorial object. The two most notablesystems are S. Fajtlowicz’s Graffiti program [14] and P. Hansen’s AutoGraphiX system [1, 17].
The first difference is that the Bound Seeker attempts to systematically construct a set of
sharp bounds on all possible combinations of a set of input characteristics. The second maindifference is that the Bound Seeker introduces secondary characteristics and searches for key
properties of extreme combinatorial objects for which the bounds are reached.
In slightly different domains, recent work in CP uses machine learning techniques toestimate the domain boundaries of an objective function [30] of an optimisation problem. Someother work uses CP to extract equations from a spreadsheet [18, 25], and some recent work
investigates how to integrate integer programming solvers within neural networks [15, 26].
The specificity of our approach compared to machine learning and constraint acquisition [7]is twofold: (i) we can generate our input data, but we need to ensure that these data containthe correct values of the sharp bounds we consider, as otherwise, we would necessarily obtainwrong maximal conjectures; moreover, maximality conjectures only make sense for sharpbounds; (ii) we have to learn concise conjectures that fit perfectly to all available data, as
minimising an error measure would be irrelevant for acquiring conjectures on sharp bounds.

6

Conclusion

We introduce a structure that connects a set of sharp bounds. Based on this structure, we
propose a constructive approach to acquire a set of interrelated conjectures on sharp bounds.
We show the relevance of using a variety of types of formulae, i.e., Boolean, conditionals, andpolynomials with shared sub-expressions, to acquire simpler conjectures. This work opens
a new application domain for CP for automated conjectures-making systems. It creates a
new line of research to those already reported in a recent survey on machine learning for
combinatorial optimisation [5].

CP 202222:16

Acquiring Maps of Interrelated Conjectures on Sharp Bounds

References
1
2

3

4

5
6

7
8

9

10

11

12

13

Mustapha Aouchiche, Gilles Caporossi, Pierre Hansen, and M. Laffay. Autographix: a survey.
Electron. Notes Discret. Math., 22:515–520, 2005. doi:10.1016/j.endm.2005.06.090.
Nicolas Beldiceanu, Mats Carlsson, and Jean-Xavier Rampon. Global Constraint Catalog, 2nd
Edition (revision a). Technical Report T2012-03, Swedish Institute of Computer Science, 2012.
Available at http://ri.diva-portal.org/smash/get/diva2:1043063/FULLTEXT01.pdf.
Nicolas Beldiceanu, Mats Carlsson, Jean-Xavier Rampon, and Charlotte Truchet. Graphinvariants as necessary conditions for global constraints. In Peter van Beek, editor, Principles
and Practice of Constraint Programming - CP 2005, 11th International Conference, CP 2005,
Sitges, Spain, October 1-5, 2005, Proceedings, volume 3709 of Lecture Notes in Computer
Science, pages 92–106. Springer, 2005.
Nicolas Beldiceanu and Helmut Simonis. A Model Seeker: Extracting Global Constraint Models
from Positive Examples. In Michela Milano, editor, Principles and Practice of Constraint
Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October
8-12, 2012. Proceedings, volume 7514 of Lecture Notes in Computer Science, pages 141–157.
Springer, 2012. doi:10.1007/978-3-642-33558-7\_13.
Yoshua Bengio, Andrea Lodi, and Antoine Prouvost. Machine learning for combinatorial
optimization: A methodological tour d’horizon. Eur. J. Oper. Res., 290(2):405–421, 2021.
Christian Bessière, Emmanuel Hebrard, George Katsirelos, Zeynep Kızıltan, Émilie PicardCantin, Claude-Guy Quimper, and Toby Walsh. The balance constraint family. In BarryO’Sullivan, editor, Principles and Practice of Constraint Programming - 20th International
Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, volume 8656 of Lecture
Notes in Computer Science, pages 174–189. Springer, 2014.
Christian Bessière, Frédéric Koriche, Nadjib Lazaar, and Barry O’Sullivan. Constraintacquisition. Artif. Intell., 244:315–342, 2017. doi:10.1016/j.artint.2015.08.001.
V. Brankov, P. Hansen, and D. Stevanović. Automated conjectures on upper bounds for thelargest laplacian eigenvalue of graphs. Linear Algebra and its Applications, 414(2):407–424,
2006.
Jure Brence, Ljupčo Todorovski, and Sašo Džeroski. Probabilistic grammars for equation
discovery. Knowledge-Based Systems, 224:107077, 2021. URL: https://www.sciencedirect.
com/science/article/pii/S0950705121003403, doi:https://doi.org/10.1016/j.knosys.
2021.107077.
Céline Brouard, Simon de Givry, and Thomas Schiex. Pushing data into CP models usinggraphical model learning and solving. In Helmut Simonis, editor, Principles and Practiceof Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve,
Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer
Science, pages 811–827. Springer, 2020. doi:10.1007/978-3-030-58475-7\_47.
John William Charnley, Simon Colton, and Ian Miguel. Automatic generation of implied
constraints. In Gerhard Brewka, Silvia Coradeschi, Anna Perini, and Paolo Traverso, editors,
ECAI 2006, 17th European Conference on Artificial Intelligence, August 29 - September 1, 2006,
Riva del Garda, Italy, Including Prestigious Applications of Intelligent Systems (PAIS 2006),
Proceedings, volume 141 of Frontiers in Artificial Intelligence and Applications, pages 73–77. IOS
Press, 2006. URL: http://www.booksonline.iospress.nl/Content/View.aspx?piid=1649.
Simon Colton, Andreas Meier, Volker Sorge, and Roy L. McCasland. Automatic generationof classification theorems for finite algebras. In David A. Basin and Michaël Rusinowitch,
editors, Automated Reasoning - Second International Joint Conference, IJCAR 2004, Cork,
Ireland, July 4-8, 2004, Proceedings, volume 3097 of Lecture Notes in Computer Science, pages
400–414. Springer, 2004. doi:10.1007/978-3-540-25984-8\_30.
Alex Davies, Petar Veličković, Lars Buesing, Sam Blackwell, Daniel Zheng, Nenad Tomašev,
Richard Tanburn, Peter Battaglia, Charles Blundell, András Juhász, Marc Lackenby, Geordie
Williamson, Demis Hassabis, and Pushmeet Kohli. Advancing mathematics by guiding

N. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

14
15

16

17

18

19

20

21
22

23
24

25

26

27

22:17

human intuition with ai. Nature, 600(7887):70–74, 2021. URL: https://doi.org/10.1038/
s41586-021-04086-x.
Siemion Fajtlowicz. On conjectures of Graffiti. Discret. Math., 72(1-3):113–118, 1988. doi:
10.1016/0012-365X(88)90199-9.
Aaron M. Ferber, Bryan Wilder, Bistra Dilkina, and Milind Tambe. Mipaal: Mixed integer
program as a layer. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI
2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI
2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI
2020, New York, NY, USA, February 7-12, 2020, pages 1504–1511. AAAI Press, 2020. URL:
https://aaai.org/ojs/index.php/AAAI/article/view/5509.
Minh Hoàng Hà, Claude-Guy Quimper, and Louis-Martin Rousseau. General bounding
mechanism for constraint programs. In Gilles Pesant, editor, Principles and Practice ofConstraint Programming - 21st International Conference, CP 2015, Cork, Ireland, August 31 September 4, 2015, Proceedings, volume 9255 of Lecture Notes in Computer Science, pages
158–172. Springer, 2015.
Pierre Hansen and Gilles Caporossi. Autographix: An automated system for finding conjectures in graph theory. Electron. Notes Discret. Math., 5:158–161, 2000. doi:10.1016/
S1571-0653(05)80151-9.
Samuel Kolb, Sergey Paramonov, Tias Guns, and Luc De Raedt. Learning constraints inspreadsheets and tabular data. Mach. Learn., 106(9-10):1441–1468, 2017. doi:10.1007/
s10994-017-5640-x.
Mohit Kumar, Stefano Teso, and Luc De Raedt. Acquiring integer programs from data. In Sarit
Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial
Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019, pages 1130–1136. ijcai.org, 2019.
doi:10.24963/ijcai.2019/158.
Guillaume Lample and François Charton. Deep learning for symbolic mathematics. In 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April
26-30, 2020. OpenReview.net, 2020. URL: https://openreview.net/forum?id=S1eZYeHFDS.
Craig E. Larson and Nicolas Van Cleemput. Automated conjecturing I: Fajtlowicz’s Dalmatianheuristic revisited. Artif. Intell., 231:17–38, 2016. doi:10.1016/j.artint.2015.10.002.
Jimmy Ho-Man Lee, Ka Lun Leung, and Yu Wai Shum. Consistency techniques for polytime
linear global cost functions in weighted constraint satisfaction. Constraints, 19(3):270–308,
2014.
Doug Lenat. AM: An artificial intelligence approach to discovery in mathematics. PhD thesis,
Stanford University, 1976.
Thorsten Papenbrock, Jens Ehrlich, Jannik Marten, Tommy Neubert, Jan-Peer Rudolph,
Martin Schönberg, Jakob Zwiener, and Felix Naumann. Functional dependency discovery: An
experimental evaluation of seven algorithms. Proc. VLDB Endow., 8(10):1082–1093, 2015.
URL: http://www.vldb.org/pvldb/vol8/p1082-papenbrock.pdf, doi:10.14778/2794367.
2794377.
Sergey Paramonov, Samuel Kolb, Tias Guns, and Luc De Raedt. Tacle: Learning constraints intabular data. In Ee-Peng Lim, Marianne Winslett, Mark Sanderson, Ada Wai-Chee Fu, JimengSun, J. Shane Culpepper, Eric Lo, Joyce C. Ho, Debora Donato, Rakesh Agrawal, Yu Zheng,
Carlos Castillo, Aixin Sun, Vincent S. Tseng, and Chenliang Li, editors, Proceedings of the2017 ACM on Conference on Information and Knowledge Management, CIKM 2017, Singapore,
November 06 - 10, 2017, pages 2511–2514. ACM, 2017. doi:10.1145/3132847.3133193.
Anselm Paulus, Michal Rolínek, Vít Musil, Brandon Amos, and Georg Martius. Comboptnet:
Fit the Right NP-Hard Problem by Learning Integer Programming Constraints, 2021. arXiv:
2105.02343.
Émilie Picard-Cantin, Mathieu Bouchard, Claude-Guy Quimper, and Jason Sweeney. Learning
the parameters of global constraints using branch-and-bound. In J. Christopher Beck, editor,
Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017,

CP 202222:18Acquiring Maps of Interrelated Conjectures on Sharp Bounds

28

29

30

31

32

Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10416 of Lecture
Notes in Computer Science, pages 512–528. Springer, 2017. doi:10.1007/978-3-319-66158-2\_33.
Steve Prestwich. Robust constraint acquisition by sequential analysis. In Giuseppe De Giacomo,
Alejandro Catalá, Bistra Dilkina, Michela Milano, Senén Barro, Alberto Bugarín, and Jérôme
Lang, editors, ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8
September 2020, Santiago de Compostela, Spain, August 29 - September 8, 2020 - Including
10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020), volume
325 of Frontiers in Artificial Intelligence and Applications, pages 355–362. IOS Press, 2020.
doi:10.3233/FAIA200113.
Gal Raayoni, Shahar Gottlieb, Yahel Manor, George Pisha, Yoav Harris, Uri Mendlovic, Doron
Haviv, Yaron Hadad, and Ido Kaminer. Generating conjectures on fundamental constants
with the Ramanujan Machine. Nature, 590:67–73, 2021. URL: https://doi.org/10.1038/
s41586-021-03229-4.
Helge Spieker and Arnaud Gotlieb. Learning objective boundaries for constraint optimization
problems. In Giuseppe Nicosia, Varun Kumar Ojha, Emanuele La Malfa, Giorgio Jansen,
Vincenzo Sciacca, Panos M. Pardalos, Giovanni Giuffrida, and Renato Umeton, editors,
Machine Learning, Optimization, and Data Science - 6th International Conference, LOD 2020,
Siena, Italy, July 19-23, 2020, Revised Selected Papers, Part II, volume 12566 of Lecture Notes
in Computer Science, pages 394–408. Springer, 2020. doi:10.1007/978-3-030-64580-9\_33.
Ljupco Todorovski. Equation discovery. In Claude Sammut and Geoffrey I. Webb, editors, Encyclopedia of Machine Learning, pages 327–330. Springer, 2010. doi:10.1007/
978-0-387-30164-8\_258.
Hao Wang. Toward mechanical mathematics. In Jörg Siekmann and Graham Wrightson,
editors, Automation of Reasoning: Classical Papers on Computational Logic 1957–1966, pages
244–264. Springer-Verlag, Berlin, 1983.

N. Beldiceanu, J. Cheukam-Ngouonou, R. Douence, R. Gindullin and C.-G. Quimper

A

22:19

Map example

Ì{v, c, s}

Í{v, c, c}

Ê{v, s, s}Ì{v, c, s}Ê c≤v

Ì{v, c, s} Ë c ≤ v − c + 1

Ì c ≤ (v = c ? v : v − c)
Í c≤c−c·c+v
Ê±²{v, s} Ë³{v, c}
Ê±²{v}
Ì´{v, c} Ê±²{v, s} Ê±²{v, s} Î c ≤ s − c · s + v
²
±
± c=v
²
²
² (A)
² c=1
Ë{v, c, s}
Ê{v, s, s}Ê{v, s, s}Ë{v, c, s}
Î{v, c, s} ³ c = (c = 1 ? v : 1)
´ c = 1 + (v 6= c)Ê c≤v Ë c≤r+cË¯{v, c, s}
Ë°{v, c, c}
Ê{v, s, s}Ë¯{v, c, s} Ë¯{v, c, s}® r = 0, c = v¯ r = max(v − 2 · c, 0)
®
±
¯
®
®
° r = v − c · c±Ê®{v, s}³´

Ë±{v, c}

®

Ê®{v}

®

Ë¯{v, c}®
Ë±{v, c, s}

Ê{v, s, s}Ê{v, s, s}±±Ê®{v, s}Ê®{v, s}

®

®

(B)

Ë±{v, c, s} Ë²{v, c, s}±²

r = v · (c ≥ 2) − c · (c ≥ 2)

c = max(2 · v − v · c, 1)
r = v + s · (c = 1) − c · s−v · (c = 1)

c = max(2 · v − v · c, s)≤
Figure 4 Map Mc{v,c,c,s,s,s}of upper-bounds of the output characteristic c found by the
Bound Seeker, where each dotted node contains, from left to right, a reference to the maximum
conjecture ¶,. . . ,º, ¶,·, possibly a set of maximality conjectures ±,. . . ,´,®,. . . ,², and the set of
input characteristics in red; Part (A) corresponds to the bounds found while only using the input
characteristics, and Part (B) refers to the bounds found using also the secondary characteristics.

CP 2022