EDIT 7/11/2022
I am glad to see a riddle solver below works based on bdd/zdd. true_frames/4 defined there is to select all frames which satisfies given specifications. For the time being, my concern is to have experiences on bdd/zdd programming, and I feel it is promissing for Prolog community; feeling it is as clear and easy as almost list processing. However, as for this riddle solver on bdd/zdd, I have no idea how to prune redundant frames in earlier stage, which is always difficult problem though.
?- #S, solve_riddle(
[bill < tom], % order on domain.
[mono([bill, tom]-[cat, dog])], % one-to-one mappling
owner_of(dog) = tom, % truth condition on frame
Sols, S),
psa(Sols, S). % print all solution frames.
[bill-cat, tom-dog] % solution.
% main.
solve_riddle(RelOnDom, FunSpec, FrameCond, Sols, S):-
funs_on_ord_dom(RelOnDom, FunSpec, Frames, S),
true_frames(Frames, Sols, FrameCond, S).
%
true_frames(X, Y, Cond, S):- true_frames(X, [], Y, Cond, S).
%
true_frames(0, _, 0, _, _):- !.
true_frames(1, H, Y, Cond, _):- !,
( frame_check(Cond, H) -> Y = 1
; Y = 0
).
true_frames(X, H, Y, Cond, S):-
cofact(X, t(A, L, R), S),
true_frames(L, H, L0, Cond, S),
true_frames(R, [A|H], R0, Cond, S),
cofact(Y, t(A, L0, R0), S).
sat((X, Y), M):-!, (sat(X, M), sat(Y, M)). % AND
sat((X; Y), M):-!, (sat(X, M); sat(Y, M)). % OR
sat(\+ X, M):-!, \+ sat(X, M). % NOT
sat(X -> Y, M):-!, (\+sat(X, M); sat(Y, M)). % IMPLY
sat(X = Y, M):-!, (eval_exp(X, I, M), eval_exp(Y, I, M)). % EQUALITY
sat(X > Y, M):-!, eval_exp(X, I, M),
eval_exp(Y, J, M),
basic_fact(I > J, M).
sat(X < Y, M):-!, eval_exp(X, I, M),
eval_exp(Y, J, M),
basic_fact( I < J, M).
sat(F, M):- basic_fact(F, M).
%
basic_fact(own(X, Y), M) :-!, member(X-Y, M).
basic_fact(owned_by(X, Y), M) :-!, member(Y-X, M).
basic_fact(X > Y, M) :-!, riddle_compare(M, >, X, Y).
basic_fact(X < Y, M) :-!, riddle_compare(M, <, X, Y).
basic_fact(X = X, _):-!.
basic_fact(F, M):- member(F, M).
riddle_compare(_, =, X, X):-!.
riddle_compare([], =, _, _):-!.
riddle_compare([X-_|_], >, X, _):-!.
riddle_compare([Y-_|_], <, _, Y):-!.
riddle_compare([_|List], C, X, Y):- riddle_compare(List, C, X, Y).
%
eval_exp(owner_of(P), X, M):-!, eval_exp(P, P0, M),
basic_fact(X-P0, M).
eval_exp(X, X, _).
End of Edit.
EDIT 06/11/2022
Combining the linear completion and building function spaces in BDD/ZDD, I have integrated them into funs_on_ord_dom/4. Roughly, it enumerates all functions on linearly orderd domain from partial specifications . Being satisfied with clean and short codes added to handle bdd/zdd (in my criteria !), now I am wondering about its application. I would like to apply it first to generate all frames for some kind of riddles soon.
This is a sample query, where mono means injection (one-to-on mapping). Also epi, surjection (onto mappling) is prepared.
% ?- open_state(S),
% funs_on_ord_dom([tom<jack, mary<betty],
% [mono([tom, jack]-[apple, grape]), mono([mary, betty]-[tennis, baseball])], Out, S),
% psa(Out, S).
%@ zid = 194
%@ [tom-grape,mary-tennis,jack-apple,betty-baseball]
%@ [tom-grape,mary-tennis,betty-baseball,jack-apple]
%@ [tom-grape,mary-baseball,jack-apple,betty-tennis]
%@ [tom-grape,mary-baseball,betty-tennis,jack-apple]
%@ [tom-grape,jack-apple,mary-tennis,betty-baseball]
%@ [tom-grape,jack-apple,mary-baseball,betty-tennis]
%@ [tom-apple,mary-tennis,jack-grape,betty-baseball]
%@ [tom-apple,mary-tennis,betty-baseball,jack-grape]
%@ [tom-apple,mary-baseball,jack-grape,betty-tennis]
%@ [tom-apple,mary-baseball,betty-tennis,jack-grape]
%@ [tom-apple,jack-grape,mary-tennis,betty-baseball]
%@ [tom-apple,jack-grape,mary-baseball,betty-tennis]
%@ [mary-tennis,tom-grape,jack-apple,betty-baseball]
%@ [mary-tennis,tom-grape,betty-baseball,jack-apple]
%@ [mary-tennis,tom-apple,jack-grape,betty-baseball]
%@ [mary-tennis,tom-apple,betty-baseball,jack-grape]
%@ [mary-tennis,betty-baseball,tom-grape,jack-apple]
%@ [mary-tennis,betty-baseball,tom-apple,jack-grape]
%@ [mary-baseball,tom-grape,jack-apple,betty-tennis]
%@ [mary-baseball,tom-grape,betty-tennis,jack-apple]
%@ [mary-baseball,tom-apple,jack-grape,betty-tennis]
%@ [mary-baseball,tom-apple,betty-tennis,jack-grape]
%@ [mary-baseball,betty-tennis,tom-grape,jack-apple]
%@ [mary-baseball,betty-tennis,tom-apple,jack-grape]
%@ -------------------
%@ S = ..,
%@ Out = 194.
End on Edit.
I am playing around zdd (now together with BDD ?) programming in SWI-Prolog. This post
is about such a codes among many others. It is an interleaving of domain disjoint family of relations.
Suppoese integers a, b, c, d satisfying conditions
a < b, a<c, b<d, c<d.
What are the possible sorted lists which is compatible with this partial information ? Of couse, for the case, it is easy to find:
[a, c, b, d]
[a, b, c, d].
I wrote codes which enumerates all such possible sorted lists which is compatble with given partial set of inequalities.
% ?- #S, linear_order_completion([a<b, a<c, b<d, c<d], Out, S), psa(LC, S).
%@ zid = 10
%@ [a,c,b,d]
%@ [a,b,c,d]
%@ -------------------
%@ S = ..,
%@ Out = 10 .
I have managed to write this codes which enumerates all lists which is compatible with given parital ordering. At first glance it seemed a well known fundamental problem, but for me it was new. My algorithm, first, divides the given relation into a set of connected subgraphs using UNION-FIND. Then for each connected subrelation, enumerates all possible total orderings introducting
new links for each incomparable pairs. Finally, interleaving all obtained linear orderings. These operations are done in BDD expecting its strucute shareing ability. Of course I believe, based on experiece in my
life, there must be clever alorighm known which I don’t . I appreciate if someone points to related information.
This is a test which enumerates all interleaving two total ordering sets with 50 elements. The test shows there is 100,891,344,545,564,193,334,812,497,256 solutions !, which might suggest that the problem is inherently hard.
%
% ?- #S, N = 100, numlist(1, N, Ns), append(A, B, Ns), length(A, ALen),
% ALen =:= N//2,
% findall(I<J, ( member(I, A), J is I+1, J =< ALen), A0),
% findall(K<L, ( member(K, B), L is K+1, L =< N ), B0),
% append(A0, B0, Rel),
% time(( relation_to_bdd_list(Rel, SubRels, S),
% fold_bdd_interleave(SubRels, 1, BddOfSortedList, S))),
% card(BddOfSortedList, Card, S).
%@ % 1,110,111,927 inferences, 79.388 CPU in 79.536 seconds (100% CPU, 13983332 Lips)
%@ S = ..,
%@ N = 100,
%@ Ns = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ A = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],
%@ B = [51, 52, 53, 54, 55, 56, 57, 58, 59|...],
%@ ALen = 50,
%@ A0 = [1<2, 2<3, 3<4, 4<5, 5<6, 6<7, 7<8, 8<9, ... < ...|...],
%@ B0 = [51<52, 52<53, 53<54, 54<55, 55<56, 56<57, 57<58, 58<59, ... < ...|...],
%@ Rel = [1<2, 2<3, 3<4, 4<5, 5<6, 6<7, 7<8, 8<9, ... < ...|...],
%@ SubRels = [51, 101],
%@ BddOfSortedList = 7601,
%@ Card = 100,891,344,545,564,193,334,812,497,256 .