Skip to content
Permalink
Browse files

[PPDP19] Update the examples in preparation for the final version of …

…the paper. Add a BAB example.
  • Loading branch information...
ptal committed Jun 27, 2019
1 parent 0d5562c commit 8ac5b94c7bfaa431f30be098716ef0fdaa29b441
@@ -30,18 +30,19 @@
public static void main(String[] args) {
PPDP19 demo = new PPDP19();
demo.beginMessage();
demo.section3BoundedDepth();
demo.section5CSP();
demo.section5LDS();
demo.section5LDS_IDS();
demo.section4BoundedDepth();
demo.section6CSP();
demo.section6BAB();
demo.section6LDS();
demo.section6LDS_IDS();
demo.endMessage();
}

// The code is slightly different than in the paper (which is simplified for clarity).
// We must initialize the field "limit" of the class "BoundedTree" outside of the constructor.
// The interface with "SpaceMachine" takes the module creating the program, and the process constructor separately.
void section3BoundedDepth() {
System.out.println("\n Section 3. Demo of iterative deepening search (IDS).");
void section4BoundedDepth() {
System.out.println("\n Section 4. Demo of iterative deepening search (IDS).");
System.out.println(" =========\n");

for(int limit = 0; limit < 3; limit++) {
@@ -54,20 +55,30 @@ void section3BoundedDepth() {
}
}

// We illustrate the section 5.1 with the NQueen CSP.
void section5CSP() {
System.out.println("\n Section 5.1. Demo of CSP state space exploration (3 first solutions of the 8-Queens problem).");
// We illustrate the section 6.1 with the NQueen CSP.
void section6CSP() {
System.out.println("\n Section 6.1. Demo of CSP state space exploration (3 first solutions of the 8-Queens problem).");
System.out.println(" ===========\n");
Solver solver = new Solver();
SolveNQueens solver = new SolveNQueens();
StackLR queue = new StackLR();
SpaceMachine<Solver> machine = new SpaceMachine<>(solver, (p) -> p.nqueens(), queue);
SpaceMachine<SolveNQueens> machine = new SpaceMachine<>(solver, (p) -> p.nqueens(), queue);
for(int i = 0; i < 3; i++) {
machine.execute();
}
}

void section5LDS() {
System.out.println("\n Section 5.2. Demo of limited-discrepancy search (LDS).");
// We illustrate the branch and bound algorithm of section 6.2 with the Golomb ruler CSP.
void section6BAB() {
System.out.println("\n Section 6.2. Demo of Branch and Bound algorithm (intermediate and best solution of the Golomb Ruler problem of size 10).");
System.out.println(" ===========\n");
SolveBAB solver = new SolveBAB();
StackLR queue = new StackLR();
SpaceMachine<SolveBAB> machine = new SpaceMachine<>(solver, (p) -> p.solve(), queue);
machine.execute();
}

void section6LDS() {
System.out.println("\n Section 6.3. Demo of limited-discrepancy search (LDS).");
System.out.println(" ===========\n");

for(int limit = 0; limit < 3; limit++) {
@@ -80,8 +91,8 @@ void section5LDS() {
}
}

void section5LDS_IDS() {
System.out.println("\n Section 5.3. Demo of LDS+IDS.");
void section6LDS_IDS() {
System.out.println("\n Section 6.3. Demo of LDS+IDS.");
System.out.println(" ===========\n");

for(int limit = 0; limit < 3; limit++) {
@@ -29,29 +29,15 @@

public class Solver
{
single_time ES consistent = unknown;
public world_line VarStore domains = new VarStore();
public world_line ConstraintStore constraints = new ConstraintStore();
single_space ArrayList<IntVar> queens = new ArrayList();

public proc nqueens =
modelNQueens(8, write queens, write domains, write constraints);
run search_one_sol()
end

public proc search_one_sol =
par
<> run search()
<> loop
when consistent |= true then
when true |= consistent then
printSolution(queens);
stop;
else pause end
else pause end
end
end
end
public ref single_time ES consistent;
public ref world_line VarStore domains;
public ref world_line ConstraintStore constraints;

public Solver(VarStore domains, ConstraintStore constraints, ES consistent) {
this.domains = domains;
this.constraints = constraints;
this.consistent = consistent;
}

public proc search = par run propagation() <> run branch() end

@@ -61,7 +47,7 @@ run search_one_sol()
end

proc branch =
single_space VariableSelector<IntVar> var = firstFail(domains);
single_space VariableSelector<IntVar> var = firstFail(write domains);
single_space IntValueSelector val = middle();
flow
when unknown |= consistent then
@@ -73,6 +59,22 @@ run search_one_sol()
end
end
// This strategy is to illustrate Golomb Ruler with BAB.
public proc searchInputOrderLB = par run propagation() <> run branchInputOrderLB() end
proc branchInputOrderLB =
single_space VariableSelector<IntVar> var = inputOrder(write domains);
single_space IntValueSelector val = min();
flow
when unknown |= consistent then
single_time IntVar x = readwrite var.getVariable(domains.vars());
single_time Integer v = readwrite val.selectValue(x);
space readwrite domains.join_eq(x, v) end;
space readwrite domains.join_neq(x, v) end
end
end
end
private VariableSelector<IntVar> firstFail(VarStore domains) {
return new FirstFail(domains.model());
}
@@ -81,6 +83,14 @@ private IntValueSelector middle() {
return new IntDomainMiddle(true);
}
private VariableSelector<IntVar> inputOrder(VarStore domains) {
return new InputOrder(domains.model());
}
private IntValueSelector min() {
return new IntDomainMin();
}
// Interface to the Choco solver.
private IntVar failFirstVar(VariableSelector<IntVar> var, VarStore domains) {
return var.getVariable(domains.vars());
@@ -89,30 +99,4 @@ private IntVar failFirstVar(VariableSelector<IntVar> var, VarStore domains) {
private Integer middleValue(IntValueSelector val, IntVar x) {
return val.selectValue(x);
}
private void modelNQueens(int n, ArrayList<IntVar> queens, VarStore domains,
ConstraintStore constraints)
{
IntVar[] vars = new IntVar[n];
IntVar[] diag1 = new IntVar[n];
IntVar[] diag2 = new IntVar[n];
for(int i = 0; i < n; i++) {
vars[i] = (IntVar) domains.alloc(new VarStore.IntDomain(1, n, false));
diag1[i] = domains.model().intOffsetView(vars[i], i);
diag2[i] = domains.model().intOffsetView(vars[i], -i);
}
constraints.join_in_place(new AllDifferent(vars, "BC"));
constraints.join_in_place(new AllDifferent(diag1, "BC"));
constraints.join_in_place(new AllDifferent(diag2, "BC"));
for(IntVar v : vars) { queens.add(v); }
}
private void printSolution(ArrayList<IntVar> queens) {
System.out.print("solution: [");
for (IntVar v : queens) {
System.out.print(v.getValue() + ",");
}
System.out.println("]");
}
}
@@ -58,7 +58,9 @@ flow yield_objective() =

public static ES updateBound(VarStore _domains, IntVar x, LMax obj) {
try {
x.updateLowerBound(obj.unwrap() + 1, Cause.Null);
if (!obj.isBottom()) {
x.updateLowerBound(obj.unwrap() + 1, Cause.Null);
}
return new ES(Kleene.UNKNOWN);
}
catch (ContradictionException c) {
@@ -58,7 +58,9 @@ flow yield_objective() =

public static ES updateBound(VarStore _domains, IntVar x, LMin obj) {
try {
x.updateUpperBound(obj.unwrap() - 1, Cause.Null);
if (!obj.isBottom()) {
x.updateUpperBound(obj.unwrap() - 1, Cause.Null);
}
return new ES(Kleene.UNKNOWN);
}
catch (ContradictionException c) {
@@ -18,8 +18,11 @@

public class LMax extends TotalOrder<Integer>
{
static Integer BOT = Integer.MIN_VALUE;
static Integer TOP = Integer.MAX_VALUE;

public LMax() {
super(new Integer(0));
super(BOT);
}

public LMax(Integer v) {
@@ -31,11 +34,19 @@ public LMax(LMax m) {
}

public LMax bottom() {
return new LMax(Integer.MIN_VALUE);
return new LMax(BOT);
}

public LMax top() {
return new LMax(Integer.MAX_VALUE);
return new LMax(TOP);
}

public boolean isBottom() {
return value == BOT;
}

public boolean isTop() {
return value == TOP;
}

// Access: READWRITE(this)
@@ -18,8 +18,11 @@

public class LMin extends TotalOrder<Integer>
{
static Integer BOT = Integer.MAX_VALUE;
static Integer TOP = Integer.MIN_VALUE;

public LMin() {
super(new Integer(0));
super(BOT);
}

public LMin(Integer v) {
@@ -31,11 +34,19 @@ private LMin(LMin m) {
}

public LMin bottom() {
return new LMin(Integer.MAX_VALUE);
return new LMin(BOT);
}

public LMin top() {
return new LMin(Integer.MIN_VALUE);
return new LMin(TOP);
}

public boolean isBottom() {
return value == BOT;
}

public boolean isTop() {
return value == TOP;
}

// Access: READWRITE(this)
@@ -4,6 +4,6 @@ cargo install --force --path .
cd runtime/
./install.sh
cd ..
# cd libstd/
# ./install.sh
# cd ..
cd libstd/
./install.sh
cd ..

0 comments on commit 8ac5b94

Please sign in to comment.
You can’t perform that action at this time.