#const m=sat. % #const m=asp. % switch between ASP and MAXSAT/PB mode #const d=1. % #const d=0. % redundant difference constraints (USED by rpoly) #const l=0. % #const l=1. % redundant lower bound constraints (not used by rpoly) #const e=0. % #const e=1. % use equivalences rather than implications (not used by rpoly) % DOMAIN mode(m). cons(0). cons(1). oppo(X,Y) :- cons(X), cons(Y), X+Y = 1. string(S) :- string(S,1,X). pos(N) :- string(1,N,X). fixed(S,P,P+Q) :- string(S), P = #count{ N : string(S,N,0) }, Q = #count{ N : string(S,N,1) }. equal(S1,S2,N) :- fixed(S1,P,R), fixed(S2,P,R), S1 != S2, string(S1,N,X), string(S2,N,X), equal(S1,S2,N-1) : 1 < N. less(S1,S2) :- fixed(S1,P1,R1), fixed(S2,P2,R2), R2 < R1. less(S1,S2) :- fixed(S1,P1,R), fixed(S2,P2,R), P2 < P1. less(S1,S2) :- fixed(S1,P,R), fixed(S2,P,R), string(S1,N,X1), string(S2,N,X2), X1 < X2, equal(S1,S2,N-1) : 1 < N. index(S2,I+1) :- string(S2), I = #count{ S1 : less(S1,S2) }. index(I,N,X) :- index(S,I), string(S,N,X). index(I) :- index(S,I). oppose(S1,S2) :- index(S1,N,X1), index(S2,N,X2), oppo(X1,X2). compat(S1,S2) :- index(S1), index(S2), not oppose(S1,S2). close(S1,S2) :- compat(S1,S2). close(S1,S3) :- compat(S1,S2), close(S2,S3). other(S2) :- close(S1,S2), S1 < S2. group(S) :- index(S), not other(S). distinct(S,N1,N2) :- group(S), close(S,S1), index(S1,N1,X), index(S1,N2,1-X), cons(X), N1 < N2. specific(S,N1,N2) :- group(S), close(S,S1), index(S1,N1,X), index(S1,N2,Y), X/2+Y/2 = 1, N1 < N2. specific(S,N1,N2) :- distinct(S,N1,N2), close(S,S1), index(S1,N1,X), index(S1,N2,X), cons(X). relevant(S,N2) :- group(S), pos(N2), specific(S,N1,N2) : N1 = 1..N2-1. % relate(S,N1,N2) :- relevant(S,N1), pos(N2), N1 < N2, not specific(S,N1,N2). evaluate(S1,N) :- relevant(S,N), close(S,S1), index(S1,N,2). evaluate(S1) :- evaluate(S1,N). evaluate(S1,N,P) :- evaluate(S1,N), P = #count{ S2 : compat(S1,S2), not evaluate(S2,N) }. select(S,M) :- evaluate(S), (Q,M) = #max{ (P,N) : evaluate(S,N,P) }. map(S,2*S,1) :- index(S). map(S,P-1,0) :- map(S,P,1), evaluate(S). map(S,P) :- map(S,P,A). map(P) :- map(S,P). static(P,N,X) :- relevant(S1,N), close(S1,S), index(S,N,X), map(S,P), cons(X). static(P,N,A) :- select(S,N), map(S,P,A). static(P,N) :- static(P,N,X). domain(P,N) :- relevant(S1,N), close(S1,S), map(S,P), not static(P,N). drop(P1,P2) :- compat(S1,S2), map(S1,P1,A), map(S2,P2,1-A), select(S1,N), select(S2,N), S1 < S2. drop(P1,P2) :- compat(S1,S2), map(S1,P1,A), map(S2,P2), select(S1,N), index(S2,N,1-A), S1 < S2. drop(P1,P2) :- compat(S1,S2), map(S2,P2,A), map(S1,P1), select(S2,N), index(S1,N,1-A), S1 < S2. comp(P1,P2) :- compat(S1,S2), map(S1,P1), map(S2,P2), not drop(P1,P2), S1 < S2. comp(P1,P2,N) :- comp(P1,P2), domain(P1,N). comp(P1,P2,N) :- comp(P1,P2), domain(P2,N). match(P1,P2) :- comp(P1,P2), d = 1. match(P2,P1) :- comp(P1,P2), d = 1. check(P1,P2) :- map(S,P1,1), map(S,P2,0), 1 < { match(P1,P); match(P2,P) : not match(P1,P) }. check(P1,P2,S1,S2) :- comp(P1,P2,N), map(S1,P1), map(S2,P2), l = 1, static(P1,N) : not static(P2,N). % ASP { parent(S,N) } :- map(S,P,0), domain(P,N), mode(asp). { differ(P1,P2) } :- comp(P1,P2), e != 1, mode(asp). { differ(P) } :- map(P), e != 1, mode(asp). differ(P1,P2,N) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e = 1, mode(asp), parent(S,N) : map(S,P1,1); not parent(S,N) : map(S,P1,0); parent(S,N) : map(S,P2,0); not parent(S,N) : map(S,P2,1). differ(P1,P2,N) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e = 1, mode(asp), parent(S,N) : map(S,P2,1); not parent(S,N) : map(S,P2,0); parent(S,N) : map(S,P1,0); not parent(S,N) : map(S,P1,1). differ(P1,P2) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e != 1, mode(asp), parent(S,N) : map(S,P1,1); not parent(S,N) : map(S,P1,0); parent(S,N) : map(S,P2,0); not parent(S,N) : map(S,P2,1). differ(P1,P2) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e != 1, mode(asp), parent(S,N) : map(S,P2,1); not parent(S,N) : map(S,P2,0); parent(S,N) : map(S,P1,0); not parent(S,N) : map(S,P1,1). differ(P1,P2) :- differ(P1,P2,N), mode(asp). differ(P1,P2) :- comp(P1,P2,N), static(P2,N,1), mode(asp), parent(S,N) : map(S,P1,0); not parent(S,N) : map(S,P1,1). differ(P1,P2) :- comp(P1,P2,N), static(P2,N,0), mode(asp), parent(S,N) : map(S,P1,1); not parent(S,N) : map(S,P1,0). differ(P1,P2) :- comp(P1,P2,N), static(P1,N,1), mode(asp), parent(S,N) : map(S,P2,0); not parent(S,N) : map(S,P2,1). differ(P1,P2) :- comp(P1,P2,N), static(P1,N,0), mode(asp), parent(S,N) : map(S,P2,1); not parent(S,N) : map(S,P2,0). differ(P2) :- map(P2), mode(asp), differ(P1,P2) : comp(P1,P2). :- check(P1,P2), mode(asp), differ(P1), differ(P2), differ(P1,P) : comp(P1,P); differ(P2,P) : comp(P2,P). :- check(P1,P2,S1,S2), check(P3,P4,S1,S2), (P1,P2) < (P3,P4), mode(asp), not differ(P1,P2), not differ(P3,P4). % SAT differ(P1,P2,N) | parent(S,N) : map(S,P1,1) | -parent(S,N) : map(S,P2,1) | -parent(S,N) : map(S,P1,0) | parent(S,N) : map(S,P2,0) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e = 1, mode(sat). differ(P1,P2,N) | -parent(S,N) : map(S,P1,1) | parent(S,N) : map(S,P2,1) | parent(S,N) : map(S,P1,0) | -parent(S,N) : map(S,P2,0) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e = 1, mode(sat). -differ(P1,P2,N) | parent(S,N) : map(S,P1,1) | parent(S,N) : map(S,P2,1) | -parent(S,N) : map(S,P1,0) | -parent(S,N) : map(S,P2,0) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e = 1, mode(sat). -differ(P1,P2,N) | -parent(S,N) : map(S,P1,1) | -parent(S,N) : map(S,P2,1) | parent(S,N) : map(S,P1,0) | parent(S,N) : map(S,P2,0) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e = 1, mode(sat). differ(P1,P2) | parent(S,N) : map(S,P1,1) | -parent(S,N) : map(S,P2,1) | -parent(S,N) : map(S,P1,0) | parent(S,N) : map(S,P2,0) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e != 1, mode(sat). differ(P1,P2) | -parent(S,N) : map(S,P1,1) | parent(S,N) : map(S,P2,1) | parent(S,N) : map(S,P1,0) | -parent(S,N) : map(S,P2,0) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e != 1, mode(sat). differ(P1,P2) | -differ(P1,P2,N) :- comp(P1,P2,N), domain(P1,N), domain(P2,N), e = 1, mode(sat). differ(P1,P2) | parent(S,N) : static(P2,N,1), map(S,P1,1) | -parent(S,N) : static(P2,N,0), map(S,P1,1) | -parent(S,N) : static(P2,N,1), map(S,P1,0) | parent(S,N) : static(P2,N,0), map(S,P1,0) :- comp(P1,P2,N), static(P2,N), mode(sat). differ(P1,P2) | parent(S,N) : static(P1,N,1), map(S,P2,1) | -parent(S,N) : static(P1,N,0), map(S,P2,1) | -parent(S,N) : static(P1,N,1), map(S,P2,0) | parent(S,N) : static(P1,N,0), map(S,P2,0) :- comp(P1,P2,N), static(P1,N), mode(sat). -differ(P1,P2) | differ(P1,P2,N) : domain(P1,N), domain(P2,N) | -parent(S,N) : comp(P1,P2,N), static(P2,N,1), map(S,P1,1) | parent(S,N) : comp(P1,P2,N), static(P2,N,0), map(S,P1,1) | -parent(S,N) : comp(P1,P2,N), static(P1,N,1), map(S,P2,1) | parent(S,N) : comp(P1,P2,N), static(P1,N,0), map(S,P2,1) | parent(S,N) : comp(P1,P2,N), static(P2,N,1), map(S,P1,0) | -parent(S,N) : comp(P1,P2,N), static(P2,N,0), map(S,P1,0) | parent(S,N) : comp(P1,P2,N), static(P1,N,1), map(S,P2,0) | -parent(S,N) : comp(P1,P2,N), static(P1,N,0), map(S,P2,0) :- comp(P1,P2), e = 1, mode(sat). differ(P2) | -differ(P1,P2) : comp(P1,P2) :- map(P2), mode(sat). -differ(P2) | differ(P1,P2) :- map(P2), comp(P1,P2), e = 1, mode(sat). -differ(P1) | -differ(P2) | -differ(P1,P) : comp(P1,P) | -differ(P2,P) : comp(P2,P) :- check(P1,P2), mode(sat). differ(P1,P2) | differ(P3,P4) :- check(P1,P2,S1,S2), check(P3,P4,S1,S2), (P1,P2) < (P3,P4), mode(sat). % OPTIMIZE :~ differ(P). [1,P] :~ not index(1). [0] % DISPLAY #show parent/2. #show -parent/2. #show differ/3. #show -differ/3. #show differ/2. #show -differ/2. #show differ/1. #show -differ/1. % UNUSED EXPERIMENTAL CODE KEPT BELOW FOR REFERENCE %* evaluate(S1,N,(P+Q-|P-Q|)/2,P+Q) :- evaluate(S1,N), P = #count{ S2 : compat(S1,S2), index(S2,N,0) }, Q = #count{ S2 : compat(S1,S2), index(S2,N,1) }. select(S,M) :- evaluate(S), (T,Q,M) = #max{ (R,P,N) : evaluate(S,N,P,R) }. *% %* tresh(#sup). ratio(4,5). prescore(S,S1,N,M) :- evaluate(S,S1,N), M = #count{ S2 : compat(S1,S2), evaluate(S2), not evaluate(S,S2,N) }. prefer(S,S1,N1,N2) :- prescore(S,S1,N1,M1), prescore(S,S1,N2,M2), (M2,N2) < (M1,N1), (M3,N3) <= (M2,N2) : prescore(S,S1,N3,M3), (M3,N3) < (M1,N1). prefer(S,S1,N2) :- prefer(S,S1,N1,N2). score(S,S1,N1,1) :- evaluate(S,S1,N1), not prefer(S,S1,N1). score(S,S1,N2,I+1) :- score(S,S1,N1,I), prefer(S,S1,N1,N2), prescore(S,S1,N1,M), prescore(S,S1,N2,M). score(S,S1,N2,I+1) :- score(S,S1,N1,I), prefer(S,S1,N1,N2), tresh(T), I < T, ratio(X,Y), prescore(S,S1,N1,M1), prescore(S,S1,N2,M2), M1 <= (M2*Y+X-1)/X. score(S,S1) :- score(S,S1,N,M). % score(S,S1,N,M) :- evaluate(S,S1,N), % M = #count{ S2 : compat(S1,S2), evaluate(S2), not evaluate(S,S2,N) }. % score(S,S1,(P/C,C)) :- score(S,S1), % C = #count{ N : evaluate(S,S1,N) }, P = #sum+{ M,N : score(S,S1,N,M) }. score(S,S1,M) :- score(S,S1), score(S,S1,N,1), prescore(S,S1,N,M). % P = #min{ N : score(S,S1,N,1), }. rowsort(S1,S2) :- score(S,S1,P1), score(S,S2,P2), (P1,S1) < (P2,S2), (P3,S3) <= (P1,S1) : score(S,S3,P3), (P3,S3) < (P2,S2). rowsucc(S2) :- rowsort(S1,S2). colsort(S1,N1,N2) :- score(S,S1,N1,P1), score(S,S1,N2,P2), (P1,N1) < (P2,N2), (P3,N3) <= (P1,N1) : score(S,S1,N3,P3), (P3,N3) < (P2,N2). colpred(S1,N1) :- colsort(S1,N1,N2). colsucc(S1,N2) :- colsort(S1,N1,N2). rank(S1,S2,N,C) :- score(S,S1), prescore(S,S2,N,M), score(S,S2,N,I), not rowsucc(S1), C = #count{ N1 : prescore(S,S2,N1,M1), score(S,S2,N1,I1), M1 < M }. rank(S2,S3,N,M) :- rank(S1,S3,N,M), rowsort(S1,S2), S1 != S3, not compat(S1,S3). rank(S2,S3,N,M) :- rank(S1,S3,N,M), rowsort(S1,S2), S1 != S3, select(S1,N1), N != N1, compat(S1,S3), evaluate(S1,N). rank(S2,S3,N,M) :- rank(S1,S3,N,M), rowsort(S1,S2), S1 != S3, select(S1,N1), % N != N1, compat(S1,S3), not evaluate(S3,N1). rank(S2,S3,N,M+1) :- rank(S1,S3,N,M), rowsort(S1,S2), S1 != S3, select(S1,N1), % N != N1, compat(S1,S3), evaluate(S3,N1), not evaluate(S1,N). rank(S2,S3,N,M+1) :- rank(S1,S3,N,M), rowsort(S1,S2), S1 != S3, select(S1,N), compat(S1,S3). pick(S1,N1,N1,M1) :- rank(S1,S1,N1,M1), not colsucc(S1,N1). pick(S1,N2,N3,M3) :- rank(S1,S1,N2,M2), colsort(S1,N1,N2), pick(S1,N1,N3,M3), M2 <= M3. pick(S1,N2,N2,M2) :- rank(S1,S1,N2,M2), colsort(S1,N1,N2), pick(S1,N1,N3,M3), M3 < M2. select(S1,N2) :- pick(S1,N1,N2,M2), not colpred(S1,N1). *% %* score(S1,N,M) :- evaluate(S1,N), M = #count{ S2 : compat(S1,S2), evaluate(S2), not evaluate(S2,N) }. score(S,(P,-Q)) :- evaluate(S), P = #max{ M : score(S,N,M) }, Q = #sum{ M : score(S,N,M) }. % rowsort(S1,S2) :- group(S), close(S,S1), close(S,S2), evaluate(S1), evaluate(S2), S1 < S2, % S3 <= S1 : close(S,S3), evaluate(S3), S3 < S2. rowsort(S1,S2) :- group(S), close(S,S1), close(S,S2), score(S1,P1), score(S2,P2), (P2,S2) < (P1,S1), (P3,S3) <= (P2,S2) : close(S,S3), score(S3,P3), (P3,S3) < (P1,S1). rowpred(S1) :- rowsort(S1,S2). rowsucc(S2) :- rowsort(S1,S2). % colsort(S,N1,N2) :- evaluate(S,N1), evaluate(S,N2), N1 < N2, % N3 <= N1 : evaluate(S,N3), N3 < N2. colsort(S,N1,N2) :- score(S,N1,M1), score(S,N2,M2), (M2,N2) < (M1,N1), (M3,N3) <= (M2,N2) : score(S,N3,M3), (M3,N3) < (M1,N1). colpred(S,N1) :- colsort(S,N1,N2). colsucc(S,N2) :- colsort(S,N1,N2). sort(S1,N1,S1,N2) :- colsort(S1,N1,N2). sort(S1,N1,S2,N2) :- rowsort(S1,S2), evaluate(S1,N1), evaluate(S2,N2), not colpred(S1,N1), not colsucc(S2,N2). sortinit(S1,N1) :- evaluate(S1,N1), not rowsucc(S1), not colsucc(S1,N1). sortexit(S2,N2) :- evaluate(S2,N2), not rowpred(S2), not colpred(S2,N2). pass(S,S1,N,M,0,1) :- group(S), close(S,S1), score(S1,N,M). % pass(S,S1,N,M,0,1) :- group(S), close(S,S1), evaluate(S1,N), % M = #count{ S2 : compat(S1,S2), evaluate(S2), not evaluate(S2,N) }. pass(S,S1,N,M,P,I+1) :- pass(S,S1,N,M,P,I), pick(S,S2,N2,S3,N3,M3,P3,I), sortexit(S2,N2), not compat(S1,S3). pass(S,S1,N,M,P,I+1) :- pass(S,S1,N,M,P,I), pick(S,S2,N2,S3,N3,M3,P3,I), sortexit(S2,N2), not evaluate(S1,N3). pass(S,S1,N,M+2,P,I+1) :- pass(S,S1,N,M,P,I), pick(S,S2,N2,S3,N,M3,P3,I), sortexit(S2,N2), compat(S1,S3), S1 != S3. pass(S,S1,N,M+1,P,I+1) :- pass(S,S1,N,M,P,I), pick(S,S2,N2,S3,N3,M3,P3,I), sortexit(S2,N2), compat(S1,S3), evaluate(S1,N3), not evaluate(S3,N). pass(S,S1,N,M,P-1,I+1) :- pass(S,S1,N,M,P,I), pick(S,S2,N2,S3,N3,M3,P3,I), sortexit(S2,N2), compat(S1,S3), evaluate(S1,N3), evaluate(S3,N), S1 != S3, N != N3. pass(I) :- pass(S,S1,N,M,P,I). skip(S,S1,I) :- pick(S,S2,N2,S1,N,M,P,I-1), sortexit(S2,N2), pass(I). skip(S,S1,I) :- skip(S,S1,I-1), pass(I). pick(S,S1,N1,S1,N1,M1,P1,I) :- sortinit(S1,N1), pass(S,S1,N1,M1,P1,I). pick(S,S1,N1,S1,N1,0,#inf,I) :- sortinit(S1,N1), pass(I), skip(S,S1,I). pick(S,S2,N2,S3,N3,M3,P3,I) :- pick(S,S1,N1,S3,N3,M3,P3,I), sort(S1,N1,S2,N2), skip(S,S2,I). pick(S,S2,N2,S2,N2,M2,P2,I) :- pick(S,S1,N1,S3,N3,M3,#inf,I), sort(S1,N1,S2,N2), pass(S,S2,N2,M2,P2,I). pick(S,S2,N2,S3,N3,M3,P3,I) :- pair(S,S2,N2,M2,P2,S3,N3,M3,P3,I), (P2,M2) <= (P3,M3). pick(S,S2,N2,S2,N2,M2,P1,I) :- pair(S,S2,N2,M2,P2,S3,N3,M3,P3,I), (P2,M2) > (P3,M3), pass(S,S2,N2,M2,P1,I). pair(S,S2,N2,M2,0,S3,N3,M3,0,I) :- pick(S,S1,N1,S3,N3,M3,P3,I), sort(S1,N1,S2,N2), pass(S,S2,N2,M2,P2,I), P3 != #inf, S2 != S3. pair(S,S1,N2,M2,P2,S1,N3,M3,P3,I) :- pick(S,S1,N1,S1,N3,M3,P3,I), sort(S1,N1,S1,N2), pass(S,S1,N2,M2,P2,I). select(S1,N1) :- pick(S,S2,N2,S1,N1,M1,P1,I), sortexit(S2,N2). *%