1% BEGIN LICENSE BLOCK
2% Version: CMPL 1.1
3%
4% The contents of this file are subject to the Cisco-style Mozilla Public
5% License Version 1.1 (the "License"); you may not use this file except
6% in compliance with the License.  You may obtain a copy of the License
7% at www.eclipse-clp.org/license.
8%
9% Software distributed under the License is distributed on an "AS IS"
10% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied.  See
11% the License for the specific language governing rights and limitations
12% under the License.
13%
14% The Original Code is  The ECLiPSe Constraint Logic Programming System.
15% The Initial Developer of the Original Code is  Cisco Systems, Inc.
16% Portions created by the Initial Developer are
17% Copyright (C) 2006 Cisco Systems, Inc.  All Rights Reserved.
18%
19% Contributor(s):
20%
21% END LICENSE BLOCK
22% The Deussen Problem -------------------------------------------------------
23
24/*From mark@ecrc.de Tue Jul 14 11:05:16 1992
25
26I thought a propositional satisfiability example would be good.
27I therefore propose the Deussen problem Ulm027r1
28(chosen pretty well at random).
29
30Mark Wallace
31*/
32
33:- [bool]. % load in boolean ECH handler
34
35% the ulm027r1 problem has 16 solutions
36
37% no labeling
38deussen0(Vars) :-
39	ulm027r1(L,Vars),
40	solve_bools(L).
41
42% built-in labeling
43deussen1(Vars) :-
44	ulm027r1(L,Vars),
45	solve_bools(L),
46	labeling.
47
48% user-defined labeling
49deussen2(Vars) :-
50	ulm027r1(L,Vars),
51	solve_bools(L),
52	label_bool(Vars).
53
54  solve_bools([]).
55  solve_bools([X|L]) :-
56	solve_bool(X,1),	% boolean expression X must be 1 (true)
57	solve_bools(L).
58
59% Deussen Problem Ulm027/1
60
61ulm027r1(
62[
63U12 + U3 + U2,
64U12 + ~~U3 + ~~U2,
65~~U12 + ~~U3 + U2,
66~~U12 + U3 + ~~U2,
67U13 + U4 + U12,
68U13 + ~~U4 + ~~U12,
69~~U13 + ~~U4 + U12,
70~~U13 + U4 + ~~U12,
71U14 + U5 + U13,
72U14 + ~~U5 + ~~U13,
73~~U14 + ~~U5 + U13,
74~~U14 + U5 + ~~U13,
75~~U14,
76U15 + U6 + U4,
77U15 + ~~U6 + ~~U4,
78~~U15 + ~~U6 + U4,
79~~U15 + U6 + ~~U4,
80U16 + U2 + U15,
81U16 + ~~U2 + ~~U15,
82~~U16 + ~~U2 + U15,
83~~U16 + U2 + ~~U15,
84U17 + U2 + U16,
85U17 + ~~U2 + ~~U16,
86~~U17 + ~~U2 + U16,
87~~U17 + U2 + ~~U16,
88U18 + U6 + U17,
89U18 + ~~U6 + ~~U17,
90~~U18 + ~~U6 + U17,
91~~U18 + U6 + ~~U17,
92~~U18,
93U19 + U10 + U3,
94U19 + ~~U10 + ~~U3,
95~~U19 + ~~U10 + U3,
96~~U19 + U10 + ~~U3,
97U20 + U11 + U19,
98U20 + ~~U11 + ~~U19,
99~~U20 + ~~U11 + U19,
100~~U20 + U11 + ~~U19,
101U21 + U6 + U20,
102U21 + ~~U6 + ~~U20,
103~~U21 + ~~U6 + U20,
104~~U21 + U6 + ~~U20,
105U22 + U7 + U21,
106U22 + ~~U7 + ~~U21,
107~~U22 + ~~U7 + U21,
108~~U22 + U7 + ~~U21,
109~~U22,
110U23 + U5 + U7,
111U23 + ~~U5 + ~~U7,
112~~U23 + ~~U5 + U7,
113~~U23 + U5 + ~~U7,
114U24 + U6 + U23,
115U24 + ~~U6 + ~~U23,
116~~U24 + ~~U6 + U23,
117~~U24 + U6 + ~~U23,
118U25 + U10 + U24,
119U25 + ~~U10 + ~~U24,
120~~U25 + ~~U10 + U24,
121~~U25 + U10 + ~~U24,
122U26 + U11 + U25,
123U26 + ~~U11 + ~~U25,
124~~U26 + ~~U11 + U25,
125~~U26 + U11 + ~~U25,
126~~U26
127],
128[
129%U1,
130U2,U3,U4,U5,U6,U7,  %U8,U9,
131U10,U11,U12,U13,U14,U15,U16,U17,U18,U19,
132U20,U21,U22,U23,U24,U25,U26
133]).
134
135
136
137
138
139