Забыли?

?

# Conflict Graph - SCIP - Konrad-Zuse

код для вставкиСкачать
Conflict Analysis
SCIP Workshop at ZIB
October 2007
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
п‚§ 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
п‚§ 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
###### Документ
Категория
Презентации
Просмотров
8
Размер файла
2 686 Кб
Теги
1/--страниц
Пожаловаться на содержимое документа