1:- module(xcnf, []). 2 3:- use_module(library(apply)). 4:- use_module(library(apply_macros)). 5:- use_module(pac(basic)). 6:- use_module(pac(meta)). 7:- use_module(util(misc)). 8:- use_module(zdd('zdd-array')). 9:- use_module(zdd(zdd)). 10:- use_module(pac(op)). 11 12 /************************ 13 * Sample Queries * 14 ************************/ 15 16% ?- N = 2, formula(1, N, _P), K is N + 1, conj(1, N, _Q), 17% time(((seq_zdd set_compare(xcnf:prop_compare), xprove(_P*_Q -> N)))). 18%@ % 5,142 inferences, 0.000 CPU in 0.001 seconds (84% CPU, 10602062 Lips) 19%@ N = 2, 20%@ K = 3. 21 22% ?- N = 100, formula(1, N, _P), K is N + 1, conj(1, N, _Q), 23% time(((seq_zdd set_compare(xcnf:prop_compare), xcnf(-(_P*_Q -> N), X), 24% card(X, Card), 25% zmod:resolve(X)))). 26%@ % 260,671,070 inferences, 29.291 CPU in 30.654 seconds (96% CPU, 8899206 Lips) 27%@ N = 100, 28%@ K = 101, 29%@ X = 2936449, 30%@ Card = 633825300114114700748351602789. 31 32 33% ?- N = 200, formula(1, N, _P), K is N + 1, conj(1, N, _Q), 34% time(((seq_zdd set_compare(xcnf:prop_compare), xcnf(_P*_Q, X)))). 35%@ % 2,064,194,409 inferences, 256.793 CPU in 270.204 seconds (95% CPU, 8038374 Lips) 36%@ N = 200, 37%@ K = 201, 38%@ X = 23082645. 39 40% ?- N = 3, formula(1, N, _P), K is N + 1, conj(1, N, _Q), 41% time(((seq_zdd set_compare(xcnf:prop_compare), xcnf(-(_P*_Q), X)))). 42% ?- seq_zdd set_compare(xcnf:prop_compare), xcnf(a*b, X). 43% ?- seq_zdd set_compare(xcnf:prop_compare), xcnf(-a, X). 44 45% ?- N = 100, formula(1, N, _P), K is N + 1, conj(1, N, _Q), 46% call_with_time_limit(360, time(zmod:prove((_P*_Q -> N)))). 47%@ % 553,415,627 inferences, 232.509 CPU in 368.663 seconds (63% CPU, 2380187 Lips) 48%@ ERROR: Unhandled exception: Time limit exceeded 49 50% ?- prop_compare(C, a, -a). 51% ?- prop_compare(C, -(a), a). 52% ?- prop_compare(C, -(b), a). 53% ?- prop_compare(C, -(a), b). 54% ?- prop_compare(C, -(a), -(b)). 55% ?- prop_compare(C, -(a), -(a)). 56% ?- prop_compare(C, -(a), ->(b,c)). 57% ?- prop_compare(C, ->(a,b), -b). 58% ?- prop_compare(C, -(->(a,b)), ->(-(a),-(a))). 59% ?- predsort(prop_compare, [a,b], X). 60% ?- predsort(prop_compare, [a,b,a], X). 61% ?- predsort(prop_compare, [a,-b,a->b], X). 62% ?- predsort(prop_compare, [-a,a,a->b], X). 63% ?- predsort(prop_compare, [-(a->b), a->b], X). 64% ?- predsort(prop_compare, [a*b, a+b, -(a->b), a->b], X). 65%@ X = [(a->b), a+b, a*b, - (a->b)]. 66 67% ?- seq_zdd zdd_sort([c, a,b,c], X). 68% ?- seq_zdd X<<{[a]}, psa(X). 69% ?- seq_zdd X<<{[a*b, a->b], [-b]}, psa(X), resolve(X). 70% ?- seq_zdd X<<{[a*b, a->b], [-b]}, psa(X), 71% ?- seq_zdd X<<{[a * (a->b)], [-b]}, psa(X), 72% seq:resolve(X). 73% ?- seq_zdd X<<{[a*b*(a->c)], [-c]}, psa(X), 74% ?- seq_zdd X<<{[a*b*(a->c)*(b->c)], [-c]}, resolve(X). 75% ?- seq_zdd X<<{[a*(a->b)], [-b]}, resolve(X). 76% ?- seq_zdd X<<{[a], [a->b], [a-> -b], [b]}, resolve(X). 77% ?- seq_zdd X<<{[a*b], [a->c], [b->c], [-c]}, resolve(X). 78% ?- seq_zdd X<<{[(a->b)->c], [-c]}, resolve(X). 79% ?- seq_zdd X << {}, psa(X), resolve(X). 80% ?- seq_zdd X << {[]}, psa(X), resolve(X). 81% ?- seq_zdd X << {[a]}, psa(X), resolve(X). 82% ?- seq_zdd X << {[a], [b], [-a, -b]}, psa(X), resolve(X). 83% ?- seq_zdd X << {[a->b], [a], [-b]}, psa(X), resolve(X). 84% ?- seq_zdd X << {[a*b->c], [a*b], [-c]}, psa(X), resolve(X). 85% ?- seq_zdd X << {[a==(b==c)], [a], [b], [-c]}, psa(X), resolve(X). 86% ?- seq_zdd X << {[a==(b==c)], [a], [b], [c]}, psa(X), resolve(X). 87% ?- seq_zdd X << {[1==(2==3)], [1], [2], [-(3)]}, psa(X), resolve(X). 88 89% ?- formula(1, 1, P). 90% ?- formula(1, 2, P). 91% ?- formula(1, 3, P). 92 93% ?- formula(1, 3, F). 94%@ F = (1==(2==(3==4))). 95formula(I, I, I==J):-!, J is I+1. 96formula(I, J, I==P):- K is I + 1, formula(K, J, P). 97 98% ?- conj(1, 3, P). 99%@ P = 1*(2*3). 100conj(I, I, I):-!. 101conj(I, J, I*P):- I0 is I + 1, conj(I0, J, P). 102 103:-op(1150, fy, seq_zdd). 104 105:-meta_predicate seq_zdd(). 106seq_zdd(X):- zdd((set_compare(xcnf:prop_compare), seq:X)).
xor(a,b) < a->b < a < -a < b < -b.116prop_compare(=, X, X):-!. 117prop_compare(C, ==(X, Y), ==(U, V)):-!, prop_compare(C, X, Y, U, V). 118prop_compare(C, ->(X, Y), ->(U, V)):-!, prop_compare(C, X, Y, U, V). 119prop_compare(C, +(X, Y), +(U, V)):-!, prop_compare(C, X, Y, U, V). 120prop_compare(C, *(X, Y), *(U, V)):-!, prop_compare(C, X, Y, U, V). 121prop_compare(C, xor(X, Y), xor(U, V)):-!, prop_compare(C, X, Y, U, V). 122prop_compare(<, +(_, _), _) :-!. 123prop_compare(>, _, +(_, _)) :-!. 124prop_compare(<, *(_, _), _) :-!. 125prop_compare(>, _, *(_, _)) :-!. 126prop_compare(<, ==(_, _), _):-!. 127prop_compare(>, _, ==(_, _)):-!. 128prop_compare(<, xor(_, _), _):-!. 129prop_compare(>, _, xor(_, _)):-!. 130prop_compare(<, ->(_, _), _):-!. 131prop_compare(>, _, ->(_, _)):-!. 132prop_compare(C, -(X), -(Y)) :-!, prop_compare(C, X, Y). 133prop_compare(C, X, -(Y)) :-!, 134 ( X = Y -> C = (<) 135 ; prop_compare(C, X, Y) 136 ). 137prop_compare(C, -(X), Y):-!, 138 ( X = Y -> C = (>) 139 ; prop_compare(C, X, Y) 140 ). 141prop_compare(C, X, Y):- compare(C, X, Y). 142 143% 144prop_compare(C, X, Y, U, V):- 145 prop_compare(C0, X, U), 146 ( C0 = (=) -> prop_compare(C, Y, V) 147 ; C = C0 148 ). 149 150% ?- zdd {prop_compare(C, a, b)}. 151% ?- zdd {prop_compare(C, -a, a)}. 152% ?- zdd {prop_compare(C, a, -a)}. 153% ?- zdd {prop_compare(C, -a, b)}. 154prop_compare(C, X, Y, S):- get_compare(F, S), 155 call(F, C, X, Y).
160% ?- seq_zdd prop_sort([-b, a*b, b,-b,(a+b), (a->b),-a], X). 161%@ X = [(a->b), a+b, a*b, -a, b, -b]. 162 163% 164xprove(X):- seq_zdd((xcnf(-X, Y), zmod:resolve(Y))). 165 166xprove(X, S):- xcnf(-X, Y, S), zmod:resolve(Y, S). 167 168% ?- xprove(a*(a->b)->b). 169% ?- seq_zdd xcnf((a+b)*c, X), psa(X). 170% ?- seq_zdd xcnf(-((a+b)*c), X), psa(X). 171% ?- predsort(prop_compare, [-c, -(a*b)], R). 172% ?- seq_zdd zdd_ord_insert([-(a*b), -c], 1, X), psa(X). 173% ?- seq_zdd xcnf(-((a+b)*(b+c)), X), psa(X). 174% ?- seq_zdd xcnf(-(a*(b+c)), X), psa(X). 175% ?- seq_zdd xcnf(-((a+b)*(c+d)), X), psa(X). 176% ?- seq_zdd xcnf(-a* a, X), psa(X). 177% ?- seq_zdd xcnf(-a, X), psa(X). 178 179xcnf(X, Y, S):- zdd_singleton(X, X0, S), 180 once(expand_cnf(X0, Y, S)). 181% 182expand_cnf(0, 0, _):-!. 183expand_cnf(1, 1, _):-!. 184expand_cnf(X, Y, S):- % memo useless here. 185 cofact(X, t(A, L, R), S), 186 expand_cnf(A, L, R, X, Y, S). 187% 188expand_cnf(A, L, R, X, Y, S):- 189 ( xliteral(A) -> Y = X 190 ; expand_cnf(A, R, R0, S), 191 ltr_join(L, R0, Y0, S), 192 expand_cnf(Y0, Y, S) 193 ). 194 195% ?- xliteral(-a). 196% ?- xliteral(-(-a)). 197xliteral(-(A)):-!, \+xprop(A). 198xliteral(A):- \+xprop(A). 199% 200xprop(_+_). 201xprop(_*_). 202xprop(_->_). 203xprop(_==_). 204xprop(xor(_,_)). 205xprop(-(_)). 206% 207expand_cnf(true, X, X, _):-!. 208expand_cnf(false, _, 0, _):-!. 209expand_cnf(-A, X, Y, S):-!, expand_cnf_neg(A, X, Y, S). 210expand_cnf(A + B, X, Y, S):-!, zdd_insert_atoms([A, B], X, Y, S). 211expand_cnf(A * B, X, Y, S):-!, ltr_insert(A, X, X0, S), 212 ltr_insert(B, X, X1, S), 213 ltr_join(X0, X1, Y, S). 214expand_cnf(A -> B, X, Y, S):-!, expand_cnf(-A + B, X, Y, S). 215expand_cnf(A == B, X, Y, S):-!, expand_cnf(A*B + (-A)*(-B), X, Y, S). 216expand_cnf(xor(A, B), X, Y, S):-!, expand_cnf(-A*B + A*(-B), X, Y, S). 217expand_cnf(A, X, Y, S):- ltr_insert(A, X, Y, S). 218% 219expand_cnf_neg(true, X, Y, S):- expand_cnf(false, X, Y, S). 220expand_cnf_neg(fase, X, Y, S):- expand_cnf(true, X, Y, S). 221expand_cnf_neg(A + B, X, Y, S):- expand_cnf(-A * -B, X, Y, S). 222expand_cnf_neg(A * B, X, Y, S):- expand_cnf(-A + -B, X, Y, S). 223expand_cnf_neg(A -> B, X, Y, S):- expand_cnf(A * -B, X, Y, S). 224expand_cnf_neg(A == B, X, Y, S):- expand_cnf( (-A)*B + (-B)*A, X, Y, S). 225expand_cnf_neg(xor(A, B), X, Y, S):- expand_cnf( (-A)*(-B) + A*B, X, Y, S). 226expand_cnf_neg(-A, X, Y, S):- expand_cnf(A, X, Y, S). 227expand_cnf_neg(A, X, Y, S):- ltr_insert(-A, X, Y, S)