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