Improving IntSat by expressing disjunctions of bounds as linear constraints

Abstract

Conflict-Driven Clause Learning (CDCL) SAT solvers can automatically solve very large real-world problems. IntSat is a new technique extending CDCL to Integer Linear Programming (ILP). For some conflicts, IntSat generates no strong enough ILP constraint, and the backjump has to be done based on the conflicting set of bounds. The techniques given in this article precisely analyze how and when that set can be translated into the required new ILP constraint. Moreover, this can be done efficiently. This obviously strengthens learning and significantly improves the performance of IntSat (as confirmed by our experiments). We also briefly discuss extensions and other applications.

Keywords

SAT conflict-driven clause learning constraint programming integer linear programming

1. Introduction and problem statement

One of the most remarkable successes of AI technology is probably the combination of heuristics, learning and novel datastructures that allow Conflict-Driven Clause Learning (CDCL) propositional SAT solvers to solve, fully automatically, very large and hard real-world industrial and scientific problem instances. It is therefore not surprising that for many years researchers have tried to produce effective extensions of CDCL able to handle richer constraint languages. In fact, SAT can be seen as the particular case of Integer Linear Programming (ILP) where all variables are binary (0–1) and constraints have the form $x_{1} + \dots + x_{m} - y_{1} - \dots - y_{n} > - n$ (usually written as clauses $x_{1} \lor \dots \lor x_{m} \lor \overline{y_{1}} \lor \dots \lor \overline{y_{n}}$ , i.e., sets (disjunctions) of literals). Of course arbitrary ILP constraints can be encoded into clauses, but handling them natively opens the door to far more compact and efficient reasoning, learning and optimization.

Indeed, an extensive amount of work exists on CDCL-like techniques for pseudo-Boolean solving (a.k.a. 0–1 ILP), which considers Boolean variables, arbitrary linear constraints of the form $a_{1} x_{1} + \dots + a_{n} x_{n} ⩽ a_{0}$ and optimizing an objective function $b_{1} y_{1} + \dots + b_{m} x_{m}$ where the coefficients $a_{i}$ , $b_{j}$ are integers (see [7] for all background and references).

The new IntSat technique for ILP [6] goes another step beyond, introducing a CDCL technique for full ILP (arbitrary integer variables, linear constraints and objective). As reported in [6], IntSat appears to be the first ILP method that is competitive with state-of-the-art commercial tools such as CPLEX and Gurobi (which solve ILP by combining LP relaxations, simplex, branch-and-cut and many other methods, see [4]). This is the case already for the first IntSat prototype implementations (single-core, unlike its competitors), performing especially well on problems having a more combinatorial (as opposed to numerical) nature.

Table 1
From CDCL to IntSat

SAT IntSat

Clause Linear constraint

$l_{1} \lor \dots \lor l_{n}$ $a_{1} x_{1} + \dots + a_{n} x_{n} ⩽ a_{0}$

0–1 variable x Integer variable x

Positive literal x Lower bound $a ⩽ x$

Negative literal $\overline{x}$ Upper bound $x ⩽ a$

Propagation Bound propagation

Resolution inference Cut inference

SAT	IntSat
Clause	Linear constraint
$l_{1} \lor \dots \lor l_{n}$	$a_{1} x_{1} + \dots + a_{n} x_{n} ⩽ a_{0}$
0–1 variable x	Integer variable x
Positive literal x	Lower bound $a ⩽ x$
Negative literal $\overline{x}$	Upper bound $x ⩽ a$
Propagation	Bound propagation
Resolution inference	Cut inference

As very roughly expressed in Table 1, IntSat extends CDCL by taking decisions on bounds (instead of literals), exhaustive bound propagation, and at each conflict it attempts to obtain by cuts a new ILP constraint, use it to backjump, and to learn it to preclude similar future conflicts (see [6] for all details).

IntSat was the motivation for the work reported in this article, but it can also be useful for other applications. In IntSat, conflict analysis may terminate with a new constraint that is not strong enough to justify a backjump. In those cases, the backjump is done based on the so-called conflicting set of bounds, thus ensuring termination and completeness of the procedure. However, the newly asserted bound is not justified by a constraint, which may weaken the learning procedure. According to our experiments, for many conflicts where no suitable cuts exist, the techniques given here allow IntSat to translate the conflicting set of bounds into the required new ILP constraint, thus improving its performance (see the short section on experiments, Section 4).

The applications of this article go beyond IntSat: indeed efficiently expressing logical constraints is of course ubiquitous in ILP (see, e.g., [3, Section 7.3]).

In what follows, X is a set of integer variables ${x_{1}, \dots, x_{n}}$ , upper and lower bounded by $B \equiv {l_{1} ⩽ x_{1} ⩽ u_{1}, \dots, l_{n} ⩽ x_{n} ⩽ u_{n}}$ . Lower case letters (possibly subscripted) x, y, z denote variables of X, and a, b, c, k, l, u denote integers. An integer linear constraint is an expression of the form $a_{1} y_{1} + \dots + a_{m} y_{m} ⩽ k$ . We consider the following basic problem. Given a disjunction D of bounds: $\begin{array}{l} y_{1} & ⩽ c_{1} \lor \dots \lor y_{p} ⩽ c_{p} \lor c_{p + 1} \\ ⩽ y_{p + 1} \lor \dots \lor c_{p + q} ⩽ y_{p + q}, \end{array}$ characterize the cases in which a single ILP constraint C exists such that $B \cup {D}$ has the same solutions in $Z$ as $B \cup {C}$ . We stress the fact that such a C is not only a valid constraint in the sense of disjunctive programming [1,2,5], that is, entailed by $B \cup {D}$ in $Z$ . Given the bounds B, the constraint C is also required to entail the disjunction D. In other words, in $Z$ and under B, the constraint C and the disjunction D should be equivalent.

By default we assume that variables ${y_{1}, \dots, y_{p + q}}$ in D are pairwise distinct. (We will discuss the case of more than one bound for the same variable in D after the proof of Lemma 2.2.) Without loss of generality we will assume that $l_{i} < c$ for every $c ⩽ x_{i}$ in D, and $c < u_{i}$ for every $x_{i} ⩽ c$ in D (note that otherwise all solutions of B are solutions of D, and $C \equiv 0 ⩽ 1$ solves the problem). Similarly, we will assume that there are no bounds in D that contradict B, that is, no $c ⩽ x_{i}$ with $c > u_{i}$ , nor $x_{i} ⩽ c$ with $c < l_{i}$ , since then D can be simplified by removing such a bound.

We say that an upper bound $x_{i} ⩽ c$ in D is improving by k if $u_{i} = c + k$ , and similarly a lower bound $c ⩽ x_{i}$ is improving by k if $l_{i} = c - k$ .

This short article is structured as follows. The main result Theorem 2.3 proves that C exists if at most one of the bounds in D is improving by more than 1; if so, a linear algorithm for computing C is given. Lemma 2.2 proves that if at least two bounds in D improve by more than 1, then not even a set S of ILP constraints exists such that $B \cup {D}$ has the same solutions in $Z$ as $B \cup S$ . An example is given in Section 3 and in Section 4 we report some first results. Section 5 discusses the situation where D is a disjunction of constraints. Finally, in Section 6, we conclude and discuss related and future work.

2. Theory

Let the disjunction D be as in the previous section. The following easy translation replacing any $x_{i}$ by $x_{i}^{'}$ simplifies matters: let $x_{i}^{'} = c - x_{i}$ for every $c ⩽ x_{i}$ in D, and $x_{i}^{'} = x_{i} - c$ for every $x_{i} ⩽ c$ in D (note the sign). After this translation all bounds occurring in D are of the form $x_{i}^{'} ⩽ 0$ . We prepare by some easy observations in linear algebra. See for example [8] for the basics in linear algebra and linear programming.

Let ${\vec{e}}_{1}, \dots, {\vec{e}}_{n}$ be the standard basis of $Q^{n}$ that is, ${\vec{e}}_{i} = (0, \dots, 1, \dots, 0)$ , with the only 1 on position i. Let $r_{1}, \dots, r_{n}$ be positive rationals. The hyperplane through $r_{1} {\vec{e}}_{1}, \dots, r_{n} {\vec{e}}_{n}$ has equation: $\begin{matrix} r_{1}^{- 1} x_{1} + \dots + r_{n}^{- 1} x_{n} = 1 . \end{matrix}$

Let $\vec{s} = \sum_{1 ⩽ i ⩽ n} r_{i} {\vec{e}}_{i}$ . In the sequel, the points ${\vec{s}}_{i} = \vec{s} - r_{i} {\vec{e}}_{i}$ are the extremal points in which D is satisfied; D is not satisfied in $\vec{s}$ . This can easily be verified, since ${\vec{s}}_{i} = (r_{1}, \dots, 0, \dots, r_{n})$ , with the only 0 on position i. The hyperplane through ${\vec{s}}_{1}, \dots, {\vec{s}}_{n}$ , which is parallel to the previous one, has equation $\begin{matrix} r_{1}^{- 1} x_{1} + \dots + r_{n}^{- 1} x_{n} = n - 1 . \end{matrix}$

If $r_{1} = \dots = r_{n - 1} = 1$ and $r_{n} = k$ , the latter equation becomes $\begin{matrix} k (x_{1} + \dots + x_{n - 1}) + x_{n} = (n - 1) k . \end{matrix}$

Lemma 2.1.
Let $u_{1}, \dots, u_{n}$ be positive integers. Let B be the set of bounds $\begin{matrix} B = {x_{i} ⩽ u_{i} ∣ 1 ⩽ i ⩽ n} \end{matrix}$ and D the disjunction $\begin{matrix} D \equiv x_{1} ⩽ 0 \lor \dots \lor x_{n} ⩽ 0 . \end{matrix}$ Let P be the bounded polyhedron in $Q^{n}$ defined by B and the constraint $\begin{matrix} u_{1}^{- 1} x_{1} + \dots + u_{n}^{- 1} x_{n} ⩽ n - 1 . \end{matrix}$ Then P contains an integer point not satisfying D if and only if at least two of $u_{1}, \dots, u_{n}$ are > 1 .
Proof.
By default we assume that all variables $x_{i}$ are distinct. Since P is downward closed in each variable $x_{i}$ , we have $(y_{1}, \dots, y_{n}) \in P$ if there exists a point $(x_{1}, \dots, x_{n}) \in P$ such that $0 ⩽ y_{i} ⩽ x_{i}$ . In particular, if P contains an all positive integer point, then P contains $(1, \dots, 1)$ . Now we argue as follows: $(1, \dots, 1) \in P$ iff $u_{1}^{- 1} + \dots + u_{n}^{- 1} ⩽ n - 1$ iff at least two of the integers $u_{1}, \dots, u_{n}$ are ⩾2 (as the sum has n terms). □
Lemma 2.2.
Let B and D be as in Section 1. If at least two bounds in D improve by more than 1, then there exists no set S of ILP constraints such that $B \cup {D}$ has the same solutions in $Z$ as $B \cup S$ .
Proof.
We first give the argument in the case in which D consists of two upper bounds that improve by more than 1, that is, $D \equiv x_{1} ⩽ c_{1} \lor x_{2} ⩽ c_{2}$ with $B = {l_{1} ⩽ x_{1} ⩽ u_{1}, l_{2} ⩽ x_{2} ⩽ u_{2}}$ such that $c_{1} + 2 ⩽ u_{1}$ , $c_{2} + 2 ⩽ u_{2}$ . Note that the points $(c_{1}, c_{2})$ , $(c_{1}, u_{2})$ , $(u_{1}, c_{2})$ satisfy D, but the point $(c_{1} + 1, c_{2} + 1)$ does not. All four points satisfy B, and the fourth point is in the convex hull of the first three, see Fig. 1. Since any set S of ILP constraints defines a convex subset of $Q^{2}$ , no such set S can contain $(c_{1}, c_{2})$ , $(c_{1}, u_{2})$ , $(u_{1}, c_{2})$ but not $(c_{1} + 1, c_{2} + 1)$ . It follows that $B \cup S$ has different solutions in $Z$ as $B \cup {D}$ . This argument can easily be adapted to the case where $D \equiv c_{1} ⩽ x_{1} \lor, x_{2} ⩽ c_{2}$ . If D contains other bounds as well, then either $\neg (c ⩽ x_{i})$ for $x_{i} = l_{i}$ or $\neg (x_{i} ⩽ c)$ for $x_{i} = u_{i}$ , not satisfying the bound in D. The argument above can now be carried out with these values for the variables occurring in the other bounds. □

Fig. 1.
Four points in B.

We now discuss what happens if some variable occurs more than once in D. First, in one pass over the disjunction D, by only retaining for each variable its least (since D is a disjunction) constraining upper bound and lower bound, one gets an equivalent disjunction with at most two bounds per variable. If there are two of them, one is an upper bound $x_{i} ⩽ c$ and one is a lower bound $c^{'} ⩽ x_{i}$ . If $c ⩾ c^{'} - 1$ , then the disjunction D is always true and we can take $C \equiv 0 ⩽ 1$ . Therefore we can assume $c + 1 < c^{'}$ , and a similar argument as for Lemma 2.2 applies. To see this, we first construct a point satisfying the bounds in B but not satisfying D. Put $x_{i} = c + 1$ for each $x_{i}$ such that both $x_{i} ⩽ c$ and $c^{'} ⩽ x_{i}$ in D. Put $x_{i} = u_{i}$ for each $x_{i}$ such that only $x_{i} ⩽ c$ in D. Put $x_{i} = l_{i}$ for each $x_{i}$ such that only $c ⩽ x_{i}$ in D. Assign an arbitrary value between $l_{i}$ and $u_{i}$ to $x_{i}$ for each $x_{i}$ not occurring in D. Call this point P. Now pick one specific $x_{i}$ such that both $x_{i} ⩽ c$ and $c^{'} ⩽ x_{i}$ in D. Define the point $P_{i}^{u}$ ( $P_{i}^{l}$ ) to be point P with the coordinate for $x_{i}$ changed into $c + 2$ (c). The points P, $P_{i}^{u}$ , $P_{i}^{l}$ all satisfy B; $P_{i}^{u}$ , $P_{i}^{l}$ satisfy D but P in the middle of $P_{i}^{u}$ , $P_{i}^{l}$ does not satisfy D. Since any set S of ILP constraints defines a convex subset of $Q^{n}$ , no such set S can contain $P_{i}^{u}$ , $P_{i}^{l}$ but not P. It follows that $B \cup S$ has different solutions in $Z$ as $B \cup {D}$ .

We now come to the main positive result. Define the standard sum $p_{D}$ for a disjunction D by $\begin{matrix} p_{D} \equiv \sum_{(x_{i} ⩽ c) \in D} (x_{i} - c) + \sum_{(c ⩽ x_{i}) \in D} (c - x_{i}) . \end{matrix}$ The number of variables in $p_{D}$ will be denoted by $# (p_{D})$ .
Theorem 2.3.
Let B and D be as in Section 1. Assume at most one bound in D is improving by more than 1. Then $B \cup {D}$ has the same solutions in $Z$ as $B \cup {C}$ , where the constraint C is defined as follows. If D is $x_{i} ⩽ c \lor D_{i}$ , where no bound in $D_{i}$ is improving by more than 1, then $\begin{matrix} C \equiv x_{i} - c + (u_{i} - c) p_{D_{i}} ⩽ # (p) (u_{i} - c) . \end{matrix}$ If D is $c ⩽ x_{i} \lor D_{i}$ , where no bound in $D_{i}$ is improving by more than 1, then $\begin{matrix} C \equiv c - x_{i} + (c - l_{i}) p_{D_{i}} ⩽ # (p) (c - l_{i}) . \end{matrix}$ In both cases $p_{D_{i}}$ is the standard sum for $D_{i}$ .
Proof.
Let conditions be as above. We first normalize the problem in order to match the format of Lemma 2.1. Define new variables: $x_{i}^{'} = x_{i} - c$ if $x_{i} ⩽ c$ in D and $x_{i}^{'} = c - x_{i}$ if $c ⩽ x_{i}$ in D. Normalize D with the new variables into $D^{'} \equiv ⋁ (x_{i}^{'} ⩽ 0)$ for all $(x_{i} ⩽ c) \in D$ or $(c ⩽ x_{i}) \in D$ . Normalize upper bounds $u_{1}^{'}, \dots, u_{n + m}^{'}$ for the new variables: $x_{i}^{'} ⩽ u_{i}^{'} = u_{i} - c$ if $x_{i} ⩽ c$ in D and (note the sign) $x_{i}^{'} ⩽ u_{i}^{'} = c - l_{i}$ if $c ⩽ x_{i}$ in D. If $D^{'}$ is $x_{i}^{'} ⩽ 0 \lor D_{i}^{'}$ , where no bound in $D_{i}^{'}$ is improving by more than 1, then Lemma 2.1 gives the constraint $C^{'} \equiv {(u_{i}^{'})}^{- 1} x_{i}^{'} + p_{D_{i}^{'}} ⩽ n + m - 1$ . Here $p_{D_{i}^{'}}$ is the sum of terms $x_{j}^{'}$ for all $j \neq i$ such that $x_{j}$ occurs in D. Note that $# (p_{D}) = # (p_{D_{i}^{'}}) = n + m - 1$ . Moreover, substituting back in $p_{D_{i}^{'}}$ yields $p_{D}$ . Finally, multiplying by $u_{i}^{'}$ and substituting back $x_{i}^{'} = x_{i} - c$ yields the desired constraint in the lemma. The other case is similar. □
3. An example

We illustrate Theorem 2.3 and its proof by an easy example. Consider the following disjunction of bounds $\begin{matrix} D \equiv 1 ⩽ x_{1} \lor x_{2} ⩽ - 2 \lor x_{3} ⩽ 1, \end{matrix}$ where the original bounds are $\begin{matrix} \begin{matrix} B = & {0 ⩽ x_{1} ⩽ 10, - 10 ⩽ x_{2} ⩽ - 1, \\ 0 ⩽ x_{3} ⩽ 8} . \end{matrix} \end{matrix}$ We want to find a constraint that is logically equivalent to D given B.

Normalize the problem:

new variables: $x_{1}^{'} = - x_{1} + 1$ , $x_{2}^{'} = x_{2} + 2$ , $x_{3}^{'} = x_{3} - 1$ ;

new bounds: $- x_{1}^{'} ⩽ 1$ , $x_{2}^{'} ⩽ 1$ , $x_{3}^{'} ⩽ 7$ ;

new disjunction: $x_{1}^{'} ⩽ 0 \lor x_{2}^{'} ⩽ 0 \lor x_{3}^{'} ⩽ 0$ .

Get the constraint, as in the proof of Theorem 2.3: $\begin{matrix} - 7 x_{1}^{'} + 7 x_{2}^{'} + x_{3}^{'} ⩽ 14 . \end{matrix}$

Express the constraint with the original variables: $\begin{matrix} - 7 x_{1} + 7 x_{2} + x_{3} ⩽ - 6 . \end{matrix}$

For example, if

x_{1} = 0

and

x_{2} = - 1

(values within the bounds, but not satisfying D), the constraint enforces

x_{3} ⩽ 1

(satisfying D). Conversely, if D is satisfied by values in B, the constraint is also satisfied.

4. Experiments

The techniques described here increase the number of early backjump cuts (see [6]) and hence at each conflict where this happens, a strictly stronger constraint is learned. The constraints learned at other conflicts are not affected. Therefore, one can expect an improvement of the learning and hence of the performance of IntSat. Here we briefly report on some first experimental results on the extent of this improvement for the IntSat ILP solver.

We took the 49 xx.lp optimization problems of Section 5 of [6], and ran our IntSat solver on each one of them with ten different random seeds (to make results statistically more significant). Each random seed was ran with a 60 s timeout, each one without and with the techniques given here, a total of 2 × 490 experiments. Percentages of early backjump cuts (see [6]) typically go up from around 3% (without) to 15% (with). The average (among the 10 seeds) best solution cost found improved in six out of 49 problems and got worse in one, but more importantly, the number of problems (out of 49) for which an optimal solution was found and optimality was proved for all 10 random seeds goes up from 31 problems (without) to 40 (with).

5. When D is a disjunction of constraints

We now discuss the case where D is not simply a disjunction of bounds, but a disjunction of constraints of the form: $\begin{array}{l} r_{1} & ⩽ c_{1} \lor \dots \lor r_{p} ⩽ c_{p} \lor c_{p + 1} \\ ⩽ r_{p + 1} \lor \dots \lor c_{p + q} ⩽ r_{p + q}, \end{array}$ where the $r_{j}$ are sums of monomials $a_{i} x_{i}$ over X. Then for each (distinct) such $r_{j}$ one can infer lower and upper bounds from the lower and upper bounds B on X. Hence, by introducing a new variable $z_{j}$ for each $r_{j}$ , one gets the corresponding bounds $B^{'}$ on $Z \equiv {z_{1}, \dots, z_{p + q}}$ , and one can replace D by the disjunction $D^{'}$ over Z: $\begin{array}{l} z_{1} & ⩽ c_{1} \lor \dots \lor z_{p} ⩽ c_{p} \lor c_{p + 1} \\ ⩽ z_{p + 1} \lor \dots \lor c_{p + q} ⩽ z_{p + q} . \end{array}$

If the resulting problem consisting of $B^{'}$ and $D^{'}$ over Z fulfils the conditions of Theorem 2.3, this theorem shows us how to efficiently obtain a linear constraint $C^{'}$ over Z such that $B^{'} \cup {C^{'}}$ has the same solutions in $Z$ as $B^{'} \cup {D^{'}}$ . It is not hard to check that, by replacing back in $C^{'}$ each $z_{j}$ by its corresponding $r_{j}$ , one gets a constraint C over X such that $B \cup {C}$ has the same solutions in $Z$ as $B \cup {D}$ : any solution $sol : X \to Z$ of $B \cup {D}$ can be extended into a solution of $B^{'} \cup {D^{'}}$ (by taking $sol (z_{j}) = sol (r_{j})$ ), which gives us a solution of $B^{'} \cup {C^{'}}$ , which in turn gives us a solution of $B \cup {C}$ , and the same steps can also be done reversely.

For example, let B be ${0 ⩽ x ⩽ 2, 0 ⩽ y ⩽ 2, 0 ⩽ u ⩽ 2}$ , and let D be $x + y ⩽ 2 \lor u - y ⩽ 1$ . Then after substitution, we get $B^{'} \equiv {0 ⩽ z_{1} ⩽ 4, 0 ⩽ z_{2} ⩽ 2}$ and $D^{'} \equiv z_{1} ⩽ 2 \lor z_{2} ⩽ 1$ , which fulfils the conditions of Theorem 2.3 since $z_{2} ⩽ 1$ is improving by 1. The resulting $C^{'}$ is $z_{1} + 2 z_{2} ⩽ 6$ , and translating back, we get that C is $x - y + 2 u ⩽ 6$ .

6. Conclusions and related work

Disjunctions (and other logical constraints) are usually expressed with the help of conjunctions of several constraints and new 0–1 variables. For example, the disjunction $D \equiv x_{1} ⩽ 0 \lor x_{2} ⩽ 0$ , in the presence of bounds $x_{1}, x_{2} ⩽ 2$ , both improved by 2 in D, can be encoded by the following constraints ( $x_{3}$ is a new 0–1 variable): $\begin{matrix} \begin{matrix} x_{1} + 2 x_{3} ⩽ 2, x_{2} - 2 x_{3} ⩽ 0, \\ 0 ⩽ x_{3} ⩽ 1 . \end{matrix} \end{matrix}$ However, such encodings do not give equivalence, but only equisatisfiability. For example, $(0, 2, 0)$ satisfies D but not $x_{2} - 2 x_{3} ⩽ 0$ . Note that our method works with a single new constraint and without the need of auxiliary variables, and both requirements are necessary for our application in IntSat.

We also remark that it is well known that in many ILP problems a large percentage of variables are 0–1. Since no bound over a 0–1 variable is improving by more than one, it is not surprising that our method applies quite frequently in practice.

Finally, we also remark that, for each $x_{i}$ that is upper bounded in D, our result only requires the existence of an upper bound in B, and not a lower bound. Similarly, a lower bound of $x_{i}$ in D requires a lower bound for $x_{i}$ in B, and no upper bound. This makes the method slightly more general.

Footnotes

Acknowledgements

Asín’s research was funded by CONICYT, Chile, under FONDECYT project 11121220. Nieuwenhuis’ and Bezem’s research was supported by the Spanish grants TIN2013-45732-C4-3-P (MINECO) and TIN2010-21062-C02-01 (MEC/MICINN).

References

[1]

Balas, Disjunctive programming, Annals of Discrete Mathematics 5 (1979), 3–51.

[2]

Balas

et al., Disjunctive programming: Cutting planes from logical conditions, in: Nonlinear Programming, Vol. 2, 1975, pp. 279–312.

[3]

Bisschop, AIMMS optimization modeling, 2006, available at: http://www.aimms.com/downloads/manuals/optimization-modeling/.

[4]

F.S.

Hillier and

G.J.

Lieberman, Introduction to Operations Research, 9th edn, McGraw-Hill, 2010.

[5]

J.N.

Hooker and

M.A.

Osorio, Mixed logical-linear programming, Discrete Applied Mathematics 96 (1999), 395–442.

[6]

Nieuwenhuis, The IntSat method for integer linear programming, in: Principles and Practice of Constraint Programming, 20th International Conference, CP 2014, LNCS, Vol. 8656, 2014, pp. 574–589.

[7]

Roussel and

V.M.

Manquinho, Pseudo-Boolean and cardinality constraints, in: Handbook of Satisfiability,

Biere,

Heule,

van Maaren and

Walsh, eds, Frontiers in Artificial Intelligence and Applications, Vol. 185, IOS Press, 2009, pp. 695–733.

[8]

Schrijver, Theory of Linear and Integer Programming, Wiley, 1998.