Modelling Constraint Solver Architecture Design as a Constraint Problem

Ian Gent, Chris Jefferson, Lars Kotthoff, Ian Miguel

larsko@cs.st-andrews.ac.uk

University of St Andrews

The Dominion Project

The Dominion Project

 
architecture Solver {
  template CopyMemoryFactory() {
    provides IMemoryManager;
    provides IRawMemory;
    provides IViewHistory;
  }
  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 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();
  }
  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;
  }
}
            
architecture Solver {
  template CopyMemoryFactory() {
    provides IMemoryManager;
    provides IRawMemory;
    provides IViewHistory;
  }
  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 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();
  }

  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 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_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]
            
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() {
    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[6], 0)
reify(watched-or({eq(pvw, 1),
                  eq(pvw, 2),
                  eq(pvw, 3),
                  eq(pvw, 4)}),
      pvw_provides[3])
eq(pvw_provides[1], 0)
reify(watched-or({eq(pvw, 2),
                  eq(pvw, 3),
                  eq(pvw, 4)}),
      pvw_provides[4])
eq(pvw_provides[5], 0)
eq(pvw_provides[2], 0)
            
check scA.param(2) accepts (pvw  +
    [(domainType, 'bound'),
     (domainSize, 1)]);
            
reifyimply(eq(pvw_properties[2], 1),
    scA_param_2_properties[2])
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_provides[6], 1),
    scA_param_2_provides[6])
reifyimply(eq(pvw_provides[3], 1),
    scA_param_2_provides[3])
            
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])

Questions?