1?- module(zdd).    2
    3% ?- solve_boole_verify([], true).
    4%@ Verified: dim = 0, count = 1.
    5%@ true .
    6% ?- solve_boole_verify([], false).
    7%@ Verified: dim = 0, count = 1.
    8%@ true .
    9% ?- spy(card), solve_boole_verify([], X).
   10% ?- spy(card), spy(card_of_sets), solve_boole_verify([X], X).
   11% ?- solve_boole_verify([X, Y], X*Y).
   12% ?- solve_boole_verify([X, Y], X+Y).
   13% ?- solve_boole_verify([X, Y], X->Y).
   14% ?- solve_boole_verify([X], X*A).
   15% ?- solve_boole_verify([X], X*A).
   16% ?- solve_boole_verify([], true).
   17% ?- solve_boole_verify([], false).
   18% ?- solve_boole_verify([X], true->X).
   19% ?- solve_boole_verify([], true->false).
   20% ?- solve_boole_verify([X], true).
   21% ?- solve_boole_verify([X], false).
   22% ?- solve_boole_verify([X], true->false).
   23% ?- solve_boole_verify([X, Y], X+Y).
   24% ?- solve_boole_verify([X, Y], X->Y).
   25% ?- solve_boole_verify([X], false->true).
   26% ?- solve_boole_verify([X], false->false).
   27% ?- solve_boole_verify([X], true->true).
   28% ?- solve_boole_verify([X], false->X).
   29% ?- solve_boole_verify([X], A*X).
   30% ?- solve_boole_verify([X], A->X).
   31% ?- solve_boole_verify([X,Y], A*X).
   32% ?- solve_boole_verify([X,Y], ((X*Y)->A)).
   33% ?- solve_boole_verify([X,Y], (A->(X*Y))).
   34% ?- solve_boole_verify([X,Y], (A-> (X*Y))).
   35% ?- solve_boole_verify([X,Y], X+Y).
   36% ?- solve_boole_verify([X,Y], X=A).
   37% ?- solve_boole_verify([X,Y], X=Y).
   38% ?- solve_boole_verify([X,Y], X->Y).
   39% ?- solve_boole_verify([X,Y], Y->X).
   40% ?- solve_boole_verify([X], \(X)+A).
   41% ?- solve_boole_verify([X], X + \(A)).
   42% ?- solve_boole_verify([X], X = false).
   43% ?- solve_boole_verify([X,Y], not(X)+(Y)).
   44% ?- solve_boole_verify([], \(X) + \(A)).
   45% ?- solve_boole_verify([X,A], \(X) + A).
   46% ?- solve_boole_verify([X], \(X)).
   47
   48?- solve_boole_verify([X,Y], \(X+A)).   49?- solve_boole_verify([X,A], \(X+A)).   50?- solve_boole_verify([X,Y], \(X+A)).   51?- solve_boole_verify([X,Y], \(X+Y)).   52?- solve_boole_verify([X], \(X)* \(A)).   53?- solve_boole_verify([X], X*A = false).   54
   55?- spy(sol_to_prop_list).   56?- solve_boole_verify([X], \(X) + \(A)), zdd_dump.   57%@ I
   58%@ =truth(2)
   59%@ L
   60%@ =truth(2)
   61%@ UL
   62%@ =truth(2)
   63%@ Root
   64%@ =node(5)=1*not(2)+not(1)
   65%@ Solutions0
   66%@ =sol(1)=true
   67%@ Residue0
   68%@ =truth(1)
   69%@ NOT verified: dim = 2, count = 3.
   70%@ *rozdd
   71%@ 1=if(1,truth(1),false)
   72%@ 2=if(1,false,truth(1))
   73%@ 3=if(2,false,truth(2))
   74%@ 4=if(1,3,3)
   75%@ 5=if(1,truth(2),truth(1))
   76%@ true .
   77
   78?- solve_boole_verify([X], \(X) + \(A)), zdd_dump.   79?- spy(elim_vars).   80?- solve_boole_verify([X], \(X) + \(A)).   81?- spy(verify_solution), spy(sol_to_prop_list),
   82   solve_boole_verify([X], \(X) + \(A)), zdd_dump.   83?- solc(1* \(2)+2* \(1)+false+false+(\(1)+ \(3)), R).   84
   85?- solc(1= 3* not(2) -> not(1)+ not(2), Count).   86
   87
   88
   89?- solve_boole_verify([X,Y], X*Y=A).   90?- solve_boole_verify([X,Y], ((X*Y)->A)*(A->(X*Y))).   91?- solve_boole_verify([X], \(X)* A)	.   92?- solve_boole_verify([X,A], \(X) + \(A)).   93?- solve_boole_verify([X,Y], \(X*Y)).   94?- solve_boole_verify([X,Y], \(X+Y)).   95
   96?- spy(elim_vars), solve_boole_verify([X,Y], \(X*Y)), zdd_dump.   97?- spy(elim_vars), solve_boole_verify([X,Y], \(X+Y)).   98?- spy(elim_vars), solve_boole_verify([X,Y], \(X=Y)).   99?- spy(elim_vars), solve_boole_verify([X,Y], not(X<->Y)).
  100?- spy(elim_vars), solve_boole_verify([X,Y], not(X->Y)).  101?- spy(elim_vars), solve_boole_verify([X,Y], \(X->Y)).  102?- spy(elim_vars), solve_boole_verify([X,Y], \(Y->X)).  103?- spy(elim_vars), solve_boole_verify([X,Y], \(X=Y)).  104?- spy(elim_vars), solve_boole_verify([X,Y], X\=Y).  105
  106
  107?- solve_boole([A], [X], \(X) + \(A), Residue, Sol).  108?- solve_boole([A], [X], \(X) + \(A), Residue, Sol).  109?- solve_boole([], [X], true, Residue, Sol).  110?- solve_boole([], [X], X, Residue, Sol).  111?- solve_boole([A], [X], X*A =false, Residue, Sol).  112?- solve_boole([A], [X], X*A =false, Residue, Sol).  113?- solve_boole([A], [X], X+A=true, Residue, Sol).  114?- solve_boole([A], [X], X+A=false, Residue, Sol).  115?- solve_boole([A], [X], \(X) * \(A),  Residue, Sol).  116?- solve_boole([], [X, Y], X*Y=true, Residue, Sol).  117?- solve_boole([], [X, Y], X*Y, Residue, Sol).  118?- solve_boole([A], [X, Y], X*Y=A, Residue, Sol).  119?- solve_boole([A], [X, Y], \(X*Y=A), Residue, Sol).  120?- solve_boole([A], [X, Y], (X*Y=A), Residue, Sol).  121?- solve_boole([A], [X, Y], (X*Y=false), Residue, Sols).  122?- solve_boole([], [Y1, Y2], Y1*Y2=false, Residue, Sol).  123?- solve_boole([], [Y1, Y2], Y1*Y2=true, Residue, Sol).  124?- solve_boole([], [Y1, Y2], Y1=true, Residue, Sol).  125?- solve_boole([], [Y1, Y2], Y1*Y2=true, Residue, Sol).  126?- solve_boole([], [Y1, Y2], Y1+Y2=true, Residue, Sol).  127?- solve_boole([], [Y1, Y2], Y1*Y2=true, Residue, Sol).  128?- solve_boole([A,B], [X, Y], A*X + B*Y = A*B, Residue, Sol);true.  129
  130?- solve([znew([X,Y]), *(X, Y, Z)]).  131?- solve([znew([X,Y]), *(X, Y, Z), +(X, Y, U)]),
  132   zout(Z),
  133   zout(U).  134?- zdd_sat([prop(A, X),prop(B, Y), *(X, Y, Z)]).  135?- time(solve_boole([A,B,C], [X, Y, Z], A*X + B*Y + C*Z = A*B*C, Reisdue, Sol)).  136?- time(solve_boole([A,B,C,D], [X,Y,Z,U], A*X + B*Y + C*Z + D*U = A*B*C*D, Reisdue, Sol)).  137?- nb_setval(slim_boole, true).  138?- nb_setval(slim_boole, false).  139?- solve_boole([A], [X, Y], X*Y = A, Reisdue, Sol); true.  140?- solve_boole([X], [Y1, Y2], (Y1*Y2 =false) * ((Y2 + not(Y1)*X) = not(X)) , Residue, Sol).  141?- solve_boole([X], [Y1, Y2], (Y1*Y2 =false) + ((Y2 + not(Y1)*X) = X) , Residue, Sol).  142?- solve_boole([X], [Y1, Y2], not((Y1*Y2 =false) + ((Y2 + not(Y1)*X) = true)) , Residue, Sol).  143?- solve_boole([X], [Y2, Y1], \((Y1*Y2 =false) + ((Y2 + not(Y1)*X) = X)) , Residue, Sol).  144?- solve_boole([X], [Y2, Y1], \((Y1*Y2 =false) + ((Y2 + not(Y1)*X) = not(X))) , Residue, Sol).  145?- solve_boole([A], [X, Y], X*Y = A , Reisdue, Sol).  146?- solve_boole([A,B,C], [X, Y,Z], A*X+B*Y+C*Z = true , Reisdue, Sol).  147?- solve_boole([A,B,C], [X, Y,Z], A*X+B*Y+C*Z = false , Reisdue, Sol).  148?- solve_boole([A], [X], A*X = true , Reisdue, Sol).  149?- spy(elim_one_var), solve_boole([A], [X], A*X = false , Reisdue, Sol), dump_rozdd.  150?- zdd_init, zdd_solve([prop(1, I), neg(I, 1, R)]), dump_rozdd.  151?- solve_boole([A], [X], A*X = false , Reisdue, Sol), dump_rozdd.  152?- zdd_init, zdd_solve([atomic_prop(A*X = false, P), prop(P, I)]),
  153?- solve_boole([A], [X], A + X = false , Reisdue, Sol).
  154?- solve_boole([A], [X], A + X = true , Reisdue, Sol).  155?- solve_boole([A], [X], A * X = true , Reisdue, Sol).  156?- solve_boole([A], [X], A * X = false , Reisdue, Sol).  157?- solve_boole([A], [X], \(A) + \(X) , Reisdue, Sol).  158?- solve_boole([A], [X], \(A) + X , Reisdue, Sol).  159?- solve_boole([A], [X], \(A) + \(X) , Reisdue, Sol).  160?- solve_boole([], [X], X , Reisdue, Sol).  161
  162?-  Hell_Heaven_Problem =
  163		   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  164	 solve_boole_verify([X, Y], [Z], Hell_Heaven_Problem).  165
  166?-  Hell_Heaven_Problem =
  167		   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  168	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]),
  169	 assoc_to_logic(Sol, Conj_of_eqns),
  170	 prop_to_basic(Conj_of_eqns * Cond_for_sol -> Hell_Heaven_Problem, Veri_cond),
  171	 solc(Veri_cond, Count).  172
  173?-  Hell_Heaven_Problem =
  174		   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  175	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]),
  176	 assoc_to_logic(Sol, Conj_of_eqns),
  177	 prop_to_basic(Conj_of_eqns * Cond_for_sol -> Hell_Heaven_Problem, Veri_cond),
  178	 solve([X=sat(Veri_cond)]).  179?- module(zdd).  180
  181
  182?- spy(zdd_sat/3), Hell_Heaven_Problem =
  183		   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  184	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]), zout(Sol),
  185	 assoc_to_logic(Sol, Logic),
  186	 prop_to_basic(Logic->Hell_Heaven_Problem, G),
  187	 solc(G, Count, [trace_node(true)]).  188
  189?-  Hell_Heaven_Problem =   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  190	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]),
  191	 assoc_to_logic(Sol, Logic),
  192	 spy(getid_with_zdd),
  193 	 spy(getid),
  194	 zdd([Res = sat(Verify)]).  195
  196?-  Hell_Heaven_Problem =   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  197	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]),
  198	 assoc_to_logic(Sol, Logic),
  199	 zdd_init,
  200	 trace,
  201 	 Verify = (Logic*Cond_for_sol -> Hell_Heaven_Problem),
  202	 zdd([Res = sat(Verify)]), sets(Res, Sets).  203
  204?- module(zdd).  205
  206?-  Hell_Heaven_Problem =   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  207	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]),
  208	 assoc_to_logic(Sol, Logic),
  209	 zdd_init,
  210	 trace,
  211 	 Verify = (Logic*Cond_for_sol -> Hell_Heaven_Problem),
  212	 solc(Verify, C).  213
  214?- spy(zdd_sat/3), Hell_Heaven_Problem =
  215		   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  216	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]), zout(Sol).  217
  218?- Hell_Heaven_Problem =
  219		   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  220	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[slim_boole(true)]), zout(Sol).  221
  222?-  Hell_Heaven_Problem = (X+Y+Z),
  223	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]).  224
  225?- Hell_Heaven_Problem = (X+Y),
  226	 solve_boole([X], [Y], Hell_Heaven_Problem, Cond_for_sol, Sol,[slim_boole(true)]).  227
  228?- Hell_Heaven_Problem = (X+Y+Z),
  229	 solve_boole([X,Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[slim_boole(true)]).  230
  231?- tree_to_prop(if(3, truth(3), truth(3)), A), slim_boole(A, B).  232
  233?- Hell_Heaven_Problem =
  234		   (not(Y) + (not(Z) + X)*(Z + not(X))) *	(Y + (not(Z) + not(X))*(Z + X)),
  235	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,
  236				[slim_boole(true)]), writeln(Sol).  237?- time((Hell_Heaven_Problem =
  238		   (not(Y) + (not(Z) + X)*(Z + not(X))) *
  239		   (Y + (not(Z) + not(X))*(Z + X)),
  240	 solve_boole([X, Y], [Z], Hell_Heaven_Problem, Residue, Sol, [slim_boole(true)]))).  241
  242
  243 ?-  zdd_init,
  244	 Hell_Heaven_Problem =
  245			(\(A2) + (\(A3) + A1)*(A3 + \(A1)))
  246		*	(A2 + (\(A3) + \(A1))*(A3 + A1)),
  247	zdd_solve([
  248		newvars([A1,A2,A3,A4]),
  249		prop(Hell_Heaven_Problem, Root),
  250		getzdd(Root, if(X, L, R)),
  251		*(L, R, Meet),
  252		neg(R, NegR)]),
  253	zdd_to_prop(L, LForm),
  254	zdd_to_prop(NegR, RForm),
  255	General_Sol_of_Hell_Heaven = A4 * LForm + RForm.  256
  257[2018/02/09] with newvars,getzdd, zdd_to_form
  258Query.
  259 ?-  zdd_init,
  260	 Hell_Heaven_Problem =
  261			(\(A2) + (\(A3) + A1)*(A3 + \(A1)))
  262		*	(A2 + (\(A3) + \(A1))*(A3 + A1)),
  263	zdd_solve([
  264		newvars([A1,A2,A3,A4]),
  265		prop(Hell_Heaven_Problem, Root),
  266		getzdd(Root, if(X, L, R)),
  267		*(L, R, Meet),
  268		neg(R, NegR)]),
  269	zdd_to_prop(L, LForm),
  270	zdd_to_prop(NegR, RForm),
  271	General_Sol_of_Hell_Heaven = A4 * LForm + RForm.  272
  273Query:
  274 ?-  zdd_init,
  275	 Hell_Heaven_Problem =
  276		(\(2) + (\(3) + 1)*(3 + \(1))) *
  277		(2 + (\(3) + \(1))*(3 + 1)),
  278	zdd_solve([
  279		prop(Hell_Heaven_Problem, Root),
  280		{ getzdd(Root, if(X, L, R)) },
  281		adjust(L, R, L0, R0),
  282		meet(L0, R0, Meet),
  283		neg(R, NegR)]),
  284	zdd_to_prop(L, LForm),
  285	zdd_to_prop(NegR, RForm),
  286	General_Sol_of_Hell_Heaven = 4 * LForm + RForm.
  287
  288 ?-  zdd_init,
  289	 Hell_Heaven_Problem =
  290		(\(2) + (\(3) + 1)*(3 + \(1))) *
  291		(2 + (\(3) + \(1))*(3 + 1)),
  292	zdd_solve([
  293		prop(Hell_Heaven_Problem, Root),
  294		getzdd(Root, if(X, L, R)),
  295		meet(L, R, Meet),
  296		neg(R, NegR)]),
  297	zdd_to_prop(L, LForm),
  298	zdd_to_prop(NegR, RForm),
  299	General_Sol_of_Hell_Heaven = 4 * LForm + RForm.  300
  301The output:
  302
  303 Hell_Heaven_Problem =  (\2+(\3+1)*(3+ \1))*(2+(\3+ \1)*(3+1)),
  304 Root = 27,
  305 X = 3,
  306 L = L0, L0 = NegR, NegR = 25,
  307 R = R0, R0 = 26,
  308 Meet = false,   % <== necessary condition for the existence of solutions.
  309 Ltree = Rtree, Rtree = if(2, if(1, truth(0), false), truth(0)),
  310 LForm = RForm, RForm = 2*(1*truth(0)+not(1)*false)+not(2)*(not(1)*truth(0)),
  311 General_Sol_of_Hell_Heaven =   4*(2*(1*truth(0)+not(1)*false)+not(2)*(not(1)*truth(0)))
  312							  + (2*(1*truth(0)+not(1)*false)+not(2)*(not(1)*truth(0))) .
  313
  314If we take the parameter 4 to be false, then we have
  315
  316						  2*1 + not(2)*not(1)
  317
  318as an answer for the puzzle.
  319
  320For joinmary, I have found the rozdd handler works well as I expected,
  321at least for the hell-heaven puzzle, though details remain
  322to be explained.
  323
  324Kuniaki Mukai
  325
  326% ?- module(zdd).
  327
  328 ?-  zdd_init,
  329	 Fxab = (\(A2) + (\(A3) + A1)*(A3+ \(A1))) *
  330			(A2 + (\(A3) + \(A1))*(A3+A1)),
  331	zdd_solve([
  332		newvars([A1,A2,A3,A4]),
  333		prop(Fxab, Root),
  334		getzdd(Root, if(X, L, R)),
  335		adjust(L, R, L0, R0),
  336		meet(L0, R0, Meet),
  337		join(L0, R0, Join),
  338		neg(R, NegR),
  339		+(L, NegR, Ans)]),
  340	zdd_to_prop(L, LForm),
  341	zdd_to_prop(NegR, RForm),
  342	General_Sol_of_Hell_Heaven = A4 * LForm + RForm.
  343 %@ Fxab =  (\2+(\3+1)*(3+ \1))*(2+(\3+ \1)*(3+1)),
  344 %@ A2 = 2,
  345 %@ A3 = X, X = 3,
  346 %@ A1 = 1,
  347 %@ A4 = 4,
  348 %@ Root = 27,
  349 %@ L = L0, L0 = NegR, NegR = Ans, Ans = 25,
  350 %@ R = R0, R0 = 26,
  351 %@ Meet = false,
  352 %@ Join = truth(2),
  353 %@ LForm = RForm, RForm = 2*(1*truth(0)+not(1)*false)+not(2)*(not(1)*truth(0)),
  354 %@ General_Sol_of_Hell_Heaven = 4*(2*(1*truth(0)+not(1)*false)+not(2)*(not(1)*truth(0)))+(2*(1*truth(0)+not(1)*false)+not(2)*(not(1)*truth(0))).
  355
  356% ?- prop((((A->B)->(B->C))=true)->((A->C)=true)), card(R).
  357% ?- prop((((A->B)->(B->C)))->((A->C))), card(R).
  358% ?- time(solc(((((A->B)*(B->C)))->((A->C))), R)).
  359% ?- time(solc(((((A->B)*(B->C)*(C->D)))->((A->D))), R)).
  360% ?- time(solc(\((((A->B)*(B->C)*(C->D)))->((A->D))), R)).