close

Вход

Забыли?

вход по аккаунту

?

Conflict Graph - SCIP - Konrad-Zuse

код для вставкиСкачать
Conflict Analysis
SCIP Workshop at ZIB
October 2007
Konrad-Zuse-Zentrum fГјr Informationstechnik Berlin (ZIB)
Tobias Achterberg
achterberg@zib.de
2
General Idea
 Problem is divided into smaller subproblems
 branching tree
 Some subproblems are infeasible
 Analyzing the infeasibilities can yield information
about the problem
 Information can be used at other subproblems to
prune the search tree
3
Example
x1 = 1
x2 = 0
c1:
x1 – x2 – x3  0
c2:
x1 + x2 – x3  1
x3 = 0
 a subproblem is infeasible
4
Example
x1 = 1
x2 = 0
x3 = 0
c1:
x1 – x2 – x3  0
c2:
x1 + x2 – x3  1
c3:
x1
– x3  0
 a subproblem is infeasible
 conflict analysis yields feasible constraint, that
cuts off other nodes in the tree
5
Outline
 Conflict Analysis in SAT
 Conflict Analysis in MIP
 Implementation
 Computational Results
6
Outline
 Conflict Analysis in SAT
 Conflict Analysis in MIP
 Implementation
 Computational Results
7
Satisfiability Problem (SAT)
 Boolean variables x1,...,xn  {0,1}
 Clauses
C1:
l11 пѓљ ... пѓљ l1k1
...
Cm:
ln1 пѓљ ... пѓљ lmkm
with literals
lik = xj or lik =пЃ xj = 1 – xj
 Task:
 find assignment x*  {0,1}n that satisfies all clauses,
or prove that no such assignment exists
8
Binary Constraint Propagation
 clause:
x6 пѓљ x7 пѓљ x9 пѓљ x10
9
Binary Constraint Propagation
x6
x9
x7
 clause:
x6 пѓљ x7 пѓљ x9 пѓљ x10
 fixings:
x6 пЂЅ 0, x7 пЂЅ 1, x9 пЂЅ 0
10
Binary Constraint Propagation
x6
x9
x7
x 10
 clause:
x6 пѓљ x7 пѓљ x9 пѓљ x10
 fixings:
x6 пЂЅ 0, x7 пЂЅ 1, x9 пЂЅ 0
 deduction:
x6 пѓ™ x7 пѓ™ x9 п‚® x10
11
Conflict Graph
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
x 10
x3
x6 пѓљ x7 пѓљ x9 пѓљ x10
 decision variables
 deduced variables
 conflict
пЃ¬
12
Conflict Graph
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
пЃ¬
x 10
x3
 decision variables
 deduced variables
 conflict
conflict detecting clause
x13 пѓљ x14 пѓљ x15
13
Conflict Graph – Conflict Cuts
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
пЃ¬
x 10
x3
 choose cut that separates decision variables from
conflict vertex
14
Conflict Graph – Conflict Cuts
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
пЃ¬
x 10
x3
reason side
conflict side
 choose cut that separates decision variables from
conflict vertex
15
Conflict Graph – Conflict Cuts
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
пЃ¬
x 10
x3
reason side
conflict side
 choose cut that separates decision variables from
conflict vertex
 conflict clause: x  x  x  x
6
7
8
12
16
Conflict Graph – Trivial Cuts
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
x 10
x3
 -cut:
x13 пѓљ x14 пѓљ x15
 decision cut: x  x  x  x
1
4
6
8
пЃ¬
17
Conflict Graph – First-UIP
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
пЃ¬
x 10
x3
 Unique Implication Point: lies on all paths from
the last decision vertex to the conflict vertex
18
Conflict Graph – First-UIP
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
пЃ¬
x 10
x3
 Unique Implication Point: lies on all paths from
the last decision vertex to the conflict vertex
 First UIP: the UIP closest to  (except  itself)
19
Conflict Graph – First-UIP Cut
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
пЃ¬
x 10
x3
 Put all vertices fixed after First-UIP to the conflict
side, remaining vertices to the reason side
 First-UIP cut:
x3 пѓљ x11
20
Conflict Analysis Algorithm (FUIP)
пЃ¬
 BCP detected a conflict
21
Conflict Analysis Algorithm (FUIP)
x 13
x 14
пЃ¬
x 15
x13 пѓљ x14 пѓљ x15
 Initialize conflict queue with the variables
involved in the conflict
22
Conflict Analysis Algorithm (FUIP)
x 13
x 14
x 15
 Initialize conflict queue with the variables
involved in the conflict
пЃ¬
23
Conflict Analysis Algorithm (FUIP)
x 13
x 14
пЃ¬
x 15
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
24
Conflict Analysis Algorithm (FUIP)
x 13
x 14
x 12
пЃ¬
x 15
x12 пѓљ x15
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
25
Conflict Analysis Algorithm (FUIP)
x 13
x 14
x 12
пЃ¬
x 15
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
26
Conflict Analysis Algorithm (FUIP)
x 13
x 11
x 14
x 12
x 15
пЃ¬
x11 пѓљ x14
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
27
Conflict Analysis Algorithm (FUIP)
x 13
x 11
x 14
x 12
x 15
пЃ¬
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
28
Conflict Analysis Algorithm (FUIP)
x11 пѓљ x14
x 13
x 11
x 14
x 12
x 15
пЃ¬
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
29
Conflict Analysis Algorithm (FUIP)
x 13
x 11
x 14
x 12
x 15
пЃ¬
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
30
Conflict Analysis Algorithm (FUIP)
x 13
x3
x 11
x 14
x 12
x 15
пЃ¬
x3 пѓљ x11 пѓљ x12
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
31
Conflict Analysis Algorithm (FUIP)
x 13
x3
x 11
x 14
x 12
x 15
пЃ¬
 As long as there is more than one variable of the
last depth level in the queue, resolve the last
deduction
32
Conflict Analysis Algorithm (FUIP)
x 13
x3
x 11
x 14
x 12
x 15
пЃ¬
 If there is only one variable of the last depth
level left, stop
33
Conflict Analysis Algorithm (FUIP)
x 13
x3
x 11
x 14
x 12
x 15
пЃ¬
 If there is only one variable of the last depth
level left, stop
 The remaining variables define the conflict set
34
Conflict Analysis Algorithm (FUIP)
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
x 10
x3
 The conflict clause consists of all (negated)
assignments in the conflict set: x3 пѓљ x11
пЃ¬
35
Outline
 Conflict Analysis in SAT
 deductions lead to conflict  conflict graph
 cut in conflict graph  conflict clause
 Conflict Analysis in MIP
 Implementation
 Computational Results
36
Outline
 Conflict Analysis in SAT
 deductions lead to conflict  conflict graph
 cut in conflict graph  conflict clause
 Conflict Analysis in MIP
 Implementation
 Computational Results
37
Mixed Integer Program
max cTx
s.t.
Ax п‚Ј b
x пѓЋ Rpп‚ґZq
 linear objective function c
 linear constraints Ax  b
 real or integer valued variables x
38
Conflict Analysis for MIP
Two main differences to SAT:
 non-binary variables
 conflict graph: bound changes instead of fixings
 conflict clause  conflict constraint
39
Conflict Analysis for MIP
Two main differences to SAT:
 non-binary variables
 conflict graph: bound changes instead of fixings
 conflict clause  conflict constraint
40
Conflict Analysis for MIP
Two main differences to SAT:
 non-binary variables
 conflict graph: bound changes instead of fixings
 conflict clause  conflict constraint
 main reason for infeasibility: LP relaxation
 conflict graph has no link from the decision and
deduction vertices to the conflict vertex
41
Conflict Analysis for MIP
Two main differences to SAT:
 non-binary variables
 conflict graph: bound changes instead of fixings
 conflict clause  conflict constraint
 main reason for infeasibility: LP relaxation
 conflict graph has no link from the decision and
deduction vertices to the conflict vertex
analyze LP
42
Back to SAT: Conflict Graph
x1
x4
x6
x8
x 13
x2
x5
x9
x7
x 11
x 14
x 12
x 15
пЃ¬
x 10
x3
 One clause detected the
conflict
conflict detecting clause
x13 пѓљ x14 пѓљ x15
 Only a few variables linked to the conflict vertex
43
Infeasible LP: Conflict Graph
x1
x4 п‚і 5
x6
x8
x 13
x2
x5
x9
x7 п‚Ј 3
x11 п‚і 4
x 14
x 12
x 15
пЃ¬
x 10
x3
 The LP as a whole is responsible for the conflict
 All local bound changes are linked to the conflict
vertex
44
Infeasible LP: Conflict Graph
x1
x4 п‚і 5
x6
x8
x 13
x2
x5
x9
x7 п‚Ј 3
x11 п‚і 4
x 14
x 12
x 15
пЃ¬
x 10
x3
 LP analysis selects some of these local bounds
45
Infeasible LP: Conflict Graph
x1
x4 п‚і 5
x6
x8
x 13
x2
x5
x9
x7 п‚Ј 3
x11 п‚і 4
x 14
x 12
x 15
x 10
x3
 LP analysis selects some of these bounds
 cut yields conflict constraint
( x3 пЂЅ 1) пѓљ ( x5 пЂЅ 1) пѓљ ( x11 п‚Ј 3)
пЃ¬
46
Conflict Analysis for infeasible LPs
 if the LP relaxation is infeasible, the whole
relaxation is involved in the conflict
 all constraints
 all global bounds
 all local bounds
 try to find a small subset of the local bounds that
still leads to an infeasible LP relaxation
 variant of minimal infeasible subsystem problem
(see Amaldi, Pfetsch, Trotter)
 heuristic: use dual ray to relax local bounds
47
Infeasible LP: Dual Ray Heuristic
 LP relaxation: max cTx
s.t.
Ax п‚Ј b
0п‚Јxп‚ЈпЃ­п‚Јu
local bounds
48
Infeasible LP: Dual Ray Heuristic
 LP relaxation: max cTx
s.t.
Ax п‚Ј b
0п‚Јxп‚ЈпЃ­п‚Јu
 dual LP:
min
bTy + пЃ­Tr
s.t.
ATy + r п‚і c
y, r п‚і 0
local bounds
49
Infeasible LP: Dual Ray Heuristic
 LP relaxation: max cTx
s.t.
Ax п‚Ј b
local bounds
0п‚Јxп‚ЈпЃ­п‚Јu
 dual LP:
min
bTy + пЃ­Tr
s.t.
ATy + r п‚і c
y, r п‚і 0
 dual ray: (y*, r*)  0, ATy* + r*  0, bTy* + Tr* < 0
50
Infeasible LP: Dual Ray Heuristic
 LP relaxation: max cTx
s.t.
Ax п‚Ј b
local bounds
0п‚Јxп‚ЈпЃ­п‚Јu
 dual LP:
min
bTy + пЃ­Tr
s.t.
ATy + r п‚і c
y, r п‚і 0
 dual ray: (y*, r*)  0, ATy* + r*  0, bTy* + Tr* < 0
51
Infeasible LP: Dual Ray Heuristic
 LP relaxation: max cTx
s.t.
Ax п‚Ј b
local bounds
0п‚Јxп‚ЈпЃ­п‚Јu
 dual LP:
min
bTy + пЃ­Tr
s.t.
ATy + r п‚і c
y, r п‚і 0
 dual ray: (y*, r*)  0, ATy* + r*  0, bTy* + Tr* < 0
 relax bounds:
пЃ­i := ui , s.t. still bTy* + пЃ­Tr* < 0
52
Outline
 Conflict Analysis in SAT
 deductions lead to conflict  conflict graph
 cut in conflict graph  conflict clause
 Conflict Analysis in MIP
 deductions lead to infeasible LP
 LP analysis links conflict vertex
conflict graph
 cut in conflict graph  conflict constraint
 Implementation
 Computational Results
53
Outline
 Conflict Analysis in SAT
 deductions lead to conflict  conflict graph
 cut in conflict graph  conflict clause
 Conflict Analysis in MIP
 deductions lead to infeasible LP
 LP analysis links conflict vertex
conflict graph
 cut in conflict graph  conflict constraint
 Implementation
 Computational Results
54
Implementation
 Which pruned subproblems should be analyzed?
 propagation conflicts
yes
 infeasible LP conflicts
yes
 bound-exceeding LP conflicts
no
 strong branching conflicts
no
 How many conflict constraints per conflict?
 all FUIP constraints: 1-FUIP, 2-FUIP, ...
 How should conflict constraints be used?
 only for propagation, not as cutting planes
 How can useless conflict constraints be identified?
 "easy" for SAT due to depth-first-search
 open topic for best-first-search MIP, needs more ideas!
 currently: aging mechanism
55
How to Support Conflict Analysis
in User Plugins
 affected plugin types
 constraint handlers (propagation)
 propagator
 special bound inference methods for propagation
 SCIPinferVarLbCons(), SCIPinferVarUbCons()
 SCIPinferVarLbProp(), SCIPinferVarUbProp()
 provide constraint and one additional integer („inferinfo“)
 reverse propagation
 must provide the „reason“ for a bound deduction
 can use the inferinfo to help finding the reason
56
Reverse Propagation
x 13
x3
x 11
x 14
x 12
x 15
x3 пѓљ x11 пѓљ x12
 input: constraint and tightened bound
 x x x
deduced x12 п‚Ј 0
3
11
12
пЃ¬
57
Reverse Propagation
x 13
x3
x 11
x 14
x 12
x 15
x3 пѓљ x11 пѓљ x12
 input: constraint and tightened bound
 x x x
deduced x12 п‚Ј 0
3
11
12
 output: bounds that are reason for deduction
 x  0 and
3
x11 п‚і 1
пЃ¬
58
Reverse Propagation: Examples
 set covering constraints
 xj
п‚і 1, x j пѓЋ пЃ»0,1пЃЅ
 only one type of propagation
пЂўj п‚№ k : x j пЂЅ 0 пѓћ xk пЂЅ 1
 reverse propagation easy:
all variables except the inferred variable are reason variables
59
Reverse Propagation: Examples
 xj
 set covering constraints
п‚і 1, x j пѓЋ пЃ»0,1пЃЅ
 only one type of propagation
пЂўj п‚№ k : x j пЂЅ 0 пѓћ xk пЂЅ 1
 reverse propagation easy:
all variables except the inferred variable are reason variables
 linear constraints
 propagation of left and right hand side
ak пЂѕ 0 пѓћ xk п‚Ј
lhs   a j x j  rhs
пѓ¶
1 пѓ¦
 rhs   min a j x j 
ak пѓЁ
j п‚№ k l j п‚Ј x j п‚Јu j
пѓё
 inferinfo: array position of inferred variable and lhs/rhs indicator
 reverse propagation:
find set of variables j п‚№ k with bounds that trigger the deduction
60
Outline
 Conflict Analysis in SAT
 deductions lead to conflict  conflict graph
 cut in conflict graph  conflict clause
 Conflict Analysis in MIP
 deductions lead to infeasible LP
 LP analysis links conflict vertex
conflict graph
 cut in conflict graph  conflict constraint
 Implementation
 Computational Results
61
Outline
 Conflict Analysis in SAT
 deductions lead to conflict  conflict graph
 cut in conflict graph  conflict clause
 Conflict Analysis in MIP
 deductions lead to infeasible LP
 LP analysis links conflict vertex
conflict graph
 cut in conflict graph  conflict constraint
 Implementation
 Computational Results
62
Computational Results
 Instances of MIPLIB 2003 and Mittelmann
 that could be solved by one of the three in 1 hour
 for which one of the three needed at least 1000 nodes
47 instances
Fails
CPLEX 10.0
SCIP
SCIP + ConfA
5
3
3
13 429
18 192
14 507
Node Winner
(24)
14 (7)
27 (17)
Time
65.1
134.7
116.5
Time Winner
(33)
16 (4)
25 (11)
Nodes
nodes: -20%
time: -14%
63
Computational Results
 ALU instances up to 8 bits
 for which one of the three needed at least 1000 nodes
 infeasible MIP instances
21 instances
Fails
CPLEX 10.0
SCIP
SCIP + ConfA
0
1
1
35 657
6 272
910
(7)
0 (3)
16 (14)
Time
23.4
29.9
12.7
Time Winner
(12)
1 (4)
16 (9)
Nodes
Node Winner
nodes: -85%
time: -58%
64
Computational Results
 "Enlight" instances up to board size 10  10
 for which one of the three needed at least 1000 nodes
 2 infeasible and 4 feasible MIP instances
6 instances
Fails
Nodes
Node Winner
Time
Time Winner
CPLEX 10.0
SCIP
SCIP + ConfA
1
0
0
50 176
70 216
15 774
0
0
6
22.2
32.3
13.1
(4)
0 (0)
5 (2)
nodes: -78%
time: -59%
65
Computational Results
 instance "arki001" from MIPLIB 3.0 / MIPLIB 2003
 first solved by Balas and Saxena (Dec 2005)
 "Optimizing over the Split Closure"
 54 hours rank-1 split cut generation + 11 hours CPLEX 9.0
 Bob-tuned CPLEX:
 "using a lot of strong branching"
 628 hours, 103 million nodes
 SCIP:
 using an insane amount of strong branching
 full conflict analysis (bound-exceeding LPs and strong branchings)
SCIP
SCIP + ConfA
Nodes
5 054 427
1 857 512
Time
11.4 hours
5.2 hours
66
Computational Results
67
Computational Results
68
Computational Results
 instance „roll3000" from MIPLIB 2003
 SCIP:
 using an insane amount of strong branching
 moderate conflict analysis
 3.2GHz Pentium-IV
SCIP
SCIP + ConfA
Nodes
9 104 084
4 139 860
Time
20.0 hours
10.3 hours
 Unfortunately...
 XPressMP 2006B with tuned settings: 1 hour (3 GHz Athlon-64)
 Reported by Alkis Vazacopoulos (ISMP 2006)
 As far as I understood: lots of local cuts
Документ
Категория
Презентации
Просмотров
3
Размер файла
2 686 Кб
Теги
1/--страниц
Пожаловаться на содержимое документа