Finished job scheduling

3 files changed, 84 insertions, 2 deletions

diff --git a/job_scheduling/JobScheduling.java b/job_scheduling/JobScheduling.java
new file mode 100644
index 0000000..ebe8d00
--- /dev/null
+++ b/job_scheduling/JobScheduling.java
@@ -0,0 +1,82 @@
+public class JobScheduling {
+
+    private static int NR_OF_JOBS = 12;
+
+    private static int MINIMIZE_A = 59;
+    private static int MINIMIZE_B = 65;
+
+    private static void assignmentA() {
+        System.out.println("(benchmark job_scheduling_a.smt");
+        System.out.println(":logic QF_UFLIA");
+        System.out.println(":extrafuns (");
+        print_predicates();
+        System.out.println(")");
+        System.out.println(":formula (and ");
+        print_formula(MINIMIZE_A);
+        System.out.println("))");
+    }
+
+    private static void assignmentB() {
+        System.out.println("(benchmark job_scheduling_b.smt");
+        System.out.println(":logic QF_UFLIA");
+        System.out.println(":extrafuns (");
+        print_predicates();
+        System.out.println(")");
+        System.out.println(":formula (and ");
+        print_formula(MINIMIZE_B);
+        print_formula_b();
+        System.out.println("))");
+    }
+
+    private static void print_predicates() {
+        for(int i = 1; i <= NR_OF_JOBS; i++) {
+            System.out.println("(j" + i + " Int)");
+        }
+    }
+
+    private static void print_formula(int minimize) {
+        for(int i = 1; i <= NR_OF_JOBS; i++) {
+            System.out.println("(<= (+ j" + i + " " + (i + 5) + ") " + minimize + ")");
+        }
+
+        for(int i = 1; i <= NR_OF_JOBS; i++) {
+            System.out.println("(>= j" + i + " 0)");
+        }
+        System.out.println("(and (>= j3 (+ j1 6)) (>= j3 (+ j2 7)))");
+        System.out.println("(and (>= j5 (+ j3 8)) (>= j5 (+ j4 9)))");
+        System.out.println("(and (>= j7 (+ j3 8)) (>= j7 (+ j4 9)) (>= j7 (+ j6 11)))");
+        System.out.println("(>= j8 j5)");
+        System.out.println("(and (>= j9 (+ j5 10)) (>= j9 (+ j8 13)))");
+        System.out.println("(>= j11 (+ j10 15))");
+        System.out.println("(and (>= j12 (+ j9 14)) (>= j12 (+ j11 16)))");
+
+        /* 5,7 and 10 resource thingy */
+        int[] smallset = {5, 7, 10};
+        for(int i : smallset) {
+            for(int j : smallset) {
+                if(i == j) continue;
+                System.out.println("(=> (<= j" + i + " j" + j + ") (<= (+ j" + i + " " + (i + 5) + ") j" + j + "))");
+            }
+        }
+    }
+
+    private static void print_formula_b() {
+        System.out.println("(>= j6 j12)");
+        System.out.println("(<= (+ j6 11) (+ j12 17))");
+    }
+
+    public static void main(String... args) {
+        assert(args.length > 0);
+        switch(args[0]) {
+            case "a":
+                assignmentA();
+                break;
+            case "b":
+                assignmentB();
+                break;
+            default:
+                System.err.println("Specify assignment a or b!");
+                break;
+        }
+    }
+}
diff --git a/job_scheduling/job_scheduling.z3 b/job_scheduling/job_scheduling.z3
deleted file mode 100644
index e69de29..0000000
--- a/job_scheduling/job_scheduling.z3
+++ /dev/null
diff --git a/packing_pallets_in_trucks/src/PackingPallets.java b/packing_pallets_in_trucks/PackingPallets.java
index baf850a..4c96cad 100644
--- a/packing_pallets_in_trucks/src/PackingPallets.java
+++ b/packing_pallets_in_trucks/PackingPallets.java
@@ -9,8 +9,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 = 14;
-    private static final int NR_OF_PRITTLES_B = 15;
+    private static final int NR_OF_PRITTLES_A = 32;
+    private static final int NR_OF_PRITTLES_B = 32;
     private static final int PRITTLES_WEIGHT = 400;
 
     private static final int NR_OF_SKIPPLES = 8;