refactoring: refactoring for models, improved scripts

jaantollander · jaantollander · commit 5eaa42b4f107 · 2021-12-04T14:55:54.000+02:00
diff --git a/models/fzn/4x4_opt.fzn b/models/fzn/4x4_opt.fzn
diff --git a/models/fzn/4x4_opt.txt b/models/fzn/4x4_opt.txt
@@ -0,0 +1,11 @@
+% Generated FlatZinc statistics:
+%%%mzn-stat: paths=1802
+%%%mzn-stat: flatBoolVars=946
+%%%mzn-stat: flatIntVars=125
+%%%mzn-stat: flatBoolConstraints=736
+%%%mzn-stat: flatIntConstraints=327
+%%%mzn-stat: evaluatedReifiedConstraints=210
+%%%mzn-stat: method="maximize"
+%%%mzn-stat: flatTime=0.324767
+%%%mzn-stat-end
+
diff --git a/models/fzn/5x5_opt.fzn b/models/fzn/5x5_opt.fzn
diff --git a/models/fzn/5x5_opt.txt b/models/fzn/5x5_opt.txt
@@ -0,0 +1,11 @@
+% Generated FlatZinc statistics:
+%%%mzn-stat: paths=3989
+%%%mzn-stat: flatBoolVars=2352
+%%%mzn-stat: flatIntVars=172
+%%%mzn-stat: flatBoolConstraints=1944
+%%%mzn-stat: flatIntConstraints=586
+%%%mzn-stat: evaluatedHalfReifiedConstraints=432
+%%%mzn-stat: method="maximize"
+%%%mzn-stat: flatTime=0.494101
+%%%mzn-stat-end
+
diff --git a/models/nxn_lock_pattern.mzn b/models/nxn_lock_pattern.mzn
@@ -1,5 +1,3 @@
-include "globals.mzn";
-
 % Define a two-dimensional nxn grid.
 int: n;
 int: m;
@@ -11,6 +9,10 @@ int: M;
 array[1..m] of var 1..m: p;
 constraint alldifferent(p);
 
+% Differences
+array[1..M] of var int: dx = [x[p[i]] - x[p[i+1]] | i in 1..M];
+array[1..M] of var int: dy = [y[p[i]] - y[p[i+1]] | i in 1..M];
+
 % Define permutations for symmetrical lock patterns
 array[1..m] of int: r90;
 array[1..m] of int: r180;
@@ -26,24 +28,3 @@ constraint symmetry_breaking_constraint(lex_lesseq(p, [p[i] | i in r180]));
 constraint symmetry_breaking_constraint(lex_lesseq(p, [p[i] | i in r180_reflect]));
 constraint symmetry_breaking_constraint(lex_lesseq(p, [p[i] | i in r270]));
 constraint symmetry_breaking_constraint(lex_lesseq(p, [p[i] | i in r270_reflect]));
-
-% Differences
-array[1..M] of var int: dx = [x[p[i]] - x[p[i+1]] | i in 1..M];
-array[1..M] of var int: dy = [y[p[i]] - y[p[i+1]] | i in 1..M];
-
-% Maximum complexity constraints.
-predicate line(int: x1, int: y1, int: k) = exists(i in 1..M, c in 1..k)(
-    (dx[i] = c*x1 /\ dy[i] = c*y1) \/ (dx[i] = -c*x1 /\ dy[i] = -c*y1)
-);
-
-% Line types
-int: N;
-array[1..N] of int: xs;
-array[1..N] of int: ys;
-array[1..N] of int: ks;
-
-constraint if N = M then
-    forall(i in 1..N)(line(xs[i], ys[i], ks[i]))
-else
-    count(i in 1..N)(line(xs[i], ys[i], ks[i])) = min(N, M)
-endif;
diff --git a/models/nxn_max_complexity.mzn b/models/nxn_max_complexity.mzn
@@ -0,0 +1,16 @@
+% Line types
+int: N;
+array[1..N] of int: xs;
+array[1..N] of int: ys;
+array[1..N] of int: ks;
+
+% Maximum complexity constraints.
+predicate line(int: x1, int: y1, int: k) = exists(i in 1..M, c in 1..k)(
+    (dx[i] = c*x1 /\ dy[i] = c*y1) \/ (dx[i] = -c*x1 /\ dy[i] = -c*y1)
+);
+
+constraint if N = M then
+    forall(i in 1..N)(line(xs[i], ys[i], ks[i]))
+else
+    count(i in 1..N)(line(xs[i], ys[i], ks[i])) = min(N, M)
+endif;
diff --git a/models/nxn_opt.mzn b/models/nxn_opt.mzn
@@ -1,4 +1,6 @@
-include "nxn_cons.mzn";
+include "globals.mzn";
+include "nxn_lock_pattern.mzn";
+include "nxn_max_complexity.mzn";
 
 % Maximize distance
 % TODO: add tight bounds for distance variable?
diff --git a/models/nxn_sat.mzn b/models/nxn_sat.mzn
@@ -1,4 +1,6 @@
-include "nxn_cons.mzn";
+include "globals.mzn";
+include "nxn_lock_pattern.mzn";
+include "nxn_max_complexity.mzn";
 
 % Find max complexity patterns
 solve satisfy;
diff --git a/scripts/2x2_sat.sh b/scripts/2x2_sat.sh
@@ -2,4 +2,5 @@
 minizinc models/nxn_sat.mzn models/instances/2x2.dzn \
     --solver gecode \
     --statistics \
-    --all-solutions
+    --all-solutions \
+    --output-time
diff --git a/scripts/3x3_sat.sh b/scripts/3x3_sat.sh
@@ -2,4 +2,5 @@
 minizinc models/nxn_sat.mzn models/instances/3x3.dzn \
     --solver gecode \
     --statistics \
-    --all-solutions
+    --all-solutions \
+    --output-time
diff --git a/scripts/4x4_opt.sh b/scripts/4x4_opt.sh
@@ -3,4 +3,5 @@ minizinc models/nxn_opt.mzn models/instances/4x4.dzn \
     --solver chuffed \
     --statistics \
     --all-solutions \
+    --output-time \
     --two-pass
diff --git a/scripts/4x4_opt_fzn.sh b/scripts/4x4_opt_fzn.sh
@@ -0,0 +1,7 @@
+#!/bin/bash
+minizinc models/nxn_opt.mzn models/instances/4x4.dzn \
+    --two-pass \
+    --fzn models/fzn/4x4_opt.fzn \
+    --compile \
+    --no-output-ozn \
+    --statistics > models/fzn/4x4_opt.txt
diff --git a/scripts/4x4_sat.sh b/scripts/4x4_sat.sh
@@ -3,4 +3,5 @@ minizinc models/nxn_sat.mzn models/instances/4x4.dzn \
     --solver chuffed \
     --statistics \
     --all-solutions \
+    --output-time \
     --two-pass
diff --git a/scripts/5x5_opt.sh b/scripts/5x5_opt.sh
@@ -0,0 +1,7 @@
+#!/bin/bash
+minizinc models/nxn_opt.mzn models/instances/5x5.dzn \
+    --solver chuffed \
+    --statistics \
+    --all-solutions \
+    --output-time \
+    --two-pass
diff --git a/scripts/5x5_opt_fzn.sh b/scripts/5x5_opt_fzn.sh
@@ -0,0 +1,7 @@
+#!/bin/bash
+minizinc models/nxn_opt.mzn models/instances/5x5.dzn \
+    --two-pass \
+    --fzn models/fzn/5x5_opt.fzn \
+    --compile \
+    --no-output-ozn \
+    --statistics > models/fzn/5x5_opt.txt
diff --git a/scripts/5x5_sat.sh b/scripts/5x5_sat.sh
@@ -3,4 +3,5 @@ minizinc models/nxn_sat.mzn models/instances/5x5.dzn \
     --solver chuffed \
     --statistics \
     --all-solutions \
+    --output-time \
     --two-pass
diff --git a/scripts/6x6_sat.sh b/scripts/6x6_sat.sh
@@ -3,4 +3,5 @@ minizinc models/nxn_sat.mzn models/instances/6x6.dzn \
     --solver chuffed \
     --statistics \
     --all-solutions \
+    --output-time \
     --two-pass
diff --git a/scripts/7x7_sat.sh b/scripts/7x7_sat.sh
@@ -3,4 +3,5 @@ minizinc models/nxn_sat.mzn models/instances/7x7.dzn \
     --solver chuffed \
     --statistics \
     --all-solutions \
+    --output-time \
     --two-pass
