Automatic Solver Configuration
Lars Kotthoff
larsko@cs.st-andrews.ac.uk
University of St Andrews
with Dharini Balasubramaniam, Lakshita de Silva, Ian Gent, Chris
Jefferson, Ian Miguel and Peter Nightingale
Aim
Automatic generation of problem-specific,
high-performance constraint solvers
The Dominion Project
The Dominion Project
template ThisProblem() {
provides IProblem;
requires IPropVariable pvw, pvx, pvy, pvz, pvc6;
requires ISumEqCon scA, scB;
check pvx.getProperties() subsetof
[(domainType, 'bound'), (domainSize, 2)];
check pvy.getProperties() subsetof
[(domainType, 'bound')];
check pvc6.getProperties() subsetof
[(domainType, 'bound'), (domainSize, 1)];
check scA.param(1) accepts (pvx +
[(domainType, 'bound'), (domainSize, 2)]);
check scA.param(1) accepts (pvy +
[(domainType, 'bound')]);
check scA.param(2) accepts (pvw +
[(domainType, 'bound'), (domainSize, 1)]);
check scA.param(2) accepts (pvc6 +
[(domainType, 'bound'), (domainSize, 1)]);
check scB.param(1) accepts (pvx +
[(domainType, 'bound'), (domainSize, 2)]);
check scB.param(1) accepts pvz;
}
}
template ThisProblem() {
provides IProblem;
requires IPropVariable pvw, pvx, pvy, pvz, pvc6;
requires ISumEqCon scA, scB;
check pvx.getProperties() subsetof
[(domainType, 'bound'), (domainSize, 2)];
check pvy.getProperties() subsetof
[(domainType, 'bound')];
check pvc6.getProperties() subsetof
[(domainType, 'bound'), (domainSize, 1)];
check scA.param(1) accepts (pvx +
[(domainType, 'bound'), (domainSize, 2)]);
check scA.param(1) accepts (pvy +
[(domainType, 'bound')]);
check scA.param(2) accepts (pvw +
[(domainType, 'bound'), (domainSize, 1)]);
check scA.param(2) accepts (pvc6 +
[(domainType, 'bound'), (domainSize, 1)]);
check scB.param(1) accepts (pvx +
[(domainType, 'bound'), (domainSize, 2)]);
check scB.param(1) accepts pvz;
}
template DiscreteVariableFactory() {
provides IPropVariable;
provides IRemoveFromDomain;
requires IMemoryManager domain;
requires IMemoryManager bounds;
property domainType = "bound";
check domain.getProperties() subsetof
[(MemoryChanges, 'Single')];
check bounds.getProperties() subsetof
[];
}
template BoolVariableFactory() {
provides IPropVariable;
provides IRemoveFromDomain;
requires IMemoryManager bounds;
property domainType = "bound";
check bounds.getProperties() subsetof [(MemoryChanges, 'Single')];
property domainSize = 2;
}
template ConstantVariableFactory() {
provides IPropVariable;
provides IRemoveFromDomain;
property domainSize = 1;
property domainType = "bound";
}
template ThisProblem() {
provides IProblem;
requires IPropVariable pvw, pvx, pvy, pvz, pvc6;
requires ISumEqCon scA, scB;
check pvx.getProperties() subsetof
[(domainType, 'bound'), (domainSize, 2)];
check pvy.getProperties() subsetof
[(domainType, 'bound')];
check pvc6.getProperties() subsetof
[(domainType, 'bound'), (domainSize, 1)];
check scA.param(1) accepts (pvx +
[(domainType, 'bound'), (domainSize, 2)]);
check scA.param(1) accepts (pvy +
[(domainType, 'bound')]);
check scA.param(2) accepts (pvw +
[(domainType, 'bound'), (domainSize, 1)]);
check scA.param(2) accepts (pvc6 +
[(domainType, 'bound'), (domainSize, 1)]);
check scB.param(1) accepts (pvx +
[(domainType, 'bound'), (domainSize, 2)]);
check scB.param(1) accepts pvz;
}
template GACSumFactory(P1, P2) {
provides ISumEqCon;
requires IMemoryManager m;
check m.getProperties() subsetof [];
check [IRawMemory] subsetof m.getInterfaces();
check [IRemoveFromDomain,IPropVariable]
subsetof P1.getInterfaces();
check [IRemoveFromDomain,IPropVariable]
subsetof P2.getInterfaces();
}
template BoolSumFactory(P1, P2) {
provides ISumEqCon;
requires IMemoryManager m;
check m.getProperties() subsetof [];
check [(domainSize, 2)] subsetof
P1.getProperties();
check [(domainSize, 1)] subsetof
P2.getProperties();
check [IPropVariable] subsetof
P1.getInterfaces();
check [IPropVariable] subsetof
P2.getInterfaces();
}
The Problem
select and connect solver components satisfying certain
restrictions
The Problem
select and connect solver components satisfying certain
restrictions
Model and solve as a constraint problem!
requires IPropVariable pvw, pvx,
pvy, pvz, pvc6;
|
DISCRETE pvw {1..3}
DISCRETE pvx {1..3}
DISCRETE pvy {1..3}
DISCRETE pvz {1..3}
DISCRETE pvc6 {1..3}
|
template ConstantVariableFactory() {
provides IPropVariable;
provides IRemoveFromDomain;
property domainSize = 1;
property domainType = "bound";
}
|
BOOL pvw_provides[7]
BOOL pvw_properties[4]
|
requires IPropVariable pvw, pvx,
pvy, pvz, pvc6;
|
DISCRETE pvw {1..3}
DISCRETE pvx {1..3}
DISCRETE pvy {1..3}
DISCRETE pvz {1..3}
DISCRETE pvc6 {1..3}
|
template ConstantVariableFactory() {
provides IPropVariable;
provides IRemoveFromDomain;
property domainSize = 1;
property domainType = "bound";
}
|
BOOL pvw_properties[4]
BOOL pvw_provides[7]
|
requires IPropVariable pvw, pvx,
pvy, pvz, pvc6;
|
DISCRETE pvw {1..3}
DISCRETE pvx {1..3}
DISCRETE pvy {1..3}
DISCRETE pvz {1..3}
DISCRETE pvc6 {1..3}
|
template ConstantVariableFactory() {
provides IPropVariable;
provides IRemoveFromDomain;
property domainSize = 1;
property domainType = "bound";
}
|
BOOL pvw_properties[4]
BOOL pvw_provides[7]
|
template DiscreteVariableFactory() {
provides IPropVariable;
...
requires IMemoryManager domain;
requires IMemoryManager bounds;
...
}
|
DISCRETE pvw_1_bounds {1..3}
BOOL pvw_1_bounds_properties[4]
BOOL pvw_1_bounds_provides[7]
|
template ConstantVariableFactory() {
provides IPropVariable;
provides IRemoveFromDomain;
property domainSize = 1;
property domainType = "bound";
}
eq(pvw_provides[0], 0)
eq(pvw_provides[1], 0)
eq(pvw_provides[2], 0)
reify(watched-or({eq(pvw, 1),
eq(pvw, 2),
eq(pvw, 3),
eq(pvw, 4)}),
pvw_provides[3])
reify(watched-or({eq(pvw, 2),
eq(pvw, 3),
eq(pvw, 4)}),
pvw_provides[4])
eq(pvw_provides[5], 0)
eq(pvw_provides[6], 0)
check scA.param(2) accepts (pvw +
[(domainType, 'bound'), (domainSize, 1)]);
reifyimply(eq(pvw_properties[0], 1),
scA_param_2_properties[0])
reifyimply(eq(pvw_provides[0], 1),
scA_param_2_provides[0])
reifyimply(eq(pvw_properties[2], 1),
scA_param_2_properties[2])
reifyimply(eq(pvw_provides[3], 1),
scA_param_2_provides[3])
reifyimply(eq(pvw_provides[6], 1),
scA_param_2_provides[6])
check [(domainSize, 2)] subsetof P1.getProperties();
check [(domainSize, 1)] subsetof P2.getProperties();
check [IPropVariable] subsetof P1.getInterfaces();
check [IPropVariable] subsetof P2.getInterfaces();
reify(watched-and({eq(scA, 3)}),
scA_3_param_1_properties_channel[2])
reifyimply(eq(scA_param_1_properties[2], 1),
scA_3_param_1_properties_channel[2])
reify(watched-and({eq(scA, 3)}),
scA_3_param_2_properties_channel[3])
reifyimply(eq(scA_param_2_properties[3], 1),
scA_3_param_2_properties_channel[3])
Solution
system Solution {
component vw = ConstantVariableFactory();
component vx = BooleanVariableFactory();
component vy = DiscreteVariableFactory();
component vz = DiscreteVariableFactory();
component vc6 = ConstantVariableFactory();
component conAf = GACSumFactory();
component conBf = GACSumFactory();
component problem = ThisProblem();
link vw.var to problem.pvw;
link vx.var to problem.pvx;
link vy.var to problem.pvy;
link vz.var to problem.pvz;
link vc6.var to problem.pvc6;
link conAf.con to problem.scA;
link conBf.con to problem.scB;
}
Disadvantages
- hard to understand transformation into constraint problem
- no direct control over which configuration selected
- does not take properties of original problem into account
Different approach
- Markov logic networks
- Statistical Relational Learning
Alchemy
alchemy.cs.washington.edu
Out of memory.
Questions?
Thank you!