this repo has no description
dekker.one
1% RUNS ON mzn20_fd
2% RUNS ON mzn-fzn_fd
3% RUNS ON mzn20_fd_linear
4% RUNS ON mzn20_mip
5%
6% SAT instance based on a DIMACS SAT problem generated by ./dimacs2minizinc.pl
7%
8% boolean variables
9array [1..3] of var bool : assignment;
10% formula
11array [1..21] of int: Formula = [ 1, 2, 3, 1, 2, -3, 1, -2, 3, 1, -2, -3, -1, 2, 3, -1, 2, -3, -1, -2, 3 ];
12
13%
14% constraints
15%
16
17% clause 1
18constraint (
19 ( ( Formula[1] > 0 ) == assignment[1] ) \/
20 ( ( Formula[2] > 0 ) == assignment[2] ) \/
21 ( ( Formula[3] > 0 ) == assignment[3] )
22);
23% clause 2
24constraint (
25 ( ( Formula[4] > 0 ) == assignment[1] ) \/
26 ( ( Formula[5] > 0 ) == assignment[2] ) \/
27 ( ( Formula[6] > 0 ) == assignment[3] )
28);
29% clause 3
30constraint (
31 ( ( Formula[7] > 0 ) == assignment[1] ) \/
32 ( ( Formula[8] > 0 ) == assignment[2] ) \/
33 ( ( Formula[9] > 0 ) == assignment[3] )
34);
35% clause 4
36constraint (
37 ( ( Formula[10] > 0 ) == assignment[1] ) \/
38 ( ( Formula[11] > 0 ) == assignment[2] ) \/
39 ( ( Formula[12] > 0 ) == assignment[3] )
40);
41% clause 5
42constraint (
43 ( ( Formula[13] > 0 ) == assignment[1] ) \/
44 ( ( Formula[14] > 0 ) == assignment[2] ) \/
45 ( ( Formula[15] > 0 ) == assignment[3] )
46);
47% clause 6
48constraint (
49 ( ( Formula[16] > 0 ) == assignment[1] ) \/
50 ( ( Formula[17] > 0 ) == assignment[2] ) \/
51 ( ( Formula[18] > 0 ) == assignment[3] )
52);
53% clause 7
54constraint (
55 ( ( Formula[19] > 0 ) == assignment[1] ) \/
56 ( ( Formula[20] > 0 ) == assignment[2] ) \/
57 ( ( Formula[21] > 0 ) == assignment[3] )
58);
59
60solve satisfy;
61
62output [
63 "simple sat: ",
64 show(assignment[1]), " ",
65 show(assignment[2]), " ",
66 show(assignment[3]), "\n"
67];