1% thom fruehwirth ECRC 1991-1993 2% 910528 started boolean,and,or constraints 3% 910904 added exor,neg constraints 4% 911120 added imp constraint 5% 931110 ported to new release 6% 931111 added card constraint 7% 980701 converted to new chr format, Kish Shen 8 9:- lib(ech). 10 11:- handler bool. 12 13:- constraints boolean/1, and/3, or/3, exor/3, neg/2, imp/2, chr_labeling/0:at_lower(1). 14 15%:- nodbgcomp. %! 16 17:- option(check_guard_bindings, off). 18:- option(already_in_heads, off). 19 20 21boolean(0) <=> true. 22boolean(1) <=> true. 23 24chr_labeling, boolean(X) <=> label_boolean(X), chr_labeling. 25 26label_boolean(0). 27label_boolean(1). 28 29 30% and/3 specification 31%and(0,0,0). 32%and(0,1,0). 33%and(1,0,0). 34%and(1,1,1). 35 36and(0,X,Y) <=> Y=0. 37and(X,0,Y) <=> Y=0. 38and(1,X,Y) <=> Y=X. 39and(X,1,Y) <=> Y=X. 40and(X,Y,1) <=> X=1,Y=1. 41and(X,X,Z) <=> X=Z. 42%and(X,Y,X) <=> imp(X,Y). 43%and(X,Y,Y) <=> imp(Y,X). 44and(X,Y,A) \ and(X,Y,B) <=> A=B. 45and(X,Y,A) \ and(Y,X,B) <=> A=B. 46 47chr_labeling, and(A,B,C) <=> label_and(A,B,C), chr_labeling. 48 49label_and(0,X,0). 50label_and(1,X,X). 51%and(X,X,X). 52%and(X,Y,0):- neg(X,Y). 53 54 55% or/3 specification 56%or(0,0,0). 57%or(0,1,1). 58%or(1,0,1). 59%or(1,1,1). 60 61or(0,X,Y) <=> Y=X. 62or(X,0,Y) <=> Y=X. 63or(X,Y,0) <=> X=0,Y=0. 64or(1,X,Y) <=> Y=1. 65or(X,1,Y) <=> Y=1. 66or(X,X,Z) <=> X=Z. 67%or(X,Y,X) <=> imp(Y,X). 68%or(X,Y,Y) <=> imp(X,Y). 69or(X,Y,A) \ or(X,Y,B) <=> A=B. 70or(X,Y,A) \ or(Y,X,B) <=> A=B. 71 72chr_labeling, or(A,B,C) <=> label_or(A,B,C), chr_labeling. 73label_or(0,X,X). 74label_or(1,X,1). 75%or(X,X,X). 76%or(X,Y,1):- neg(X,Y). 77 78 79% exor/3 specification 80%exor(0,0,0). 81%exor(0,1,1). 82%exor(1,0,1). 83%exor(1,1,0). 84 85exor(0,X,Y) <=> X=Y. 86exor(X,0,Y) <=> X=Y. 87exor(X,Y,0) <=> X=Y. 88exor(1,X,Y) <=> neg(X,Y). 89exor(X,1,Y) <=> neg(X,Y). 90exor(X,Y,1) <=> neg(X,Y). 91exor(X,X,Y) <=> Y=0. 92exor(X,Y,X) <=> Y=0. 93exor(Y,X,X) <=> Y=0. 94exor(X,Y,A) \ exor(X,Y,B) <=> A=B. 95exor(X,Y,A) \ exor(Y,X,B) <=> A=B. 96 97chr_labeling, or(A,B,C) <=> label_exor(A,B,C), chr_labeling. 98label_exor(0,X,X). 99label_exor(1,X,Y):- neg(X,Y). 100%exor(X,X,0). 101%exor(X,Y,1):- neg(X,Y). 102 103 104% neg/2 specification 105%neg(0,1). 106%neg(1,0). 107 108neg(0,X) <=> X=1. 109neg(X,0) <=> X=1. 110neg(1,X) <=> X=0. 111neg(X,1) <=> X=0. 112neg(X,X) <=> fail. 113neg_neg ::= neg(X,Y) \ neg(Y,Z) <=> X=Z. 114neg_neg ::= neg(X,Y) \ neg(Z,Y) <=> X=Z. 115neg_neg ::= neg(Y,X) \ neg(Y,Z) <=> X=Z. 116% Interaction with other boolean constraints 117neg(X,Y) \ and(X,Y,Z) <=> Z=0. 118neg(Y,X) \ and(X,Y,Z) <=> Z=0. 119neg(X,Z) , and(X,Y,Z) <=> X=1,Y=0,Z=0. 120neg(Z,X) , and(X,Y,Z) <=> X=1,Y=0,Z=0. 121neg(Y,Z) , and(X,Y,Z) <=> X=0,Y=1,Z=0. 122neg(Z,Y) , and(X,Y,Z) <=> X=0,Y=1,Z=0. 123neg(X,Y) \ or(X,Y,Z) <=> Z=1. 124neg(Y,X) \ or(X,Y,Z) <=> Z=1. 125neg(X,Z) , or(X,Y,Z) <=> X=0,Y=1,Z=1. 126neg(Z,X) , or(X,Y,Z) <=> X=0,Y=1,Z=1. 127neg(Y,Z) , or(X,Y,Z) <=> X=1,Y=0,Z=1. 128neg(Z,Y) , or(X,Y,Z) <=> X=1,Y=0,Z=1. 129neg(X,Y) \ exor(X,Y,Z) <=> Z=1. 130neg(Y,X) \ exor(X,Y,Z) <=> Z=1. 131neg(X,Z) \ exor(X,Y,Z) <=> Y=1. 132neg(Z,X) \ exor(X,Y,Z) <=> Y=1. 133neg(Y,Z) \ exor(X,Y,Z) <=> X=1. 134neg(Z,Y) \ exor(X,Y,Z) <=> X=1. 135neg(X,Y) , imp(X,Y) <=> X=0,Y=1. 136neg(Y,X) , imp(X,Y) <=> X=0,Y=1. 137 138chr_labeling, neg(A,B) <=> label_neg(A,B), chr_labeling. 139label_neg(0,1). 140label_neg(1,0). 141 142 143% imp/2 specification 144%imp(0,0). 145%imp(0,1). 146%imp(1,1). 147 148imp(0,X) <=> true. 149imp(X,0) <=> X=0. 150imp(1,X) <=> X=1. 151imp(X,1) <=> true. 152imp(X,X) <=> true. 153imp(X,Y),imp(Y,X) <=> X=Y. 154 155chr_labeling, imp(A,B) <=> label_imp(A,B), chr_labeling. 156label_imp(0,X). 157label_imp(1,1). 158%imp(X,X). 159%imp(0,1). 160 161 162 163% Boolean cardinality operator 164% card(A,B,L,N) constrains list L of length N to have between A and B 1s 165 166:- constraints card/4. 167 168card(A,B,L):- 169 length(L,N), 170 A=<B,0=<B,A=<N,%0=<N % negariant of the constraint 171 card(A,B,L,N). 172 173% card/4 specification 174%card(A,B,[],0):- A=<0,0=<B. 175%card(A,B,[0|L],N):- 176% N1 is N-1, 177% card(A,B,L,N1). 178%card(A,B,[1|L],N):- 179% A1 is A-1, B1 is B-1, N1 is N-1, 180% card(A1,B1,L,N1). 181 182% Following operational specification from Pascal Van Hentenryck 183triv_sat ::= card(A,B,L,N) <=> A=<0,N=<B | true. % trivial satisfaction 184pos_sat ::= card(N,B,L,N) <=> set_to_ones(L). % positive satisfaction 185neg_sat ::= card(A,0,L,N) <=> set_to_zeros(L). % negative satisfaction 186pos_red ::= card(A,B,L,N) <=> delete(X,L,L1),X==1 | % positive reduction 187 A1 is A-1, B1 is B-1, N1 is N-1, 188 card(A1,B1,L1,N1). 189neg_red ::= card(A,B,L,N) <=> delete(X,L,L1),X==0 | % negative reduction 190 N1 is N-1, 191 card(A,B,L1,N1). 192% New special cases with two variables 193card2nand ::= card(0,1,[X,Y],2) <=> and(X,Y,0). 194card2neg ::= card(1,1,[X,Y],2) <=> neg(X,Y). 195card2or ::= card(1,2,[X,Y],2) <=> or(X,Y,1). 196 197chr_labeling, card(A,B,L,N) <=> label_car(A,B,L,N), chr_labeling. 198label_card(A,B,[],0):- A=<0,0=<B. 199label_card(A,B,[0|L],N):- 200 N1 is N-1, 201 label_card(A,B,L). 202label_card(A,B,[1|L],N):- 203 A1 is A-1, B1 is B-1, N1 is N-1, 204 label_card(A1,B1,L). 205 206 set_to_ones([]). 207 set_to_ones([1|L]):- 208 set_to_ones(L). 209 210 set_to_zeros([]). 211 set_to_zeros([0|L]):- 212 set_to_zeros(L). 213 214 215 216% Auxiliary predicates 217 218:- op(100,fy,(~~)). 219:- op(100,xfy,(#)). 220 221 solve_bool(A,C) :- var(A), !, A=C. 222 solve_bool(A,C) :- atomic(A), !, A=C. 223 solve_bool(A * B, C) ?- !, 224 solve_bool(A,A1), 225 solve_bool(B,B1), 226 and(A1,B1,C). 227 solve_bool(A + B, C) ?- !, 228 solve_bool(A,A1), 229 solve_bool(B,B1), 230 or(A1,B1,C). 231 solve_bool(A # B, C) ?- !, 232 solve_bool(A,A1), 233 solve_bool(B,B1), 234 exor(A1,B1,C). 235 solve_bool(~~A,C) ?- !, 236 solve_bool(A,A1), 237 neg(A1,C). 238 solve_bool(A -> B, C) ?- !, 239 solve_bool(A,A1), 240 solve_bool(B,B1), 241 imp(A1,B1),C=1. 242 solve_bool(A = B, C) ?- !, 243 solve_bool(A,A1), 244 solve_bool(B,B1), 245 A1=B1,C=1. 246 247 bool_portray(and(A,B,C),Out)?- !, Out = (A*B = C). 248 bool_portray(or(A,B,C),Out)?- !, Out = (A+B = C). 249 bool_portray(exor(A,B,C),Out)?- !, Out = (A#B = C). 250 bool_portray(neg(A,B),Out)?- !, Out = (A= ~~B). 251 bool_portray(imp(A,B),Out)?- !, Out = (A -> B). 252 bool_portray(card(A,B,L,N),Out)?- !, Out = card(A,B,L). 253 254 :- define_macro(type(compound),bool_portray/2,[write]). 255 256% Labeling 257 label_bool([]). 258 label_bool([X|L]) :- 259 (X=0;X=1), 260 label_bool(L). 261 262/* end of handler bool */ 263 264 265 266