From 0162250208e431e2a76ec64ceff4c28a796bf19b Mon Sep 17 00:00:00 2001 From: Koen van der Heijden Date: Tue, 13 Dec 2016 11:32:30 +0100 Subject: a is good. b is not --- packing_pallets_in_trucks/PackingPallets.java | 148 ++++++++++++-------------- 1 file 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(")))"); } -- cgit v1.2.1