summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorKoen van der Heijden <koen.vd.heijden1@gmail.com>2016-12-13 11:32:30 +0100
committerKoen van der Heijden <koen.vd.heijden1@gmail.com>2016-12-13 11:32:30 +0100
commit0162250208e431e2a76ec64ceff4c28a796bf19b (patch)
tree57d1a4e54f72990e8a57cbc64fd2877719b353a8
parent7269acd9fbc6c20d4961ce6a5851bfee3a41cb4a (diff)
download2IMF25-AR-0162250208e431e2a76ec64ceff4c28a796bf19b.tar.gz
a is good. b is not
-rw-r--r--packing_pallets_in_trucks/PackingPallets.java148
1 files changed, 71 insertions, 77 deletions
diff --git a/packing_pallets_in_trucks/PackingPallets.java b/packing_pallets_in_trucks/PackingPallets.java
index c2cceda..ca790d8 100644
--- a/packing_pallets_in_trucks/PackingPallets.java
+++ b/packing_pallets_in_trucks/PackingPallets.java
@@ -8,8 +8,8 @@ public class PackingPallets {
private static final int NR_OF_NUZZLES = 4;
private static final int NUZZLES_WEIGHT = 700;
- private static final int NR_OF_PRITTLES_A = 32;
- private static final int NR_OF_PRITTLES_B = 32;
+ private static final int NR_OF_PRITTLES_A = 22;
+ private static final int NR_OF_PRITTLES_B = 19;
private static final int PRITTLES_WEIGHT = 400;
private static final int NR_OF_SKIPPLES = 8;
@@ -21,13 +21,19 @@ public class PackingPallets {
private static final int NR_OF_DUPPLES = 20;
private static final int DUPPLES_WEIGHT = 200;
+ private static final int OFFSET_NUZZLES = 0;
+ private static final int OFFSET_SKIPPLES = OFFSET_NUZZLES + NR_OF_NUZZLES;
+ private static final int OFFSET_CROTTLES = OFFSET_SKIPPLES + NR_OF_SKIPPLES;
+ private static final int OFFSET_DUPPLES = OFFSET_CROTTLES + NR_OF_CROTTLES;
+ private static final int OFFSET_PRITTLES = OFFSET_DUPPLES + NR_OF_DUPPLES;
+
private static void assignmentA() {
System.out.println("(benchmark packing_pallets_a.smt");
System.out.println(":logic QF_UFLIA");
System.out.println(":extrafuns (");
print_predicates(NR_OF_PRITTLES_A);
System.out.println(")");
- System.out.print(":formula (");
+ System.out.print(":formula (and ");
print_formula(NR_OF_PRITTLES_A);
System.out.println("))");
}
@@ -38,134 +44,122 @@ public class PackingPallets {
System.out.println(":extrafuns (");
print_predicates(NR_OF_PRITTLES_B);
System.out.println(")");
- System.out.print(":formula (");
+ System.out.print(":formula (and ");
print_formula(NR_OF_PRITTLES_B);
print_formula_b(NR_OF_PRITTLES_B);
System.out.println("))");
}
private static void print_predicates(int prittles) {
- for(int i = 1; i <= NR_OF_NUZZLES; i++) {
- System.out.print("(n" + i + " Int) ");
- }
- System.out.println();
- for(int i = 1; i <= prittles; i++) {
- System.out.print("(p" + i + " Int) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_SKIPPLES; i++) {
- System.out.print("(s" + i + " Int) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_CROTTLES; i++) {
- System.out.print("(c" + i + " Int) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_DUPPLES; i++) {
- System.out.print("(d" + i + " Int) ");
- }
- System.out.println();
+ System.out.print("(N Int Int) ");
+ System.out.print("(Ns Int Int) ");
+ System.out.print("(P Int Int) ");
+ System.out.print("(Ps Int Int) ");
+ System.out.print("(S Int Int) ");
+ System.out.print("(Ss Int Int) ");
+ System.out.print("(C Int Int) ");
+ System.out.print("(Cs Int Int) ");
+ System.out.print("(D Int Int) ");
+ System.out.print("(Ds Int Int) ");
+ System.out.print("(Trucks Int Int Int) ");
+ System.out.print("(Weight Int Int)");
}
private static void print_formula(int prittles) {
/* valid truck assignment */
- System.out.println("and ");
+ System.out.println("(<= " + (NR_OF_NUZZLES + prittles + NR_OF_SKIPPLES + NR_OF_CROTTLES + NR_OF_DUPPLES) + " " + (NR_OF_TRUCKS * TRUCK_PALLET_CAPACITY) + ")");
for(int i = 1; i <= NR_OF_NUZZLES; i++) {
- System.out.print("(<= n" + i + " " + NR_OF_TRUCKS +") (> n" + i + " 0) ");
+ System.out.print("(<= (N " + i + ") " + NR_OF_TRUCKS +") (> (N " + i + ") 0) ");
+ System.out.print("(<= (Ns " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Ns " + i + ") 0) ");
+ System.out.print("(= (Weight " + (OFFSET_NUZZLES + i) + ") " + NUZZLES_WEIGHT + ")");
}
System.out.println();
for(int i = 1; i <= prittles; i++) {
- System.out.print("(<= p" + i + " " + NR_OF_TRUCKS +") (> p" + i + " 0) ");
+ System.out.print("(<= (P " + i + ") " + NR_OF_TRUCKS +") (> (P " + i + ") 0) ");
+ System.out.print("(<= (Ps " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Ps " + i + ") 0) ");
+ System.out.print("(= (Weight " + (OFFSET_PRITTLES + i) + ") " + PRITTLES_WEIGHT + ")");
}
System.out.println();
for(int i = 1; i <= NR_OF_SKIPPLES; i++) {
- System.out.print("(<= s" + i + " " + NR_OF_COOLING_TRUCKS +") (> s" + i + " 0) ");
+ System.out.print("(<= (S " + i + ") " + NR_OF_COOLING_TRUCKS +") (> (S " + i + ") 0) ");
+ System.out.print("(<= (Ss " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Ss " + i + ") 0) ");
+ System.out.print("(= (Weight " + (OFFSET_SKIPPLES + i) + ") " + SKIPPLES_WEIGHT + ")");
}
System.out.println();
for(int i = 1; i <= NR_OF_CROTTLES; i++) {
- System.out.print("(<= c" + i + " " + NR_OF_TRUCKS +") (> c" + i + " 0) ");
+ System.out.print("(<= (C " + i + ") " + NR_OF_TRUCKS +") (> (C " + i + ") 0) ");
+ System.out.print("(<= (Cs " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Cs " + i + ") 0) ");
+ System.out.print("(= (Weight " + (OFFSET_CROTTLES + i) + ") " + CROTTLES_WEIGHT + ")");
}
System.out.println();
for(int i = 1; i <= NR_OF_DUPPLES; i++) {
- System.out.print("(<= d" + i + " " + NR_OF_TRUCKS +") (> d" + i + " 0) ");
+ System.out.print("(<= (D " + i + ") " + NR_OF_TRUCKS +") (> (D " + i + ") 0) ");
+ System.out.print("(<= (Ds " + i + ") " + TRUCK_PALLET_CAPACITY +") (> (Ds " + i + ") 0) ");
+ System.out.print("(= (Weight " + (OFFSET_DUPPLES + i) + ") " + DUPPLES_WEIGHT + ")");
}
System.out.println();
/* assignment constraints */
for(int j = 1; j <= NR_OF_TRUCKS; j++) {
- System.out.println("(< (+ ");
- for(int i = 1; i <= NR_OF_NUZZLES; i++) {
- System.out.print("(ite (= n" + i + " " + j + ") " + NUZZLES_WEIGHT + " 0)" );
- }
- System.out.println();
- for(int i = 1; i <= prittles; i++) {
- System.out.print("(ite (= p" + i + " " + j + ") " + PRITTLES_WEIGHT + " 0) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_SKIPPLES; i++) {
- System.out.print("(ite (= s" + i + " " + j + ") " + SKIPPLES_WEIGHT + " 0) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_CROTTLES; i++) {
- System.out.print("(ite (= c" + i + " " + j + ") " + CROTTLES_WEIGHT + " 0) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_DUPPLES; i++) {
- System.out.print("(ite (= d" + i + " " + j + ") " + DUPPLES_WEIGHT + " 0) ");
+ System.out.println("(<= (+ ");
+ for (int i = 1; i <= TRUCK_PALLET_CAPACITY; i++) {
+ System.out.print("(Weight (Trucks " + j + " " + i + "))");
}
System.out.println(") " + TRUCK_CAPACITY + ")");
}
- for(int j = 1; j <= NR_OF_TRUCKS; j++) {
- System.out.println("(< (+ ");
- for(int i = 1; i <= NR_OF_NUZZLES; i++) {
- System.out.print("(ite (= n" + i + " " + j + ") 1 0) ");
- }
- System.out.println();
- for(int i = 1; i <= prittles; i++) {
- System.out.print("(ite (= p" + i + " " + j + ") 1 0) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_SKIPPLES; i++) {
- System.out.print("(ite (= s" + i + " " + j + ") 1 0) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_CROTTLES; i++) {
- System.out.print("(ite (= c" + i + " " + j + ") 1 0) ");
- }
- System.out.println();
- for(int i = 1; i <= NR_OF_DUPPLES; i++) {
- System.out.print("(ite (= d" + i + " " + j + ") 1 0) ");
+ for(int i = 1; i <= NR_OF_TRUCKS; i++) {
+ for(int j = 1; j <= TRUCK_PALLET_CAPACITY; j++) {
+ System.out.println("(<= (Trucks " + i + " " + j + ") " + (OFFSET_PRITTLES + prittles) + ")");
+ System.out.println("(>= (Trucks " + i + " " + j + ") 0)");
}
- System.out.println(") " + TRUCK_PALLET_CAPACITY + ")");
}
+ System.out.println("(= (Weight 0) 0)");
+ /**** NEEDS REWRITING ****/
for(int i = 1; i <= NR_OF_NUZZLES; i++) {
- for(int j = i + 1; j <= NR_OF_NUZZLES; j++ ) {
- System.out.println("(not (= n" + i + " n" + j +"))");
- }
+ System.out.println("(= (Trucks (N " + i + ") (Ns " + i + ")) " + (OFFSET_NUZZLES + i) + ") ");
}
+ for(int i = 1; i <= prittles; i++) {
+ System.out.println("(= (Trucks (P " + i + ") (Ps " + i + ")) " + (OFFSET_PRITTLES + i) + ") ");
+ }
+ for (int i = 1; i <= NR_OF_SKIPPLES; i++) {
+ System.out.println("(= (Trucks (S " + i + ") (Ss " + i + ")) " + (OFFSET_SKIPPLES + i) + ") ");
+ }
+ for (int i = 1; i <= NR_OF_CROTTLES; i++) {
+ System.out.println("(= (Trucks (C " + i + ") (Cs " + i + ")) " + (OFFSET_CROTTLES + i) + ") ");
+ }
+ for (int i = 1; i <= NR_OF_DUPPLES; i++) {
+ System.out.println("(= (Trucks (D " + i + ") (Ds " + i + ")) " + (OFFSET_DUPPLES + i) + ") ");
+ }
+ /**** NEEDS REWRITING ****/
+
+ System.out.print("(distinct");
+ for(int i = 1; i <= NR_OF_NUZZLES; i++) {
+ System.out.print(" (N " + i + ")");
+ }
+ System.out.println(")");
}
private static void print_formula_b(int prittles) {
for(int i = 1; i <= NR_OF_TRUCKS; i++) {
System.out.print("(=> (or ");
for(int j = 1; j <= prittles; j++) {
- System.out.print("(= p" + j + " " + i + ") ");
+ System.out.print("(= (P " + j + ") " + i + ") ");
}
System.out.print(") (not (or ");
for(int j = 1; j <= NR_OF_CROTTLES; j++) {
- System.out.print("(= c" + j + " " + i + ") ");
+ System.out.print("(= (C " + j + ") " + i + ") ");
}
System.out.println(")))");
System.out.print("(=> (or ");
for(int j = 1; j <= NR_OF_CROTTLES; j++) {
- System.out.print("(= c" + j + " " + i + ") ");
+ System.out.print("(= (C " + j + ") " + i + ") ");
}
System.out.print(") (not (or ");
for(int j = 1; j <= prittles; j++) {
- System.out.print("(= p" + j + " " + i + ") ");
+ System.out.print("(= (P " + j + ") " + i + ") ");
}
System.out.println(")))");
}