Takustraße 7 D-14195 Berlin-Dahlem Germany
Konrad-Zuse-Zentrum
f ¨ur Informationstechnik Berlin
T
OBIASA
CHTERBERGConflict Analysis in Mixed Integer Programming
URL:http://www.zib.de/projects/integer-optimization/MIP
Conflict Analysis in Mixed Integer Programming
Tobias Achterberg
∗August 3, 2005
Abstract
Conflict analysis for infeasible subproblems is one of the key ingredients in modern SAT solvers to cope with large real-world instances. In contrast, it is common practice for today’s mixed integer programming solvers to just discard infeasible subproblems and the information they reveal. In this paper we try to remedy this situation by generalizing SAT infeasibility analysis to mixed integer programming.
We present heuristics for branch-and-cut solvers to generate valid inequal- ities from the current infeasible subproblem and the associated branching in- formation. SAT techniques can then be used to strengthen the resulting cuts.
We performed computational experiments which show the potential of our method: On feasible MIP instances, the number of required branching nodes was reduced by 50% in the geometric mean. However, the total solving time increased by 15%. On infeasible MIPs arising in the context of chip verifica- tion, the number of nodes was reduced by 90%, thereby reducing the solving time by 60%.
Keywords: mixed integer programming, branch-and-cut, conflict analysis, SAT, infeasible MIP
1 Introduction
A well-known approach to solve mixed integer programs (MIPs) is to apply branch- and-bound type algorithms: the given problem instance is divided into smaller sub- problems, and this decomposition is continued recursively until an optimal solution of the respective subproblem can be identified or the subproblem is detected to be infeasible or to exceed the primal bound. It seems that current state-of-the-art MIP solvers like CPlex [13], Lindo [14], SIP [16], or XPress [9], simply discard infea- sible and bound exceeding subproblems without paying further attention to them.
For solving the satisfiability problem (SAT), a similar branching scheme to de- compose the problem into smaller subproblems is applied, which was proposed by Davis, Putnam, Longemann, and Loveland [10, 11]. Modern SAT solvers, how- ever, try to learn from infeasible subproblems, an idea due to Marques-Silva and Sakallah [15]. The infeasibilities are analyzed in order to generate so-called conflict clauses. These are implied clauses that help to prune the search tree.
The idea of conflict analysis is to identify a reason of the current subproblem’s infeasibility and exploit this knowledge. In SAT solving, such a reason is a subset of the current variable fixings which already suffices to trigger a chain of logical deductions that ends in a contradiction. That means, the fixing of the variables of
∗Konrad-Zuse-Zentrum f¨ur Informationstechnik Berlin, achterberg@zib.de
this conflict set renders the problem instance infeasible. The conflict clause that can be learned from this conflict states that at least one of the variables in the conflict set has to take the opposite truth value. This clause is added to the clause database and can then be used at other subproblems to find additional implications, thereby pruning the search tree.
In this paper, we propose a generalization of conflict analysis to branch-and- bound based mixed integer programming. We consider a mixed integer program of the form
(MIP) max{cTx| Ax ≤ b, l ≤ x ≤ u, xj ∈ Z for all j ∈ I}
with A ∈ Rm×n, b ∈ Rm, c, l, u ∈ Rn, and I ⊆ N = {1, . . . , n}. Suppose a subproblem in the branch-and-bound search tree is detected to be infeasible or to exceed the primal bound. We will show that this situation can be analyzed with similar techniques as in SAT solving: a conflict graph is constructed from which conflict constraints can be extracted. These constraints can be used as cutting planes to strengthen the relaxations of other subproblems in the tree.
Note that the term “conflict graph” is used differently in the SAT and MIP communities. In MIP solving, the conflict graph consists of implications between two binary variables each, see e.g., Atamt¨urk, Nemhauser, and Savelsbergh [5]. It represents a vertex packing relaxation of the MIP instance and can, e.g., be used to derive cutting planes like clique cuts. In SAT solving, however, the conflict graph arises from the implication graph which is a hyper-graph containing all implications between any number of variables. For each infeasible subproblem, a specific con- flict graph is constructed to represent the implications from which the infeasibility follows. In this paper we adopt the nomenclature of the SAT community.
There are two main differences of MIP and SAT solving in the context of conflict analysis. First, the variables of a MIP need not to be of binary type. We also have to deal with general integer and continuous variables. Furthermore, the infeasibility of a subproblem in the MIP search tree usually has its sources in the linear pro- gramming (LP) relaxation of the subproblem. In this case, we first have to find a (preferably simple) reason for the LP’s infeasibility before we can apply the SAT conflict analysis techniques for generating conflict constraints.
The rest of the paper is organized as follows. Section 2 reviews conflict graph analysis of SAT solvers. For an infeasible subproblem, it is shown how to generate the conflict graph and how to extract valid conflict clauses out of this graph. Section 3 deals with the generalization of these techniques to mixed integer programming. We explain how infeasible and bound exceeding linear programs can be analyzed in order to detect a conflict in the variables’ local bounds. This conflict is used as starting point to construct the conflict graph from which conflict constraints can be extracted with the techniques explained in Section 2. Additionally, we discuss how we have to generalize the notion of the conflict graph in the presence of non-binary variables.
Experimental results in Section 4 demonstrate that conflict analysis can lead to substantial savings in the number of branching nodes to solve a MIP. However, time measurements indicate that further enhancements to the given algorithms are needed in order to produce an overall speed-up on the investigated feasible instances.
For infeasible MIPs, conflict analysis can yield major performance improvements in both, the number of branching nodes and the time needed to prove the infeasibility.
2 Conflict Analysis in SAT Solving
In this section we review the conflict analysis techniques used in SAT solving, see e.g., Marques-Silva and Sakallah [15] or Zhang et al. [23]. The Boolean satisfiability problem (SAT) is defined as follows. The Boolean truth values false and true are identified with the values 0 and 1, respectively, and Boolean formulas are evaluated correspondingly.
Definition 2.1 (SAT) Let C = C1∧ . . . ∧ Cm be a logic formula in conjunctive normal form (CNF) on Boolean variables x1, . . . , xn. Each clause Ci= ℓi1∨ . . . ∨ ℓiki is a disjunction of literals. A literal ℓ ∈ L = {x1, . . . , xn,x¯1, . . . ,x¯n} is either a variable xj or the negation of a variable ¯xj. The task is to either find an assignment x⋆ ∈ {0, 1}n, such that the formula C is satisfied, i.e., each clause Ci evaluates to 1, or to conclude that C is unsatisfiable, i.e., for all x ∈ {0, 1}n at least one Ci
evaluates to 0.
SAT was the first problem shown to be N P-complete by Cook [8]. Besides its theoretical relevance, it has many practical applications, e.g., in the design and verification of integrated circuits or in the design of logic-based intelligent systems.
We refer to Biere and Kunz [6] for an overview of SAT techniques in chip verification and to Truemper [21] for details on logic-based intelligent systems.
Modern SAT solvers like Chaff [18] or BerkMin [12] rely on the following techniques:
• using a branching scheme (the DPLL-algorithm of Davis, Putnam, Longemann, and Loveland [10, 11]) to split the problem into smaller subproblems,
• applying Boolean Constraint Propagation (BCP) [22] on the subproblems, which is a simple node preprocessing, and
• analyzing infeasible subproblems to produce conflict clauses [15], which help to prune the search tree later on.
The DPLL-algorithm creates two subproblems at each node of the search tree by fixing a single variable to zero and one, respectively. The nodes are processed in a depth first fashion. At each node, BCP is applied to derive further deductions by substituting the fixed variables in the clauses. It may happen that a still unsatisfied clause is thereby reduced to a single literal, a so-called unit clause. In this case, the remaining literal can be fixed to 1. BCP is applied iteratively until no more deductions can be found or a clause gets empty, i.e., all its literals are fixed to 0.
The latter case is called a conflict, and conflict analysis can be performed to produce a conflict clause, which is explained in the following.
2.1 Conflict Graph Analysis
The deductions performed in BCP can be visualized in a conflict graph G = (V, A).
The vertices V = {ℓ1, . . . , ℓk, λ} ⊂ L ∪ {λ} of this directed graph represent the current value assignments of the variables, with the special vertex λ representing the conflict. The arcs can be partitioned into A = A1∪ . . . AD∪ Aλ. Each subset Ad, d = 1, . . . , D, represents one deduction: whenever a clause Ci= ℓi1∨ . . . ∨ ℓiki∨ ℓir became a unit clause in BCP with remaining unfixed literal ℓir, a set of arcs Ad = {(¯ℓi1, ℓir), . . . , (¯ℓiki, ℓir)} is created in order to represent the deduction ¯ℓi1∧ . . . ∧ ¯ℓiki → ℓir that is implied by Ci. The additional set of arcs Aλ = {(¯ℓλ1, λ), . . . , (¯ℓλkλ, λ)}
¯ x1
x2
¯ x3
x4
¯ x5
¯ x6
¯ x7
x8
x9
x10
x11
¯ x12
x13
x14
x15
¯ x16
x17
x18
λ A
B C D
depth 1 depth 2 depth 3 depth 4 depth 5
Figure 1. Conflict graph of Example 2.2. The vertices in the top row are branching decisions, the ones below are deductions. Each cut separating the branching vertices and the conflict vertex (λ) yields a conflict clause.
represents clause Cλ that detected the conflict (i.e., the clause that got empty in BCP).
Example 2.2 Consider the CNF C = C1∧ . . . ∧ C18 with the following clauses:
C1: x1∨ x2 C7: ¯x10∨ x11 C13: x16∨ x18
C2: ¯x2∨ ¯x3 C8: ¯x8∨ x12∨ x13 C14: ¯x17∨ ¯x18
C3: ¯x2∨ ¯x4∨ ¯x5 C9: x12∨ x14 C15: ¯x12∨ x19
C4: x6∨ ¯x7 C10: ¯x8∨ ¯x13∨ ¯x14∨ x15 C16: x7∨ ¯x19∨ x20
C5: x3∨ x5∨ x7∨ x8 C11: ¯x8∨ ¯x9∨ ¯x15∨ ¯x16 C17: x15∨ ¯x20∨ x21
C6: x3∨ ¯x8∨ x9 C12: ¯x15∨ x17 C18: ¯x8∨ ¯x20∨ ¯x21
Suppose the fixings x1 = 0, x4 = 1, x6 = 0, x10 = 1, and x12 = 0 were applied in the branching steps of the DPLL procedure. This leads to a conflict generated by constraint C14. The corresponding conflict graph is shown in Figure 1.
In the conflict graph, we distinguish between branching vertices VB and deduced vertices V \ VB. Branching vertices are those without incoming arcs. Each cut separating the branching vertices VB from the conflict vertex λ gives rise to one distinct conflict clause (see Figure 1), which is obtained as follows.
Let V = Vr∪ Vc, Vr∩ Vc = ∅, be a partition of the vertices arising from a cut with VB ⊆ Vr and λ ∈ Vc. Vr is called reason side, and Vc is called conflict side.
The reason side’s frontier Vf := {ℓp∈ Vr| ∃(ℓp, ℓq) ∈ A, ℓq∈ Vc} is called conflict set. Fixing the literals in Vf to 1 suffices to produce the conflict. Therefore, the conflict clause Cf =W
ℓj∈Vf
ℓ¯j is valid for all feasible solutions of the SAT instance at hand.
Figure 1 shows different types of cuts (labeled ’A’ to ’D’), leading to different conflict clauses. The cut labeled ’A’ produces clause CA= x1∨ ¯x4∨ x6∨ ¯x10∨ x12
consisting of all branching variables. This clause would not help to prune the search tree, because the current subproblem is the only one where all branching variables are fixed to these specific values. The clause would never be violated again. Cut ’D’
is not useful either, because clause CD= ¯x17∨ ¯x18 is equal to the conflict detecting clause Cλ = C14 and already present in the clause database. Therefore, useful cuts must be located somewhere “in between”.
There are several methods for generating useful cuts. Two of them are the so- called All-FUIP and 1-FUIP schemes which proved to be successful for SAT solving.
These are explained in the following. We refer to [23] for a more detailed discussion.
Each vertex in the conflict graph represents a fixing of a variable that was applied in one of the nodes on the path from the root node to the current node in the search tree. The depth level of a vertex is the depth of the node in the search tree at which the variable was fixed. In each depth level, the first fixing corresponds to a branching vertex while all subsequent fixings are deductions. In the example shown in Figure 1, there are 5 depth levels (excluding the root node) which are defined by the successive branching vertices ¯x1, x4, ¯x6, x10, and ¯x12.
Definition 2.3 (unique implication point) An unique implication point (UIP) of depth level d is a vertex ℓdu ∈ V representing a fixing in depth level d, such that every path from the branching vertex of depth level d to the conflict vertex λ goes through ℓdu or through a UIP ℓdu′′ of higher depth level d′ > d. The first unique implication point (FUIP) of a depth level d is the UIP ℓdu 6= λ that was fixed last, i.e., that is closest to the conflict vertex λ.
Note that the UIPs of the different depth levels are defined recursively, starting at the last depth level, i.e., the level of the conflict. UIPs can be identified in linear time by a single scan through the conflict graph. In the example, the FUIPs of the individual depth levels are x15, x11, x8, ¯x5, and ¯x3, respectively.
The 1-FUIP scheme finds the first UIP in the last depth level. All literals that were fixed after this FUIP are put to the conflict side. The remaining literals and the FUIP are put to the reason side. In the example shown in Figure 1, the FUIP of the last depth level is x15. The 1-FUIP cut is the one labeled ’C’. It corresponds to the clause CC= ¯x8∨ ¯x9∨ ¯x15.
The All-FUIP scheme finds the first UIP of every single depth level. From each depth level, the literals fixed after their corresponding FUIP are put to the conflict side. The remaining literals and the FUIPs are put to the reason side. In the example, this results in cut ’B’ which corresponds to the clause CB = x3∨ ¯x8∨ ¯x15.
2.2 Reconvergence Cuts
In the previous section it was shown that each cut separating the branching vertices from the conflict vertex gives rise to a conflict clause, which contains the literals of the reason side’s frontier. By dropping the requirement that the cut must separate the conflict vertex from the branching vertices, we get a different class of cuts which are called cuts not involving conflicts (see [23]). These cuts can also be used to derive valid clauses from the conflict graph. In order to apply non-chronological backtracking, which is explained in Section 2.3, one has to generate some of these cuts, in particular the UIP reconvergence cuts of the last depth level (see below).
Figure 2 gives an example of a cut not involving conflicts. In conflict graph analysis, the conflict vertex λ is substituted by an arbitrary vertex ℓu representing a literal. In the example, ℓu= x15was chosen, which is the first unique implication point of the last depth level.
Each cut separating the branching vertices VBfrom the vertex ℓuby partitioning the vertices V into Vr⊇ VBand Vc ∋ ℓugives rise to the clause Cu= (W
ℓi∈Vf
ℓ¯i)∨ℓu.
¯ x1
x2
¯ x3
x4
¯ x5
¯ x6
¯ x7
x8
x9
x10
x11
¯ x12
x13
x14
x15
¯ x16
x17
x18
λ
Figure 2. The cut separating the branching vertices (top row) and a deduced vertex (x15) yields the reconvergence clause ¯x8∨ x12∨ x15.
Again, Vf consists of the vertices at the reason side’s frontier of the cut. However, such a clause is only useful if Vc∪ Vf contains an ℓu-reconvergence, i.e., two different paths from a vertex ℓi ∈ Vc∪ Vf to ℓu. Otherwise, it can be proved that all possi- ble deductions of Cu can already be found by iterated BCP on the current clause database.
The cut shown in Figure 2 is a UIP reconvergence cut which connects the two successive UIP ’s ¯x12and x15of depth level 5: by applying all fixings of lower depth levels, Cu = ¯x8∨ x12∨ x15 reduces to the implication ¯x12 → x15. Note that BCP can now also deduce ¯x15→ x12, which is not possible without using Cu.
2.3 Non-chronological Backtracking
Suppose the conflict analysis procedure produced a clause with only one literal ℓdu fixed at depth level d in which the conflict was detected. All other literals were fixed at depth levels smaller or equal to d′ < d. If this clause would have been known earlier, the literal ℓdu could already have been fixed to the opposite value in depth d′. Suppose the conflict analysis procedure also produced all reconvergence clauses necessary to connect ℓdu to the branching vertex ℓdb of depth d. Then, also the branching variable of depth d could have been fixed to the opposite value in depth d′.
Therefore, after having found such a conflict clause, the search tree’s node in depth level d′ can be reevaluated to apply the deductions leading to the opposite fixing of ℓdb. Further deductions may lead to another conflict, thus rendering the whole subtree rooted in depth d′ infeasible without evaluating its remaining leaves.
In [15] it was empirically shown, that this so-called non-chronological backtracking can lead to large reductions in the number of evaluated nodes to solve SAT instances.
In our Example 2.2, the conflict analysis engine used in this paper produces the conflict clauses CB = x3∨ ¯x8 ∨ ¯x15 and CC = ¯x8∨ ¯x9∨ ¯x15. Additionally, the reconvergence clause CR = ¯x8∨ x12∨ x15 is added to the clause database.
Evaluating the node in depth 3 again, x15 = 0 (using CC) and x12 = 1 (using CR) can be deduced, leading together with C15, . . . , C18 to another conflict (see Figure 3). Therefore, the subtree with x1 = 0, x4 = 1, and x6 = 0 can be pruned
¯ x1
x2
¯ x3
x4
¯ x5
¯ x6
¯ x7
x8
x9
x12
¯ x15
x19
x20
x21
λ
Figure 3. Reevaluation of the node in depth 3 after inserting conflict and reconvergence clauses again leads to a conflict.
without evaluating the intermediate branching decisions (in this case x10 = 0 and x10= 1).
3 Conflict Analysis in MIP
In this section we describe the generalization of conflict analysis of Section 2 to mixed integer programming. Recall that we consider a mixed integer program of the form
(MIP) max{cTx| Ax ≤ b, l ≤ x ≤ u, xj∈ Z for all j ∈ I}
with A ∈ Rm×n, b ∈ Rm, c, l, u ∈ Rn, and I ⊆ N = {1, . . . , n}. A branch-and-bound based MIP solver decomposes the problem instance into subproblems typically by modifying the bounds l and u of the variables. These branching decisions may entail further deductions on the bounds of other variables. The deductions can be gener- ated by bound strengthening rules on linear constraints (see, e.g., Savelsbergh [20]).
Suppose we detected a subproblem in the branch-and-bound search tree to be infeasible, either because a deduction leads to a variable with empty domain or because the LP relaxation is infeasible. To analyze this conflict, we proceed in the same fashion as in SAT solving: we construct a conflict graph, choose a cut in this graph, and produce a conflict constraint which consists of the variables in the conflict set, i.e., in the cut’s frontier. Because a MIP may contain non-binary variables, we have to extend the concept of the conflict graph: it has to represent bound changes instead of fixings of variables. This generalization is described in Section 3.1.
A conflict in SAT solving is always detected due to a single clause that became empty during the binary constraint propagation process (see Section 2). This con- flict detecting clause provides the links from the vertices in the conflict graph that represent fixings of variables to the conflict vertex λ. In contrast, in an LP based branch-and-bound algorithm to solve mixed integer programs, infeasibility of a sub- problem is almost always detected due to the infeasibility or bound exceedance of its LP relaxation. In this case the LP relaxation as a whole is responsible for the infeasibility. There is no single conflict detecting constraint that defines the pre- decessors of the conflict vertex in the conflict graph. To cope with this situation,
we have to analyze the LP in order to identify a subset of the bound changes that suffices to render the LP infeasible or bound exceeding. The conflict vertex can then be connected to the vertices of this subset. Section 3.2 explains how to analyze infeasible LPs and how to identify an appropriate subset of the bound changes. The case of bound exceedance is treated in Section 3.3.
After the conflict graph has been constructed, we have to choose a cut in the graph in order to define the conflict set and the resulting conflict constraint. In the case of a binary program, i.e., I = N , l = 0, u = 1, the conflict graph can be analyzed by the same algorithms as described in Section 2 to produce a conflict clause Cf =W
ℓj∈Vf
ℓ¯j. This clause can be linearized by the set covering constraint X
j:xj∈Vf
(1 − xj) + X
j:¯xj∈Vf
xj≥ 1, (1)
and added to the MIP’s constraint set. However, in the presence of non-binary variables, the analysis of the conflict graph may produce a conflict set that contains bound changes on non-binary variables. In this case the conflict constraint can not be linearized by the set covering constraint (1). Section 3.4 shows how non-binary variables can be incorporated into the conflict constraints.
3.1 Generalized Conflict Graph
If general integer or continuous variables are present in the problem, a bound on a specific variable could have been changed more than once on the path from the root node to the current subproblem. A local bound change on a non-binary variable can be both reason and consequence of a deduction, similar to a fixing of a binary variable. Therefore, we generalize the concept of the conflict graph: the vertices now represent bound changes instead of fixings. Note that there can now exist multiple vertices corresponding to the same non-binary variable in the conflict graph, each vertex representing one change of the variable’s bounds.
Example 3.1 Consider the following constraints of an integer program with vari- ables x1, . . . , x7∈ {0, 1} and z1, . . . , z5∈ Z≥0.
2x1 + 3z1+ 2z2 ≤ 9 (2)
+ 9x2 − z1− 2z2 ≤ 0 (3)
− 3x2+ 5x3− 3x4 ≤ 4 (4)
− 3x2 + 9x4 − 2z3 ≤ 6 (5)
+ 9x5 − z2+ 2z3 ≤ 8 (6)
− 4x6− 7x7 + 2z3 ≤ 3 (7)
+ 5x7 − 2z2 ≤ 2 (8)
− x5 + 5x7 + 4z2− 5z3 ≤ 2 (9)
x1− x2+ x3 − 2x5+ x6 − z1− 2z2+ z3− 2z4+ 4z5≤ 1 (10) + 2x2 − x4+ 3x5− 2x6 − z1+ 5z2+ z3+ 2z4− 6z5≤ 2 (11)
−2x1 − 2x3+ x4+ x5 + z1+ 2z2− 2z3+ 2z4− 2z5≤ 1 (12) By the basic bound strengthening techniques of Savelsbergh [20], we can deduce upper bounds z1 ≤ 3, z2 ≤ 4, z3 ≤ 6, z4≤ 23, and z5 ≤ 15 on the general integer variables. Assume we branched on x1 = 1. By applying bound strengthening on
x1= 1
x2= 0 x3= 1
x4= 1
x5= 0
x6= 0
x7= 1 z1≤2
z2≤3
z3≤5
z3≥2
z2≥2
z3≥3
z1≤1
λ LP
Figure 4. Conflict graph of Example 3.1. After applying the branching decisions x1= 1, x3= 1, x6= 0, and all inferred bound changes, the LP relaxation becomes infeasible. The implications on variables z4and z5are not included in the figure.
constraint (2) we can deduce z1≤ 2 and z2≤ 3 (see Figure 4). Using constraint (3) and the new bounds on z1 and z2 it follows x2 = 0. By inserting the bound on z2
into constraint (6) we can also infer z3 ≤ 5. After branching on x3= 1 and x6= 0 and applying the deductions that follow from these branching decisions we arrive at the situation depicted in Figure 4 with the LP relaxation being infeasible. Note that the non-binary variables zi appear more than once in the conflict graph. For example, the upper bound of z3was changed once and the lower bound was changed twice. The implications on variables z4 and z5 are not included in the figure. They can be tightened to 7 ≤ z4≤ 11 and 4 ≤ z5≤ 6.
We use the following notation in the rest of the paper. Let BL= {B1, . . . , BK} with hyperplanes Bk = Lµjkk := {x | xjk ≥ µk} or Bk = Ujµkk := {x | xjk ≤ µk}, 1 ≤ jk≤ n, ljk≤ µk≤ ujk, k = 1, . . . , K. The set BL corresponds to the additional bounds imposed on the variables in the local subproblem. Thus, the subproblem is defined as
(MIP′) max{cTx| Ax ≤ b, l ≤ x ≤ u, xj∈ Z for all j ∈ I, x ∈ \
B∈BL
B}
The vertices of the conflict graph correspond to the local bound changes BL. As before, the arcs of the graph represent the implications.
3.2 Analyzing Infeasible LPs
In order to analyze the conflict expressed by an infeasible LP, we have to find a subset BC⊆ BLof the local bound changes that suffice to render the LP (together with the global bounds and rows1) infeasible. If all these remaining bound changes are fixings of binary variables, this already leads to a valid inequality of type (1). Furthermore,
1In a branch-and-cut framework, we have to either remove local cuts from the LP or mark the resulting conflict clause being only locally valid at the depth level of the last local cut remaining in the LP. Removing local rows can of course render the LP feasible again, thus making conflict analysis impossible.
even if bound changes on non-binary variables are present, such a subset can be used like the conflict detecting clause in SAT to represent the conflict in the conflict graph. Analysis of this conflict graph may also lead to a valid inequality.
A reasonable heuristic to select BC ⊆ BL is to try to make |BC| as small as possible. This would produce a conflict graph with the least possible number of predecessors of the conflict vertex and thus (hopefully) a small conflict clause. Un- fortunately, the problem of finding the smallest subset of BLwith the LP still being infeasible is N P-hard:
Definition 3.2 Let A ∈ Rm×n, b ∈ Rm, and F = {x | Ax ≤ b}. Let BL = {B1, . . . , BK} be additional bounds with Bk = {x | xjk ≥ µk} or Bk = {x | xjk ≤ µk}, 1 ≤ jk ≤ n, for all k = 1, . . . , K, such that F ∩ (T
B∈BLB) = ∅. Then, the minimal cardinality bound-IIS2 problem is to find a subset BC⊆ BL with
F∩ ( \
B∈BC
B) = ∅, and |BC| = min
B⊆BL
n|B|
F∩ (\
B∈B
B) = ∅o .
Lemma 3.3 The minimal cardinality bound-IIS problem is N P-hard.
Proof. We provide a reduction from the minimal cardinality IIS problem, which is N P-hard [4]. Given an instance F′= (A, b) of the minimal cardinality IIS problem with {x | Ax ≤ b} = ∅, the task is to find a minimal cardinality subset of the rows of Ax ≤ b that still defines an infeasible subsystem. Consider now the minimal cardinality bound-IIS problem instance F = {(x, s) ∈ Rn×m | Ax + s = b} and BL = {B1, . . . , Bm} with Bi = {(x, s) | si ≥ 0} for i = 1, . . . , m. Then, for each subset B ⊆ BL, the index set IB= {i | Bi ∈ B} defines an infeasible subsystem of F′ if and only if F ∩ (T
B∈BB) = ∅. Hence, there exists a one-to-one correspondence between the set of solutions of (F, BL) and the one of F′. Because |IB| = |B|, the optimal solution of (F, BL) defines an optimal solution of F′. 2 There are various heuristics for minimal cardinality IIS (see [19]). These can easily be specialized to the minimal cardinality bound-IIS problem. We implemented a preliminary version of a heuristic based on one of these methods which applies the Farkas lemma, but the overhead in running time was very large. Therefore, we employ very simple heuristics using the LP information at hand, which are described in the following.
First, we will only consider the case with the global lower bounds l and local lower bounds ˜l being equal to l = ˜l = 0. We further assume that each component of the global upper bounds u was tightened at most once to obtain the local upper bounds ˜u ≤ u. Thus, the set of local bound changes BL consists of at most one bound change for each variable.
Suppose the local LP relaxation
(P) max{cTx| Ax ≤ b, 0 ≤ x ≤ ˜u}
is infeasible. Then its dual
(D) min{bTy+ ˜uTr| ATy+ r ≥ c, (y, r) ≥ 0}
has an unbounded ray, i.e., (¯y,¯r) ≥ 0 with ATy¯+ ¯r= 0 and bTy¯+ ˜uTr <¯ 0. Note that the dual LP does not need to be feasible.
2IIS: irreducible inconsistent subsystem (an infeasible subsystem all of whose proper subsystems are feasible)
We can aggregate the rows and bounds of the primal LP with the non-negative weights (¯y,r) to get the following proof of infeasibility:¯
0 = (¯yTA+ ¯rT)x ≤ ¯yTb+ ¯rTu <˜ 0. (13) Now we try to relax the bounds as much as possible without loosing infeasibility.
Note that the left hand side of (13) does not depend on ˜u. Relaxing ˜u to some ˆu with ˜u≤ ˆu≤ u increases the right hand side of (13), but as long as ¯yTb+ ¯rTu <ˆ 0, the relaxed LP
( ˆP) min{cTx| Ax ≤ b, 0 ≤ x ≤ ˆu}
is still infeasible with the same infeasibility proof (¯y,¯r). This leads to the following heuristic to produce a relaxed upper bound vector ˆuwith the corresponding LP still being infeasible.
Algorithm 3.4 Let max{cTx| Ax ≤ b, 0 ≤ x ≤ ˜u≤ u} be an infeasible LP with dual ray (¯y,¯r).
1. Set ˆu:= ˜u, and calculate the infeasibility measure d := ¯yTb+ ¯rTu <ˆ 0.
2. Select a variable j with ˆuj < uj and dj := d + ¯rj(uj− ˜uj) < 0. If no such variable exists, stop.
3. Set ˆuj := uj, update d := dj, and go to 2.
In the general case of multiple bound changes on a single variable, we have to process these bound changes step by step, always relaxing to the previously active bound. In the presence of non-zero lower bounds the reduced costs r may also be negative. In this case, we can split up the reduced cost values into r = ru− rl. It follows from the Farkas lemma that ru· rl = 0. The infeasibility measure d of the dual ray has to be defined in Step 1 as d := ¯yTb+ (¯ru)Tuˆ+ (¯rl)Tˆl. A local lower bound ˜l can be relaxed in the same way as an upper bound ˜u, where u has to be replaced by l in the formulas of Steps 2 and 3.
Example 3.5 (continued) After applying the deductions on the bounds of the variables in Example 3.1, the LP relaxation is infeasible. Let y(i) denote the dual variable of constraint (i) and rj the reduced cost value of variable j. Then the dual ray ¯y(10) = 2, ¯y(11) = 1, ¯y(12) = 1, ¯rz1 = 2, ¯rz2 = −3, ¯rz3 = −1, and the remaining coefficients set to zero proves the infeasibility of the LP. In Step 1 of Algorithm 3.4 the infeasibility measure is calculated as
d = ¯y(10)b(10)+ ¯y(11)b(11)+ ¯y(12)b(12)+ ¯rzu1u˜z1− ¯rlz2˜lz2− ¯rlz3˜lz3
= 2 · 1 + 1 · 2 + 1 · 1 + 2 · 1 − 3 · 2 − 1 · 3 = −2.
In Step 2, all local bounds except the upper bound of z1 and the lower bounds of z2 and z3 can be relaxed to the corresponding global bounds, because their reduced cost values in the dual ray are zero. Additionally, the lower bound of z3 can be relaxed from 3 to 2, which was the lower bound before z3 ≥ 3 was deduced. This relaxation increases d by 1 to d = −1. No further relaxations are possible without increasing d to d ≥ 0. Thus, the local bounds z1 ≤ 1, z2 ≥ 2, and z3 ≥ 2 are identified as initial reason for the conflict, and the “global” arc from the LP to the conflict vertex in Figure 4 can be replaced by three arcs as shown in Figure 5.
x1= 1
x2= 0 x3= 1
x4= 1
x5= 0
x6= 0
x7= 1 z1≤2
z2≤3
z3≤5
z3≥2
z2≥2
z3≥3
z1≤1
λ
B A
Figure 5. Conflict graph of Example 3.1 after the infeasible LP was analyzed. Cut ’A’ is the 1-FUIPcut. Cut ’B’ was constructed by moving the non-binary variables of the conflict set of cut
’A’ to the conflict side.
3.3 Analyzing LPs Exceeding the Primal Bound
In principle, the case of an LP exceeding the primal bound can be handled as in the previous section by adding an appropriate objective bound inequality to the constraint system. In the implementation, however, we use the dual solution directly as a proof of objective bound exceedance. Then, we relax the bounds of the variables as long as the dual solution’s objective value stays below the primal bound. Again, we describe the case with l = ˜l = 0 and with at most one upper bound change per variable on the path from the root node to the local subproblem.
Suppose, the local LP relaxation
(P ) max{cTx| Ax ≤ b, 0 ≤ x ≤ ˜u}
exceeds (i.e., falls below) the primal objective bound ¯z. Then the dual (D) min{bTy+ ˜uTr| ATy+ r ≥ c, (y, r) ≥ 0}
has an optimal solution (¯y,r) with b¯ Ty¯+ ˜uTr¯≤ ¯z. Note that the variables’ upper bounds ˜udo not affect dual feasibility. Thus, after relaxing the upper bounds ˜uto a vector ˆuwith ˜u≤ ˆu≤ u that also satisfies bTy¯+ ˆuTr¯≤ ¯z, the LP’s objective value stays below the primal objective bound.
After relaxing the bounds, the vector (¯y,¯r) is still feasible, but not necessarily optimal for the dual LP. We may resolve the dual LP in order to get a stronger dual bound which can be used to relax further local upper bounds. The following algorithm summarizes this procedure.
Algorithm 3.6 Let max{cTx | Ax ≤ b, 0 ≤ x ≤ ˜u ≤ u} be an LP, ¯z a primal objective bound, and (¯y,r) a dual feasible solution with b¯ Ty¯+ ˜uTr¯≤ ¯z.
1. Set ˆu:= ˜u.
2. Calculate the bound exceedance measure d := bTy¯+ ˆuT¯r− ¯z≤ 0.
3. Select a variable j with ˆuj < uj and dj := d + ¯rj(uj− ˜uj) ≤ 0. If no such variable exists, go to 5.
4. Set ˆuj := uj, update d := dj, and go to 3.
5. (optional) If at least one upper bound was relaxed in the last iteration, resolve the dual LP to get the new dual solution (¯y,¯r), and go to 2.
3.4 Conflict Constraints with Non-binary Variables
Despite the technical issue of dealing with bound changes instead of fixings in the conflict graph, there is also a principle obstacle in the presence of non-binary vari- ables, which is the construction of the conflict constraint if non-binary variables appear in the conflict set.
The conflict graph analysis yields a conflict set, which is a subset Bf⊆ BL that together with the global bounds l and u suffices to render the current subproblem infeasible. This conflict set leads to the conflict constraint
_
Lµj∈Bf
(xj < µ) ∨ _
Ujµ∈Bf
(xj> µ).
If at least one of the conflict variables xj is continuous, the linearization of the conflict constraint would remain a strict inequality, which cannot be handled by an LP solver. If all conflict variables are integers, the conflict constraint has the form
_
Lµj∈Bf
(xj≤ µ − 1) ∨ _
Ujµ∈Bf
(xj≥ µ + 1). (14)
As shown in the introduction of Section 3, this constraint can be expressed by the set covering constraint (1) if all conflict variables are binary. However, if a general integer variable is involved in the conflict, we cannot use such a simple linearization.
In this case, (1) can be modeled with the help of auxiliary variables yµj, zjµ∈ {0, 1}:
X
Lµj∈Bf
yjµ+ X
Ujµ∈Bf
zjµ≥ 1
xj− (µ − 1)yµj ≤ 0 for all Lµj ∈ Bf
xj− (µ + 1)zjµ≥ 0 for all Ujµ ∈ Bf
(15)
The question arises, whether the potential gain in the dual bound justifies the ex- penses in adding system (15) to the LP. Many fractional points violating conflict constraint (14) cannot even be separated by (15) if the integrality restrictions on the auxiliary variables are not enforced through other cutting planes or branching.
This suggests that system (15) is probably very weak, although we did not verify this hypotheses by computational studies.
We therefore refrain from creating conflict constraints with non-binary variables.
Instead, we modified the cut selection rules in the conflict graph analysis in order to always choose the cut such that the non-binary variables are not involved in the resulting conflict set. This can be achieved by moving the bound changes on non-binary variables from the reason side’s frontier to the conflict side of the cut.
However, this is not possible if the bound change was due to a branching decision, because branching vertices must be located on the reason side. In this case, we just remove the bound change from the conflict set, thereby destroying the global validity of the resulting conflict clause. The clause can therefore only be added to the local subtree which is rooted at the node where the bound change on the non-binary variable was applied.
Example 3.7 (continued) Figure 5 shows the conflict graph of Example 3.1 after branching on x1 = 1, x3 = 1, and x6 = 0. The analysis of the LP relaxation identified z1 ≤ 1, z2 ≥ 2, and z3 ≥ 2 as sufficient to cause an infeasibility in the LP. The 1-FUIP cut selection scheme leads to the cut labeled ’A’ in the figure. The corresponding conflict constraint is
(z2≤ 1) ∨ (z3≤ 1).
Because there are non-binary variables involved in the conflict constraint, it cannot be represented by the set covering constraint (1). To avoid the introduction of the auxiliary variables of System (15), the bound changes z2≥ 2 and z3≥ 2 are put to the conflict side, resulting in cut ’B’. Thus, the conflict constraint that is added to the constraint database is (x2= 1) ∨ (x4= 0) ∨ (x7= 0), which can be written as
x2+ (1 − x4) + (1 − x7) ≥ 1.
4 Computational Results
In this section we examine the computational effectiveness of conflict analysis on several MIP instances. All calculations were performed on a 3.2 GHz Pentium-4EE workstation with 2 GB RAM. In all runs we used a time limit of 3600 seconds.
The conflict analysis techniques described in Sections 2 and 3 were implemented into the constraint and mixed integer programming framework SCIP version 0.79a (see [1]). Conflicts detected in constraint propagation and infeasible (or bound exceeding) LP relaxations of local nodes are analyzed to produce conflict clauses.
Additionally, infeasibilities of LP relaxations that are detected in the strong branch- ing calls of the reliability branching rule [3] are examined with the same algorithms.
If the initial conflict set produced by the LP analysis already consists of only binary variables, the corresponding conflict clause is added to the constraint database. In every case, the conflict graph analysis produces additional conflict clauses with the 1-FUIP and All-FUIP schemes [23] and reconvergence clauses to connect the last depth level’s first UIP and branching vertex.
To solve the LP relaxations, the dual simplex algorithm of CPlex is applied. It immediately stops after a dual feasible solution that exceeds the primal bound has been found. This solution, which is usually not optimal, can result in a very small initial bound exceedance measure (Algorithm 3.6 Step 2). In order to get useful initial conflict sets, we continue solving the LP to optimality without objective limit and use the optimal solution for LP infeasibility analysis. The optional Step 5 of Algorithm 3.6 is not applied, because it usually reduces the size of the initial conflict set by only a few additional bound changes and therefore does not justify its additional costs.
We only separate cutting planes in the root node, which seems to yield the best performance on most MIP instances using SCIP.3 The generated conflict clauses are added on demand to the LP relaxations at local nodes and take part in the propagation process inside the local nodes’ solving loop.
Because the recorded conflict clauses increase the costs for processing the sub- problems, we try to only keep the “useful” conflict clauses. We implemented a constraint aging mechanism to identify useless conflict clauses. Clauses are deleted, if they did not help for a couple of consecutive iterations to tighten the LP relaxation
3In the current version, SCIP separates Gomory MIR cuts, strong CG cuts, c-MIR cuts, lifted knapsack cover cuts, implied bound cuts, and clique cuts.
during separation or propagation. Longer clauses are discarded earlier than clauses with fewer literals.
4.1 Test Set
Our first test set consists of instances from Miplib 2003 [2] and instances collected by Mittelmann [17]. We selected all problems where CPlex 9.03 needs at least 1000 branching nodes and 30 seconds and at most one hour CPU time for solving.4
As a second test set, we use IP models of chip design verification problems. The data are for a very simple arithmetic logical unit (ALU) of different register widths ranging from 4 to 10 bits and with different properties to be checked (see, e.g., [7]).
The instances, the ALU model, and the property definitions can be found in the contributed instances section of Miplib 2003.
The so-called property checking problem addressed here is to prove the validity of a certain property for a given chip design. This problem can be modeled as IP, where each feasible solution represents a counter-example of the property. Hence, in order to prove that the property holds, one has to show the infeasibility of the IP.
All of the ALU instances investigated here correspond to valid properties, i.e., the IP instances are infeasible.
Note that the ALU design includes signed and unsigned multiplication of the two input registers. The internal calculations for multiplying the n-bit input registers operate on 2n-bit variables. Therefore, the IP instances include integer variables and matrix coefficients that are in the range of 22n. In order to overcome the numerical difficulties arising from such large values, we had to set the solvers’ feasibility and integrality tolerances for this second test set to 10−9.
4.2 Description of the Results
Table 1 gives some statistics on the problems in the first test set and shows the results with the default settings for MIP solving and those with activated conflict analysis.
Columns ‘Rows’, ‘Cols’, ‘Bins’, and ‘Ints’ show the number of rows, columns, binary, and general integer variables of the problem instances, respectively. Columns ‘Nodes’
and ‘Time’ show the number of branching nodes and the total time in seconds needed to solve the instances. Values marked with a ‘>’ denote that the instance could not be solved within the time limit. The comparison with CPlex indicates that SCIP’s performance (using CPlex as LP solver) is not strictly competitive, but not far away from a state-of-the-art MIP solver.
We can observe that conflict analysis yields a reduction of branching nodes of about 50% in terms of the geometric mean. Nevertheless, this does not reduce the total running time. In fact, the geometric mean of the running time increases by about 15%. Similar observations can be made for the reduced test set consisting of only those instances that could be solved by both settings within the time limit. A closer look at the single instances reveals that activating conflict analysis reduces the number of nodes on 21 instances and the solving time on 12 instances. The default MIP setting needs fewer nodes on 5 instances and is faster on 16 instances.
Table 2 gives a more detailed timing analysis of the two settings. The basic time (BTime) is the time spent for presolving, node processing (including LP solving), and primal heuristics. In particular, this also includes the additional overhead of processing the conflict constraints in domain propagation and cut separation. The
4CPlex was run with default settings, except that “absolute mipgap” was set to 10−9 and
“relative mipgap” to 0.0, which are the corresponding values in SCIP.
Problem Size CPlex9.03 SCIP0.79a (default) SCIP0.79a (conflict)
Name Rows Cols Bins Ints Nodes Time Nodes Time Nodes Time
10teams 230 2025 1800 2 771 63.5 596 73.8 313 77.0
aflow30a 479 842 421 37 116 86.9 14 269 77.6 6 322 66.3
mas74 13 151 150 5 311 878 1306.6 3 378 402 902.1 >810 784 >3600.0 mas76 12 151 150 375 729 56.8 566 581 152.3 >437 272 >3600.0
misc07 212 260 259 72 420 60.2 35 210 47.8 41 138 87.1
mzzv11 9499 10240 9989 251 3 820 443.4 4 668 1285.2 2 847 1269.5
pk1 45 86 55 365 710 86.8 230 529 86.3 352 533 644.0
qiu 1192 840 48 11 431 107.5 10 023 166.8 9 275 207.5
rout 291 556 300 15 843 504 1845.2 27 476 52.2 8 988 38.1
acc-6 3047 1335 1335 1 084 656.5 >8 959 >3600.1 5 398 2582.4
bc1 1913 1751 252 9 939 270.4 62 624 1514.9 564 125.5
bienst1 576 505 28 12 292 113.7 9 064 61.3 5 842 52.2
bienst2 576 505 35 161 843 2381.4 89 989 868.6 77 768 980.8
mkc1 3411 5325 3087 14 236 48.9 >449 959 >3600.0 >294 204 >3600.0
neos2 1103 2101 1040 40 193 83.5 129 695 314.9 10 736 125.0
neos3 1442 2747 1360 835 129 2630.7 >903 445 >3600.0 103 956 1310.7
neos6 1036 8786 8340 5 328 232.6 1 033 191.9 2 224 293.6
neos7 1994 1556 434 20 113 861 423.3 40 056 390.3 36 974 446.3
neos11 2706 1220 900 3 058 179.7 11 247 1018.4 9 832 1537.0
neos21 1085 614 613 7 531 85.1 1 611 36.3 1 579 62.0
neos22 5208 3240 454 13 520 45.2 30 598 282.0 24 615 318.3
prod1 208 250 149 97 507 68.2 67 311 45.2 43 486 64.9
ran10x26 296 520 260 20 176 42.0 50 525 116.0 21 451 85.8
ran12x21 285 504 252 81 525 159.2 129 096 282.2 47 764 218.8
ran13x13 195 338 169 62 936 63.6 103 302 118.2 21 459 60.5
seymour1 4944 1372 451 10 459 1056.2 4 378 880.9 4 206 1103.5
swath1 884 6805 2306 15 860 42.2 378 31.6 387 45.9
swath2 884 6805 2406 150 740 383.2 12 418 120.3 12 450 187.2
swath3 884 6805 2706 728 982 2180.0 54 858 401.0 44 382 545.9
Total (29) 9 410 578 15202.4 6 428 300 20318.4 2 438 749 23335.9
Geom. Mean 41 268 202.0 29 633 257.2 15 441 297.8
Reduced (24) 2 872 522 10502.7 1 120 954 8463.9 787 135 8642.9
Geom. Mean 32 994 178.8 17 509 179.4 9 720 187.4
Table 1. Comparison of runs with CPlex 9.03, SCIP with default MIP settings, and SCIP with conflict analysis. Results marked with ‘>’ were not solved to optimality within the time limit. The totals and geometric means are given for the full test set as well as the reduced test set excluding those instances (printed in bold face) not solved to optimality by one or both of the two SCIP settings.
switching time (STime) denotes the time used for setting up the subproblems to be processed. This includes updating the set of local constraints and the variables’
local bounds. The conflict analysis time (CTime) summarizes the extraction of starting conflicts from infeasible and bound exceeding LPs as well as the conflict graph analysis itself. The largest fraction of this time is usually spent to continue solving bound exceeding LPs to optimality in order to get useful initial conflict sets.
The additional columns ’Confs’ and ’∅Lits’ show the number of conflict clauses generated during each run and the average number of literals per conflict clause, respectively.
One can see that the reduction of 50% in the number of branching nodes ob- tained with conflict analysis lead to a saving of 10% in the basic solution time in terms of the geometric mean. Unfortunately, this does not result in an overall per- formance improvement, because the additional costs for the conflict analysis itself (in particular to continue solving the LPs to optimality) outweigh the benefit of the node reduction. In addition, due to the additional constraints generated in the local nodes, the switching time increases. This increase in switching time has the most
