heaven-hell-puzzle in boolean constraing.

[Kuniaki Mukai]

Hi,

Is there any solution in clpb library for a popular logic puzzle heaven-hell:

http://www.crazyforcode.com/heaven-hell-puzzle-2/

As far as my reach of my knowledge on clpb, I am afraid it is not easy for us.

I knew a general answer in a text book by Hidaka 1997 in Japanese written as an
example of applications of solutions of system of boolean equations, which uses
a well-known and fundamental but a little bit lengthy normal form theorem with
heavy use of "co-factoring."

As for me, with a little hope, I am trying to find a simple solution applying my rozdd builder
without resorting to that theorem. It is a kind of brain storming.

Kuniaki Mukai

[Kuniaki Mukai]

For the puzzle, I have managed to handle my rozdd builder
to produce the required boolean sentence in the form of a rozdd:

if(2, if(1, true(0), false), true(0)) .

This rozdd reads 2*1 + not(2)*not(1) (Do you live here ?)

I am sorry not to explain mysterious symbols here, though I would like to
do so if requested.

I am not sure where to go from here; I have found myself no to be so interested in
solving other puzzles.

?- init_rozdd,
Fxyq = (\(2) + (\(3) + 1)*(3+ \(1))) *
(2 + (\(3) + \(1))*(3+1)),
bdd_solve([
prop(Fxyq, Root),
{ getbdd(Root, if(X, L, R)) },
meet(L, R, false),
sum(L, R, true(2)),
neg(R, NegR),
sum(L, NegR, Ans)]),
bdd_to_tree(Ans, Anstree).


Fxyq = (\2+(\3+1)*(3+ \1))*(2+(\3+ \1)*(3+1)),
Root = 27,
X = 3,
L = NegR, NegR = Ans, Ans = 25,
R = 26,
Anstree = if(2, if(1, true(0), false), true(0)) .
(Do you live here ?)

Kuniaki Mukai

[Harry Stoteles]

Error 404, puzzle not found.

[Kuniaki Mukai]

Hi

I think the posted solution to the heaven-hell-puzzle  is  for a special simple case 

of a system of boolean equations with a single  unknown propositonal variable which 

is to be represented in other variables.

With this small success,  I would like to step  forward to handle rozdd  for 

more general cases of a system of boolean equations. 

However,  boolean constraint sounds for me now almost equal to  

a system of boolean equations, which  means that the current boolean constraint library clpb

must be  already  a solver for that because of its name.  If it is the case, 

I have to be very sorry for such ignorance.

Kuniaki Mukai

[Kuniaki Mukai]

Hi 

Let me put differently my question on rozdd and boolean constraint.

I have learned recently a general theorem on the normal form of  solutions for boolean equations. 

The theorem  seems a well-established classical theorem and also a  powerful tool for wide applications.

I am  ashamed of having been playing around boolean constraint so far  without paying little attention

to such a classical result.

Now my question is:  what is a relationship between rozdd and the classical normalization theorem ?

I guess they have  tight connections, which is only my hope for the time being 

without confidence.  

I will appreciate any comments on my  question for not reinventing wheel.

Kuniaki Mukai

[Harry Stoteles]

error 404, theorem not found

What do you want to do exactly? CLP(X) for B is relatively easy.
One way is to do it as follows:

- you have a predicate sat/1 that states some boolean expressions.
- you have a predicate labeling/1 that takes the conjunction
   of all states boolean expressions, and tries to find solutions
    for these, and displays the instantiations of the boolean variables.
- if you don't use the predicate labeling/1 the top level will
   show the stated boolean expressions.

This is all indepedented whether you use RZODD or something
else. The definition is along boolean expressions. Which have
an easy truth table defined satisfiability. Which is:

    A B  A*B      A ~A
   ------------      -------
    0 0   0          0 1
    0 1   0          1 0
    1 0   0     
    1  1  1   

The above framework is easy enough for novices, and well
suited for typical puzzler and puzzles. Of course more and more
could be done. I guess Intel would be not interested in

this simple framework, since Intel does probably not only
do puzzling. But your thread has the title puzzle in boolean
constraints, so I guess this is it. A puzzle is problem that

demands a solution. A boolean puzzle is a boolean problem
that demands a boolean solution. You can also call it SAT,
you can name the sat/1 formulae constraints, but

this is just naming cosmetics...

[Harry Stoteles]

Here is a collection of simple boolean puzzzles,
why are the following fallacies?Affirming a Disjunct: (p v q) & p => ~q.
Affirming the Consequent: (p => q) & q => p.
Commutation of Conditionals: (p => q) => (q => p).
Denying a Conjunct: ~(p & q) & ~p => q.
Denying the Antecedent: (p => q) & ~p => ~q.
Improper Transposition: (p => q) => (~p => ~q).

Well go to your local grocery (SWI-Prolog) and buy
the appropriate bread (CLP(B)). It will give you the
answer why these are fallacies, just ask for the satisfiability

of the negation. Here is an example run:

Welcome to SWI-Prolog (threaded, 64 bits, version 7.7.8)
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

?- use_module(library(clpb)).
true.


?- sat(~((P + Q) * P =< ~Q)).
P = Q, Q = 1.

?- sat(~((P =< Q) * Q =< P)).
P = 0,
Q = 1.

?- sat(~((P =< Q) =< (Q =< P))).
P = 0,
Q = 1.

?- sat(~(~(P * Q) * ~P =< Q)).
P = Q, Q = 0.

?- sat(~((P =< Q) * ~P =< ~Q)).
P = 0,
Q = 1.

?- sat(~((P =< Q) =< (~P =< ~Q))).
P = 0,
Q = 1.

Interesting observation, all examples work without labeling.
The built in unit propagation of the CLP(B) solver does
already the job. If you have more variables and/or different

problems, you would need labeling/1. For what is
unit propagation, see for example the original DPLL
algorith. You would get an idea what it is. I don't know how

to formulate it for RZODD. For BDD there are different
options to do it. I have opted for one of the ways to do it,
which gives a rather large applicability of unit propagation.

https://en.wikipedia.org/wiki/DPLL_algorithm#The_algorithm

If you would have a prototype that gives you labeling for
your RZODD, we could start also talking about unit propagation.
I remember that original, when the whol RZODD discussion

started it was all about labeling, the Markus Triska Link
showed a problem of the attributed variable framework with
labeling constraints. Meanwhile we were going algebraic,

to be able to count an example, but maybe for puzzling we
should go back to the roots of Markus Triska Link with mention of
Shin-ichi Minato paper. This was some months ago in  2017.

[Harry Stoteles]

Here is more examples what unit propagation
can do. The last two examples show, that my
heuristic is variable order dependent:

/* no unit propagation, impossible */
?- sat(X+Y+Z).
sat((X->1;Y->1;Z->1;0))

/* unit propagation, same as possible */
- sat(X*Y*Z).
X = 1,
Y = 1,
Z = 1

/* unit propagation, same as possible */
?- sat(X*(Y+Z)).
X = 1,
sat((Y->1;Z->1;0))

/* no unit propagation, despite possible */
?- sat((Y+Z)*X).
sat((Y->(X->1;0);Z->(X->1;0);0))

The used unit propagation is one single Prolog code line,
in  the SAT solver. The line reads as follows:

sat_propagate(node3(X,_,_,zero)) :- !,

var_map_back(X, Y),

    Y = 1.
https://github.com/jburse/jekejeke-devel/blob/master/jekmin/headless/jekmin/reference/finite/clpb.p#L126

[Harry Stoteles]

Maybe if trees would be used with some automatic
variable reordering (there seem to be such algorithms),
as a side effect/benefit a larger class of units could be

detected, by simple pattern matching. If the units
would be ordered to the front, then this would do the
job. Maybe with variable reordering, automatic,

also the problem(7), problem(8), would get a more
compact representation. Not sure. If the units are
move to the front, one sees immediately that the

expanded trees are smaller. Not sure whether
with common subexpressions, we could still say
that the tree is smaller. But examing the root of

a tree for a unit, is much simpler, than searching
the whole tree whether it has a unit somewhere.
This is why I am using this heuristic, its a very

cheap heuristic, that doesn't slow down the solver.

[Kuniaki Mukai]

Hi Harry, 

Thank you for response.  Your summary  has made certain that I am more interested in 

solving a boolean equation than encoding the set of  of solutions of constraints (truth table).

Kuniaki Mukai

--
You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.
To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+...@googlegroups.com.
Visit this group at https://groups.google.com/group/swi-prolog.
For more options, visit https://groups.google.com/d/optout.

[Kuniaki Mukai]

Seeing your post, I could not stop running my rozdd builder for myself.

% ?- prop(((A->B)*(B->C))->(A->C)), card(N).

%@ N = 8 .

% ?- prop(\(((A->B)*(B->C))->(A->C))), card(N).

%@ N = 0 .

Indeed, it is a model theoretic proof for the proposition (A->B) * (B->C)  -> (A->C).

Almost twenty years ago, I wrote a simple cgi in SWI on Gentzen 

style prover for *classical* proposinal logic. It still works. 

For example the following is a copy of the output proof tree (upside down).

(a>b)*(b>c)>(a>c) is provable in LK.

                        |- (a>b)*(b>c)>(a>c)                           

                      -----------------------(|->)                     

                         (a>b)*(b>c) |- a>c                            

                        --------------------(*|-)                      

                          a>b, b>c |- a>c                              

         --------------------------------------------------(>|-)       

          b>c |- a, a>c                      b, b>c |- a>c             

---------------------------------(>|-) --------------------------(>|-) 

  |- b, a, a>c       c |- a, a>c        b |- b, a>c  c, b |- a>c       

---------------(|->)--------------(|->)             --------------(|->)

  a |- c, b, a       a, c |- c, a                    a, c, b |- c      

Sorry for this irrelevant post.  

Kuniaki Mukai

On Feb 7, 2018, at 22:05, Harry Stoteles <in...@xlog.ch> wrote:

[Harry Stoteles]

An LK calculus is certainly not irrelevant. But a LK calculus
is designed to enumerate tautologies. You can test tautology
by a SAT solver by this query:

   ?- term_variables(F,L), \+ (sat(~F), labeling(L)),

If the above query says Yes, then F is a tautology. If the
above query says No, then F is not a tautology. But you
will not know whether its antilogy though, you would
need to check this separately.

You can try it yourself, try SWI-Prolog CLP(B) or
any other SAT solver. Here are 192 test cases from

    192 principia mathematica test cases:
    https://gist.github.com/jburse/99d9a636fd6218bac8c380c093e06287#file-principia-p

Example test case from above:

    Test case from principia mathematica:
    case('3.3', 'Exp (GB 63=>59)', (p&q=>r)=> (p=> (q=>r))).

Verification with a SAT solver (using CLP(B) from SWI-Prolog):

    Welcome to SWI-Prolog (threaded, 64 bits, version 7.7.8)
    SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software.

   ?- use_module(library(clpb)).
   true.

   ?- F=((P*Q=<R)=< (P=< (Q=<R))), term_variables(F,L), \+ (sat(~F), labeling(L)).
   true

    SWI-Prolog Predicate taut/2 documentation
    http://www.swi-prolog.org/pldoc/doc_for?object=taut/2

But in SWI-Prolog, you can also use the predicate taut/2, this is
probably easier and faster. Here are some examples using taut/2:

   ?- taut(P, A).
   false.

   ?- taut((P*Q=<R)=< (P=< (Q=<R)), A).
   A = 1

The predicate taut/2 checks whether a formula is a tautology (A=1) or
an antilogy (A=0). I never looked up how Markus Triska has implemented
the predicate, and its currently also not part of my CLP(B) library. Since
it is kind of a redundant predicate, when there is alraedy sat/1 and labeling/1

as shown above. But there are again similar tricks like with counting, doing
it algebraically, to make it faster than using sat/1 and labeling/1 as above,
so I guess this is the reason why a taut/2 predicate might exist in a SAT
solver parallel to other predicates...

[Kuniaki Mukai]

Thanks. I could easily  imagine what were done already on such topics.

Now I am interested in solving equations, which is more fresh for me. Thank you for

turning me for that direction.   If I meet luckily something interesting for me

and possibly for  this forum, it would be my great pleasure to post it.

Kuniaki Mukai

[Harry Stoteles]

I wouldn't count determining tautologies as "puzzles" for the every
day newspaper reader riddle section person. If you look at the
SAT solver formulation, you see it has a negation.

But a riddle section person wants to do something, you should
give him a problem (sat/1) and then he needs to fiddle around
(labeling/1), when sitting in the train during his daily commute,

(I have a friend who does sodoku(*) during his daily commute). So
I guess just (sat/1) and (labeling/1) would be a very nice addition
to your RZODD library, and it would make people feel comfortable

that already know SWI-Prolog CLP(B).

(*)
Sodoku was first popular in Japan, but it got spread to Europe,
newspapers now printing riddles every week:
http://sudoku.tagesspiegel.de/

[Harry Stoteles]

But this fever was 10 years ago:

Akte 06 Sudoku DM 2007 Teil1
https://www.youtube.com/watch?v=GAENH00NMfo

[Harry Stoteles]

You could also make empirical research with real world
persons and look what solving strategies they apply.
For example new SAT solvers, that have some conflict
learning, this seems to be a very natural behaviour,

which is also seen whan a person solves a sudoku. On
the other hand the mathematical equation solving, did
need some time to develop, maybe Vieta (1540 - 1603)
made some leaps here, he introduce calculating with

symbolic letters, instead only with numbers. He
was Code-breaker to two kings:

He then ended the algebra of procedures (al-Jabr and Muqabala),
creating the first symbolic algebra and claiming that with it,
all problems could be solved (nullum non problema solvere).
https://en.wikipedia.org/wiki/Fran%C3%A7ois_Vi%C3%A8te#A_new_algebra

But I don't know how the history goes in Japan culture.
They probably tell other stories there...

[Harry Stoteles]

boolean equations are especially simple, since
equality is the same as biconditional:

    A  B  A = B                  A B A <->B
   ----------------               ------------------
    0 0      1                       0 0     1
    0 1      0                       0 1     0
    1 0      0                       1 0     0
    1 1      1                       1 1     1

But I consider my BDD SAT solver (and somehow also
your RZODD prototype), still stupid. Why can
it not solve problem(8) much faster, when there
are so many symmetries. One answer might be

that the stupid solver neither sees nor applies laws like
for example this law, substitution of equals by equals:

    s = t /\ A(s) -> A(t)

Which also holds for boolean equations, or written
with biconditiona, we would have:

    p <-> q /\ A(p) -> A(q)

Even your propositional LK calculus from Gentzen
doesn't use this law, since it doesn't use higher order
logic. But this law was already catalogued  by
Gottlob Frege, it seems, have seen few propositional

provers seen so far, trying to explore it.

For Gottlob Frege, see here (numbered
page 340 Law Nr. 56 and 57):

C. Propositional Laws from the Begriffschrift,
History of formal logic
by Bochenski, Joseph M.
https://archive.org/details/historyofformall00boch

[Harry Stoteles]

There is a similar law with positive
and negative occurence:

       p -> q /\ A+(p) -> A+(q)

So a prover could see (your example):

      B->C /\ A->B -> A->C

In blink. Didn't you know that
already, Kuniaki Mukai?

[Harry Stoteles]

This could be a bridge in explaining the pure step of the
DPLL algorithm. I see the pure step for the first time.I
think I remember only an old wikipedia or an old reading

of DPLL algorithm, which had only the unit step. But
the pure step is also interesting, and I implemented something
also for my solver. Wikipedia says for the pure step:

  for every literal l that occurs pure in Φ
      Φ ← pure-literal-assign(l, Φ);

https://en.wikipedia.org/wiki/DPLL_algorithm#The_algorithm

My SAT solver has a pure step detection and elimination,
respectively the Gottlob Frege cataloged Law, as follows,
in the sense that it does apply it:

   ?- sat(C+D), sat(A=<B).
   sat((C->1;D->1;0)),
   sat((A->(B->1;0);1))

   ?- sat(C+D), sat(A=<B), B=C.
   B = C,
   sat((C->1;D->1;0)),
   sat((A->(C->1;0);1))

The substitution is implemented via the existential
quantifier, so I compute A[X/Y] as follows:

      A[X/Y] := exists X(A /\ X <->Y)

     /* or in the SWI-Prolog CLP(B) notation itself */

      A[X/Y] := X^(A*(X=:=Y))

Markus Triska does also something. You find a similar
behaviour with SWI-Prolog CLP(B), But I dont recognize
the replacing A=<B by A=<C structurally:

    ?- sat(C+D), sat(A=<B).
    sat(C=\=C*D#D),
    sat(A=:=A*B).

   ?- sat(C+D), sat(A=<B), B=C.
   C = B,
   sat(1#B*A#A),
   sat(B=\=B*D#D).

I think Markus Triska uses the variable ordering differently,
and instead replaces C+D by C+B. But why A=<B is now
shown differently I don't understand, but the two displays
are equivalent:
      
   ?- sat(A=:=A*B), labeling([A,B]), write(A-B), nl, fail; true.
   0-0
   0-1
   1-1
   true.

   ?- sat(1#B*A#A), labeling([A,B]), write(A-B), nl, fail; true.
   0-0
   0-1
   1-1
   true.

Maybe the display differs since Markus Triskas CLP(B) doesn't
not guarantee a canonical display. On the other hand I always
display the normalized BDD. Or its a canonical form that can differ,

again because of some subleties of variable ordering. I would
love to implement more, than only the X=Y pure step. Like do
something for positive and negative occurence.

But this seems harder, also propagation wise, an X=Y can be
easily propagate via the Prolog unification, and you only need
a attributed variable hook that does the right thing...

[Kuniaki Mukai]

I have continued with some additional test on the rozdd builder of mine
as a helper for solving the hell-heaven puzzle.

The method of solution should be well-known in the literature
on boolean algebra; the general form of solution
to a boolean equation

a*x + b = 1 (=true).

Integers 1,2,3,4 are for propositional variables intended
to be:

1 -- "you are honest."
2 -- "you come from overthere."
3 -- target question to be constructed.
4 -- as an arbitrary parameter in solution.

Note that 'you' and 'overthere' is indexicals,
which I have to skip to explain.

\ -- negation
+ -- disjunction
* -- conjunction
which are as usual.


bdd_solve/1 -- handler for rozdd builder.

Query:
?- init_rozdd,
Hell_Heaven_Problem =
(\(2) + (\(3) + 1)*(3 + \(1))) *

(2 + (\(3) + \(1))*(3 + 1)),
bdd_solve([

prop(Hell_Heaven_Problem, Root),

{ getbdd(Root, if(X, L, R)) },

adjust(L, R, L0, R0),
meet(L0, R0, Meet),
neg(R, NegR)]),
bdd_to_tree(L, Ltree),
tree_to_prop(Ltree, LProp),
bdd_to_tree(NegR, Rtree),
tree_to_prop(Rtree, RProp),
General_Sol_of_Hell_Heaven = 4 * LProp + RProp.

The output:

Hell_Heaven_Problem = (\2+(\3+1)*(3+ \1))*(2+(\3+ \1)*(3+1)),

Root = 27,
X = 3,

L = L0, L0 = NegR, NegR = 25,
R = R0, R0 = 26,
Meet = false, % <== checking necessary condition for the existence of solutions.
Ltree = Rtree, Rtree = if(2, if(1, true(0), false), true(0)),
LProp = RProp, RProp = 2*(1*true(0)+not(1)*false)+not(2)*(not(1)*true(0)),
General_Sol_of_Hell_Heaven = 4*(2*(1*true(0)+not(1)*false)+not(2)*(not(1)*true(0)))
+ (2*(1*true(0)+not(1)*false)+not(2)*(not(1)*true(0))) .

If we take the parameter 4 to be false, then we have

2*1 + not(2)*not(1)

as a standard answer for the puzzle.

For summary, I have found the rozdd handler works well as I expected,
at least for the hell-heaven puzzle, though details much remain
to be explained, for which I am sorry.

Kuniaki Mukai

[Harry Stoteles]

Warning this is not the solution you want. You want to solve for
A,B. But here in Europe we usually solve for the X. Well
the equation:

      A*X + B = 1,

has only a solution in the following A,B situation:

?- sat(X^(X*A+B =:= 1)), labeling([A,B]), write(A-B), nl, fail; true.

0-1
1-0
1-1
Yes

Depending on the A,B situation, the X solution is then:

?- sat(X^(X*A+B =:= 1)), labeling([A,B]), write(A-B), 
       (sat(X*A+B =:= 1), labeling([X]), write(+X), fail; true), 
       nl, fail; true.
0-1+0+1
1-0+1
1-1+0+1
Yes

The above solution uses the boolean existential quantifier. Did you
already implement it algebraically for ROZDD? The existential
quantifier is specified here:

Var ^ Expr existential quantification
CLP(B) for SWI-Prolog
http://www.swi-prolog.org/pldoc/man?section=clpb

You can draw the following analogy. For quadratic equations there
is the determinant, which says when there is a solution. With the
help of existential quantifier you can determine the same.

BTW: Tarskis famous equation solver is also a
quantifier elimination (QED) algorithm.

The QED algorithm for BDD is especially simple. You can
use the following rules, which you probably will
immmediately agree on:

   X^(if-then-else(X,A,B))    :<=>  A \/ B

   X^(if-then-else(Y,A,B))    :<=> if-then-else(Y,X^A,X^B)   for X and Y different

[Harry Stoteles]

Do you mean given C,D solve for X,Y such that:

    X*C + Y = D  ?

[Harry Stoteles]

But lets get back to A*X+B = 1. Usually if a SAT solver can take
such a formula, convert it to a tree and normalize the tree, then
you have already solved the equation,

there is nothing to do anymore.

The SAT solver has already create a solved form, that has
completely determined whether the equation has a solution
and what solution the equation has.

The only thing that is left to do, is maybe some variable
reordering. Here is variable reordering done in a typical
SWI-Prolog like CLP(B) solver,

the variable ordering is the input order, so I will not
input A*X+B = 1, but write X last. So I will for example
input 1 = B + A*X. Lets see what we get:

?- sat(1 =:= B + A*X).
sat((B->1;A->(X->1;0);0))

Lets see whether it encodes these solutions:

?- sat(1 =:= B + A*X), labeling([B,A,X]), 
   write(B-A-X), nl, fail; true.
0-1-1
1-0-0
1-0-1
1-1-0
1-1-1
Yes

The resulting if-then-else tree was (B->1;A->(X->1;0);0). You
can easily veryify that it encodes the above table. To view the
if-then-else tree in SWI-Prolog you need to do:

?- set_prolog_flag(clpb_residuals, bdd).
true.

It then uses the same variable ordering, as in my system.
At least I then get:

?- sat(1 =:= B + A*X).
clpb:'$clpb_bdd'([
node(4)-(v(B, 0)->true;node(3)),
node(3)-(v(A, 1)->node(2);false),
node(2)-(v(X, 2)->true;false)]).

[Kuniaki Mukai]

given a boolean equation,  for example, 

a*x + b*y = 1 

find a most general boolean forms f(a,b) and g(a,b) such that 

      a*f(a,b) + b*g(a,b) = 1

 

is true for all possible assignments. Of course,

it is necessary to find a condition on a b for such solutions.

I am currently trying  to use a rozdd for  such given equation

to  find general form of  f(a,b) and g(a,b).  

Anyway, I thought  what I am playing around is far from new, 

but well-known to  rozdd people like you.  So your long comments were 

only strange to  me. 

Kuniaki Mukai

[Harry Stoteles]

Order variables, A, B, X, Y, compute your tree. The tree
will be a partial and/or multi-value function h(A,B)={<X,Y>},
that give you for an <A,B> value pair, some <X,Y> value pairs.

As a final step use the existential quantifier, if you would
have one in your ROZDD library, and computed the
following two new trees from the tree you already computed:

        X^(A*X+B*Y =:= 1)  == exists X (h(A,B)={<X,Y>})

                                        == g(A,B)={Y}

        Y^(A*X+B*Y =:= 1)  == exists Y (h(A,B)={<X,Y>})

                                        == f(A,B)={X}

The functions above are partial and/or multi-valued functions.
How to get formulas you can plug in? Well we would
need to order the variables again differently. Namely
we would need to have the variable X at the beginning

so that we get a tree as follows:

      f(A,B,X) = if-then-else(X,P,Q)

Now this is logically equivalent to:
 
     (X -> P) /\ (~X -> Q)

This is not a biconditional X <-> F aka X = F, so it doesn't
give a value for X. Can we turn it into a formula that gives
sometimes a formula? So you cannot get f(a,b) and
g(a,b) solutions. You can only get something along:

      k(a,b) ->   a*f(a,b) + b*g(a,b) = 1

You have to think about side conditions from the
beginning. But I already showed in another post
how the side condition k(a,b) can be found, again
its using the existential quantifier:

      k(a,b) == X^Y^(A*X+B*Y =:= 1)

Now there remains still a problem. You would need
a choice functions. Now in the presence of the
side condition, for the remaining input range, the
functions f and g are not anymore partial,

they are now total, but still they can be multi value.
How to turn a multi value functions into a single value
functions in a SAT solver. I dunno. There are many
many ways to make the multi value f and g,

single value. This is related to the problem of:

https://en.wikipedia.org/wiki/Equisatisfiability

Here is my guess, what maybe could be automatized,
for a multi valued function i, to get a single valued function j:

    If i(A,B) = {0}       do nothing,        j(A,B) := {0}

    if i(A,B) = {1}       do nothing         j(A,B) := {1}

    if i(A,B) = {0,1}    choose zero?    j(A,B) := {0}

Is there a well known manipulation of trees, that
gives this haircut? Well the last situtaion, if we look
at the if-then-else tree, is the situation:

     P /\ Q

This situation is computed by the forall quatifier,
so the multi valued situation is basically:

    ~(X^(~f(A,B,X)) == P /\ Q

Can we reshape f(A,B,X) to then return only zero?
Well yes, that is easy, just use the modified if-then-else:

      (X -> P /\ ~(P /\ Q)) /\ (~X -> Q) ==

      (X -> P /\ ~Q) /\ (~X -> Q)

The above is an Equisatisfiable tree. This is related
to the short-cut disjunction and conjunction found in programming
languages. I already experimented withn this Equisatisifability
trick for my problem(7), problem(8), etc.. but it doesn't yield

anything. What operator gives you this short cutted formula.
I dunno. Let me post about a short cut operator in another
post. I have to think first how this could be obtained via

logical operators. Thats an interesting problem. but unfortunately
as my empirical research showed, its not relevant to my
problem(7), problem(8). So we are back to square zero...

[Harry Stoteles]

So the bottom line of my post is, you need to find a short cut
operator, to solve equations, which does for example for you:

    If i(A,B) = {0}       do nothing,        j(A,B) := {0}

    if i(A,B) = {1}       do nothing         j(A,B) := {1}

    if i(A,B) = {0,1}    choose zero?    j(A,B) := {0}

Or maybe they do something else, like settig j(A,B) := {1},
or even something variying. Such transformations are
called Equisatisfiability transformations. The wiki doesn't show
a very useful example.

https://en.wikipedia.org/wiki/Equisatisfiability

I don't know whether your cryptic code has such an short cut
computation somewhere, maybe in your bdd_solve ? Who knows
its a black box. What would be needed is something that computes
single valued boolean function from a multi valued functions,
so that you can solve:

      k(a,b) ->   a*f(a,b) + b*g(a,b) = 1

You would need to explain your code in more detail.
Here is another Equisatisfiability transformation, that
can be easily explored with a CLP(B) SWI-Prolog like
SAT solver, on the toplevel. The identity is:

         A /\ B     == A /\ (~A \/ B)

Here is a part of my problem(7), trying this Equisatisfiability
transformation, we see it gives the same solutions:

?- A=X*U#Y*V, B=X*W#Y*T, sat(A), sat(B), labeling([X,Y,U,V,W,T]), write(X-Y-U-V-W-T), nl, fail; true.
0-1-0-1-0-1
0-1-0-1-1-1
0-1-1-1-0-1
0-1-1-1-1-1
1-1-0-1-0-1
1-1-0-1-1-0
1-0-1-0-1-0
1-0-1-0-1-1
1-0-1-1-1-0
1-0-1-1-1-1
1-1-1-0-0-1
1-1-1-0-1-0
true.

?- A=X*U#Y*V, B=X*W#Y*T, sat(A), sat(~A+B), labeling([X,Y,U,V,W,T]), write(X-Y-U-V-W-T), nl, fail; true.
0-1-0-1-0-1
0-1-0-1-1-1
0-1-1-1-0-1
0-1-1-1-1-1
1-1-0-1-0-1
1-1-0-1-1-0
1-0-1-0-1-0
1-0-1-0-1-1
1-0-1-1-1-0
1-0-1-1-1-1
1-1-1-0-0-1
1-1-1-0-1-0
true.

But I don't get some speed-up. The fastest is when I compute a
single tree, i.e. if I don't use DPLL like algorithm two different sat/1, but
only a single sat/1 constraint, where we are back to
your ROZDD prototype:

?- A=X*X#Y*Y#Z*Z, B=X*P#Y*Q#Z*R, term_variables((A,B),L), sat(A*B),
    time((between(1,1000,_), labeling(L), fail; true)), fail; true.
% 9,642,001 inferences, 0.703 CPU in 0.703 seconds (100% CPU, 13713068 Lips)
true.

?- A=X*X#Y*Y#Z*Z, B=X*P#Y*Q#Z*R, term_variables((A,B),L), sat(A), sat(B),
    time((between(1,1000,_), labeling(L), fail; true)), fail; true.
% 9,642,001 inferences, 0.719 CPU in 0.719 seconds (100% CPU, 13414958 Lips)
true.

?- A=X*X#Y*Y#Z*Z, B=X*P#Y*Q#Z*R, term_variables((A,B),L), sat(A), sat(~A+B),
    time((between(1,1000,_), labeling(L), fail; true)), fail; true.
% 10,169,001 inferences, 0.750 CPU in 0.750 seconds (100% CPU, 13558668 Lips)
true.

?- A=X*X#Y*Y#Z*Z, B=X*P#Y*Q#Z*R, term_variables((A,B),L), sat(~B+A), sat(B),
   time((between(1,1000,_), labeling(L), fail; true)), fail; true.
% 15,375,001 inferences, 1.094 CPU in 1.094 seconds (100% CPU, 14057144 Lips)
true.

Why do I still research DPLL algorithm? Well together with
Equisatisfiability it is said to use only O(n) space. This means
bigger and bigger problems like problem(7), problem(8), etc..

can be solved. The only problem is that it is also O(2^n) in
time. And in the face of the hardness of the SAT problem in
general, maybe nothing can be done for problem(7), problem(8), etc..

Maybe if we would try some develoment from MiniSat, like
clause learning we could tear down one barrier...

[Harry Stoteles]

If you have two variables, you need to do the choice,
so that you don't exclude one variable from the other.

So better do the choice on the function multi-value
function h(A,B)={<X,Y>}. So you would need to
think about a choice for a tree:

     if-then-else(X,if-then-else(Y,P1,Q1),if-then-else(Y,P2,Q2))

If you do a choice indepently for X and Y, the choices
might not fit together. You might not get f(A,B) and g(A,B)
that work together.

[Kuniaki Mukai]

Hi Harry,

I am afraid that it would  take much time for me to understand your idea posted in long.

Instead, I would like to try for myself to understand the general case of solving 

boolean constraints consulting published literature available at hand.

I hope it would be achieved by simple recursive  application of what I have done 

in the hell-heaven puzzle,  though I am far from sure.  

Kuniaki Mukai

[Boris Vassilev]

> your idea posted in long.

The ideas are flowing, so he's just writing them down.

Save our in-boxes! http://emailcharter.org

To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.

Visit this group at https://groups.google.com/group/swi-prolog.
For more options, visit https://groups.google.com/d/optout.

--
You received this message because you are subscribed to the Google Groups "SWI-Prolog" group.

To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+unsubscribe@googlegroups.com.

[Harry Stoteles]

The problem is that you require (truth) functions f(a,b) and g(a,b), but
BDD trees and other trees basically define relations over their
boolean variables, R(x1,..,xn). So you are faced with two problems

to get from a relation to a functions, namely a relation R'(S,T)
is a functions, lets use the armstrong arrow S -> T, when we have:

   Existence:
         forall S exists T R'(S,T)

   Uniqueness:
          forall S,T,R R'(S,T) & R(S,R) -> T=S

So basically for a problem R(A,B,X,Y), you want to find
R'1(A,B,X) whit armstrong arrow A,B -> X and R'2(A,B,Y)
with armstrong arrow A,B -> Y.

One alternative strategy would be:

- The uniqueness requirement above leads to the idea of
   implementing some choice. But we need to think for
   choices in R'1 and R'2 based on R, which ties X and Y together.

- But here is a new idea from just now, instead of solving the
  problem in one step. Just do it step-wise. We could also
  do the following:

      1) First fix a choice for R'1 so that there is always also some Y.
           Hint use existential quantifier and the if-then-else formula I
           already showed which gives you X <-> P /\ ~Q.

      2) Then consider the new problem:

                 R'1(A,B,X) /\ R(A,B,X,Y)

          and fix a choice for R'2. You can use again existential quantifier
          and the if-then-else formula I already show which gives you
          X <-> P /\ ~Q.

You should like the choice X <-> P /\ ~Q, since it prefers zeros and could
be helpful for ROZDD, since ROZDD are zero supressed. I don't use
RZODD, I only use BDD. But you might find remarks in Minatos Paper,
for example about boolean don't care variables etc..

The new algorithmic idea above, to do a step-wise refinement so
that all variables are taken care of, with the tools that we have already
developed, i.e. existential quantifier and X <-> P /\ ~Q to prefer zeros
through a choice anlong don't care variables, is in the spirit of

this step-wise refinement:

"In total, n+1 runs of the algorithm are required,
where n is the number of distinct variables in Φ."
https://en.wikipedia.org/wiki/Boolean_satisfiability_problem#Self-reducibility

The armstrong arrow is from here:
https://en.wikipedia.org/wiki/Armstrong's_axioms

During your literature search, you might want to search for boolean
don't care variables. When you assume a function f(a,b) and g(a,b),
you don't care anymore about all possible values of X and Y, you just
want to give X and Y some value, this is why your problem formulation,

probably not intended by you, leads to don't care variables.

[Harry Stoteles]

By don't care I don't mean boris.vassilev, who repastes the
same link again and again, nobody knows why he thinks
this adds something to the discussion. Obviously it doesn't.

By don't care I mean a subtopic inside SAT solvers, which
you might find papers about, and which you get into since
your functions f(a,b) and g(a,b) overshadow X and Y:

Example paper:

Managing don't cares in Boolean satisfiability

"Don't care sets are addressed in this work both statically
and dynamically to reduce the search space and guide
the decision making process."
Sean Safarpour, Andreas G. Veneris, Rolf Drechsler,
Joanne Lee - Published 2004 in

Proceedings Design, Automation and Test in

I tried yesterday something with SWI-Prolog CLP(B). SWI-Prolog
CLP(B) has two kinds of variables in its SAT Solver. You can
also use lower case Prolog atoms.

But I couldn't get something with don't care and your equational
problem Kuniaki Mukai . It seems that the lower case Prolog
atoms in the SWI-Prolog CLP(B) serve another purpose,

I guess they are universally quantified or something like this.
Maybe need an expert with don't care variables. Actually I
don't don't care about don't care variables, since this is related

to equisatisifiability and can speed up the search. But I am not
an expert in the field of don't care variables. Again its not because
I don't care, but rather because I leave it to others to be the

Leonardo Davici of SAT Solvers...

[Harry Stoteles]

Corr.: ... leave it to others to be the
Leonardo Davincis of SAT Solvers...

Maybe this name could be a good entry point for
non-puzzles hobbyst SAT solving:

https://de.wikipedia.org/wiki/Rolf_Drechsler

[Harry Stoteles]

There are companies that are specialized in using SAT
solver to optimize logic circuits and take advantage of

don't care states. Modern CPUs would be much larger
and consume more power without such tricks. You can

also have don't care states in temporal development of
a boolean system, that has feedback loops, flip-flops, etc...

Etc.. Etc... looks pretty non-puzzle non-hobbyst to me.
Disclaimer: Don't buy stocks based on what I wrote...

[Harry Stoteles]

So if you choose zero, and zero is that state that consumes
less power, then zero is the preffered choice.

But don't choose zero, if zero is -12 volts, and one is 0 volts,
then maybe better choose one. He He

[Harry Stoteles]

I guess "save our in-boxes!" and "save my in-boxe!",
is also demonstratably not _exactly_ the same thing.

Boris Vassilev schrieb (to my personal in-box, sic!):

> > By don't care I don't mean boris.vassilev, who repastes the
> > same link again and again, nobody knows why he thinks
> > this adds something to the discussion. Obviously it doesn't.
>

> The link is a part of my email signature. I appologize for forcing it upon you.
>
> And "nobody knows why he thinks...": you probably mean "I don't know
> why he thinks... " which is
> demonstratably not _exactly_ the same thing.
>
> Cheers,
> Boris

>
>
>
> Save our in-boxes! http://emailcharter.org

[Harry Stoteles]

One more question, why use an Email charter footer, for
responses to a Newsgroup. Doesn't make any sense.

[Harry Stoteles]

Since 1995 there exists graphic browsers (Mosaik etc..), now
I do something that your Email charter forbids, including an attachment,

but this is to show that you could use an URL, and then use the
google web reader, which will allow you to easily click into what

interests you, and ignore the rest. The ignore the rest works not
if you want to molest somebody. But well you got the idea.

[Harry Stoteles]

I still don't understand why "Email style" is refered to, and why
brainstorming should be forbidden. After all the OP, Kuniaki Mukai,
does brainstorming all the time. All his posts are brainstorming
of his ongoing development. So according to your logic they are

all polution. Maybe SWI-Prolog, which is also an ongoing development
is also polution. Please consult the header of the inline image
of my previous post, to read the charter of this newsgroup. I can
copy it here for you:

"Welcome to the SWI-Prolog discussion forum.  Please use this
forum to (1) ask questions how to solve programming problems
in (SWI-)Prolog, (2) ask questions about porting and installation,
(3) discuss best practices for applying Prolog, (4) announce your
great library, application, etc., (5) discuss the future of (SWI-)Prolog or
other topics of interest to the (SWI-)Prolog community."

So whats your best practice of CLP(B) or SAT Solving in Prolog to
solve Kuniaki Mukai problem? Are you even interested in this
problem, or only in harassing people because it is weekend and
you have nothing todo? Well I now better places to give in into this

impulse. I don't think Kuniaki Mukai and I will appreciate this
kind of contribution, namely cutting off the Brainstorming...

> A lot of things that make sense to one person make little sense
> to another person; that's just how it is. "Common sense" is a
> misnomer for sure.. For example, for me it makes no sense to
> write email after email after email, in a "stream of consciousness"
> style. Why not think about what you want to say, write it down,
> re-read it to make sure it's ready, then send?

>

> Even now, you somehow managed to split a 4-line response into
> 2 emails of 2 lines each :-(
>

> As to sending to your personal in-box: I really didn't want to pollute
> the space even more. I underestimated you; I appologize yet again.
>

> Cheers,

> Boris
>

> PS: A third email while I was still typing. I give up.

>

> Save our in-boxes! http://emailcharter.org

[Boris Vassilev]

Dear Harry,

When I said "pollution" I meant my first email on this thread. It was not on topic, completely unnecessary, and pure trash. I can't remember now what I thought is gonna happen; either way, I was wrong to send it.

I do not think that anything should be forbidden. I cannot forbid you to write emails, in any form, of any length and at any frequency. Just keep going for as long as you need to.

I apologize to you and to all innocent bystanders.

Best regards,

Boris

Save our in-boxes! http://emailcharter.org

[Harry Stoteles]

Nevertheless I consider our brainstorming a failure. It
seems to be rather repellent, about SAT Solving. Sorry for that.

Just saying, don't miss SAT Solving, its really fun, and
SWI-Prolog has a nice CLP(B) library. I am really currious

about the future, and what SWI-Prolog will offer...

To unsubscribe from this group and stop receiving emails from it, send an email to swi-prolog+...@googlegroups.com.

[Kuniaki Mukai]

I have slightly generalized  “heaven-hell-puzzle” into a boolean constraint solver

solve_boole_in_rozdd/5  below.

Currently the predicate eliminates only one unknown variable. 

All unknown variables must be eliminted, but I have no idea yet how to do so.

Also boole simplifier seems necessary outside rozdd.

?-   Hell_Heaven_Problem =

  (not(Y) + (not(Z) + Y)*(X + not(Y))) * (X + (not(Z) + not(Y))*(X + Y)),

solve_boole_in_rozdd([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol).

%@ Hell_Heaven_Problem =  (not(2)+(not(3)+2)*(1+not(2)))*(1+(not(3)+not(2))*(1+2)),

%@ Y = 2,

%@ Z = 3,

%@ X = 1,

%@ Cond_for_sol = 2*(1*true(0)+not(1)*false)+not(2)*(1*true(0)+not(1)*false),

%@ Sol =  (3=4*(2*(1*true(0)+not(1)*false)+not(2)*(1*true(0)+not(1)*false))+(2*(not(1)*true(0))+not(2)*(not(1)*true(0)))).

?-   solve_boole_in_rozdd([A], [Y,X], X*Y = A, Cond_for_sol, Sol).

%@ Cond_for_sol = 2*true(1)+not(2)*(not(1)*true(0)),

%@ Sol =  (3=4*(2*(1*true(0)+not(1)*false)+not(2)*(not(1)*true(0)))+(2*(1*true(0)+not(1)*false)+not(2)*(1*true(0)+not(1)*false))).

solve_boole_in_rozdd(KnownVars,

UnknownVars,

Problem,

Cond_for_sol_to_exists,

Solution) :-

init_rozdd,

append(KnownVars, UnknownVars, Vars),

zdd_solve([

newvars(Vars),

basic_prop(Problem, Problem0),

prop(Problem0, Root),

path_sum(UnknownVars, Root, Cond_zdd),

getzdd(Root, if(Elim_Var, L, R)),

neg(R, NegR),

newvars([U])]),

zdd_to_prop(L, LProp),

zdd_to_prop(NegR, RProp),

zdd_to_prop(Cond_zdd, Cond_for_sol_to_exists),

Solution = (Elim_Var = U * LProp + RProp).

p.s. 

According to Markus, rozdd is a canonical encoding of a truth set.

This idea drives me to the current post.  Personally I prefer

to say   rozdd is a universal covering of given 

propositional formula.  This analogy is often an unreasonable engine for me

to play around with poor knowledge on  SAT. Useful analogy, but 

I have no idea on that to explain to others. 

Kuniaki Mukai

[Harry Stoteles]

There is a very simple analog to Polynomial equations and boolean
algebra equations. You can use this operation mapping:

        Polynomial equation                Boolean algebra equation
        Addition                                    Xor
        Multiplication                            Conjunction
       
This was also the analog I used for my problem(7), with the
orthogonial vectors, why I came up with this problem. So what
makes a polynomial an boolean algebra equation then.

According to George Boole, its enough to add for each variable,
the side condition as follows:

        X^2 - X = 0

       /* check for yourself X^2 - X = 0, is the same as X*(X-1) = 0,
          is the same as X=0 or X=1 */

Since you have implemented already Gröbner Basis algorithm,
you should know what can be done now. I tryied this once, its
slower than a SAT Solver, but it works.

Here is the code, these are the side equations, the expression
Y is X^2 - X will compute a polynomial, I have overloaded the
(is)/2 operator:

bool([X|L], [Y|R]) :-

Y is X^2-X,

bool(L, R).

bool([], []).

This is the tautology checker based on Gröber Basis algorithm,
it simply check whether the given polynomial reduces completely
to zero, and is removed from the basis:

taut(F) :-

term_variables(F, L),

G is (~F),

bool(L, H),

sys_poly_groeb([G|H], R),

     R == H.

You find all logical operations defined as polynomial operations here:

https://gist.github.com/jburse/99d9a636fd6218bac8c380c093e06287#file-boole-p-L38

My testing notes say, it was already a year ago, 20 Mar 2017:

"Added 193+6 propositional logic problems as Boole polynomials.
Its much slower than Wangs algorithm, kind of 200x slower.

From testing I see that it also works with polynomial reduction
only, but I dont have a proof that S-polynomials are not needed."

https://gist.github.com/jburse/99d9a636fd6218bac8c380c093e06287#gistcomment-2032509

[Harry Stoteles]

Here is how George Boole comes up with the side condition:

"Let us adopt the same principle of notation here; for the mode of expressing a
particular succession of mental operations is a thing in itself quite as arbitrary
as the mode of expressing a single idea or operation (II. 3). In accordance with
this notation, then, the above equation assumes the form
       x^2 = x; (2)
and is, in fact, the expression of a second general law of those symbols by which
names, qualities, or descriptions, are symbolically represented."

Title: An Investigation of the Laws of Thought
Author: George Boole
CHAPTER II. SIGNS AND THEIR LAWS 22
http://www.gutenberg.org/files/15114/15114-pdf.pdf

But his side condition:

     x^2 = x

Is the same as:

    x^2 -  x = 0

[Harry Stoteles]

Actually in the polynomials, you use as add the normal add,
not xor. Its enough that the variables are from {0,1}, and all
operations, that were composed to make polynomials, were:

     Op : {0,1} x ... x {0,1} -> {0,1}

So what George Boole did was not really the Boolean Algebra
approach. Sorry for this misleading statement. The Boolean
Algebra approach, which now has his name,

is slightly different:

In Boolean Algebra where addition is XOR,
you do disjunction as follows(*):

     X v Y = X # Y # X*Y.

In George Boole Polynomials where addition is ADD,
you do disjunction as follows(*):

     X v Y = X + Y - X*Y

(*)
To be clear, I used (#)/2 for XOR as SWI-Prolog CLP(B) uses the
same sign for XOR. On the other hand the (+)/2 above is the normal
integer add, not the one from SWI-Prolog CLP(B).

[Kuniaki Mukai]

Hi,

I have a little bit generalized again my solve_boole_in_rozdd predicates,
this time for multiple unknown variables. The current solution works
as if it does in a small universe of rozdd, thtat is, “eliminating variables” is performed
staying in the universe. No need to simplifying process at induction steps on the
number of unknown variables, without going outside the universe and coming back into.

I regret that I took the comment “rozdd is a way of encoding of truth set”
in a too narrow way than the commentator might have in his mind.
Also, it maybe all folklore what I, a hobbyist, have done on rozdd programming in SWI.

Sorry for cryptic codes below in SWI. In fact, I am trying to find a way
for experience in rozdd public in a quiet way, but to fail.

?- Hell_Heaven_Problem =
(not(Y) + (not(Z) + X)*(Z + not(X))) * (Y + (not(Z) + not(X))*(Z + X)),
solve_boole_in_rozdd([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol),
Sol = [_-S],
zdd_to_prop(S, OutSol).

%@ Hell_Heaven_Problem = (not(2)+(not(3)+1)*(3+not(1)))*(2+(not(3)+not(1))*(3+1)),

%@ Y = 2,
%@ Z = 3,
%@ X = 1,

%@ Cond_for_sol = true(2),
%@ Sol = [3-25],
%@ S = 25,
%@ OutSol = 2*(1*true(0)+not(1)*false)+not(2)*(not(1)*true(0)).

%
solve_boole_in_rozdd(KnownVars,
UnknownVars,
InputProblem,
Cond_for_sol_to_exists,
Solutions) :-

init_rozdd,
append(KnownVars, UnknownVars, Vars),
zdd_solve([
newvars(Vars),

basic_prop(InputProblem, Problem),
prop(Problem, Root),
path_sum(UnknownVars, Root, Cond_for_sol_to_exists),
{ elim_vars(UnknownVars, Root, Solutions, _FreeVars) }]).

%
elim_vars([], _, [], []).
elim_vars([V|Vars], Root, [V-Sol|Sols], [U|FreeVars]):-
elim_one_var(Root, Sol, U),
elim_vars(Vars, Sol, Sols, FreeVars).

%
elim_one_var(Root, Sol, U):- zdd_solve([
getzdd(Root, if(_, L, R)),
neg(R, NegR),
newvars([U]),
prop(U, U0),
meet(U0, L, L0),
sum(L0, NegR, Sol)]).

[Harry Stoteles]

Hi Kuniaki Mukai,

I made a choice operator, which could solve your problem.
I don't know yet how to solve it in the multi-variate output
case. But the choice operator works in the uni-variate
output case.

Lets recap what quantifier like operators are known in
the literature. These can be all defined in terms of Shannon
co-factors, which I write A[X/0] and A[X/1].

Read these co-factors as setting X to 0 in the formul A,
and setting X to 1 in the formula A. So in the literature is
found the following:

     exists X A(X) :<=>  A[X/0] + A[X/1]       /* disjunction */

     forall X A(X) :<=> A[X/0] * A[X/1]          /* conjunction */

     d A(X) / dX :<=> A[X/0] # A[X/1]           /* xor */

So based on the rather longer previous post here, unfortunately
this post is even longer, which already explained my choice function,
which prefers zeros, I simply defined a new quantifier:

     choice X A(X) :<=> ~A[X/0] * A[X/1]    /* difference */

Here is your example, first use the existence quantifier
to determine the precondition when your formula is
satisifiable, it turns out always:
 

?- sat(X^((~Y+(~Z+X)*(Z+ ~X))*(Y+(~Z+ ~X)*(Z+X)))).
Yes

Now as a next step, find a formula for X, based on Y,Z.
This is as simple as applying the choice operator now,
which will give you Y=:=Z as a result:

?- current_op(X,Y,_:!).
X = 200,
Y = xfy 

?- sat(X!((~Y+(~Z+X)*(Z+ ~X))*(Y+(~Z+ ~X)*(Z+X)))).
Y = Z

Lets see whether this is really the solution. Note there can be
more solutions. The choice operator will only give one special
form of turning the multi-valued BDD tree into a single valued

BDD tree. So lets substitute back Y=:=Z for X, and lets see
what your original formula then says. I did this manually by
just rewriting the formula:

?- sat((~Y+(~Z+(Y=:=Z))*(Z+ ~(Y=:=Z)))*(Y+(~Z+ ~(Y=:=Z))*(Z+(Y=:=Z)))).
Yes

Another trick, known to Markus Triska as well, is to compute the
substitution via the use of the existential quantifier:

?- sat(X^(X=:=(Y=:=Z)*(~Y+(~Z+X)*(Z+ ~X))*(Y+(~Z+ ~X)*(Z+X)))).
Yes

I see one use case here of the new operator (!)/2, and the
choice it implemets for BDD trees. I guess we have just invented
an operator for the don't care problem. But I guess

it cannot enumerate all formulas that could be substituted
into the original formula. I also don't see that solve_boole_in_rozdd
does some backtracking and give different formulas.

So maybe the use case is quite limited. I think it solves the don't care
problem, but further research would be needed whether we really
need it for equations, such a strict choice.

Of course a sketch for multiple output variables would be also needed.
I have some scribbles how to do it with just this new choice operator
and nothing else more, but didn't try it yet...

Bye

P.S.: Here is the source code:

/* the existence quantifier tree_exists(A,X,R),
    gives the normal form R of X^A, aka exists X A */

tree_exists(zero, _, R) :- !,
   R = zero.
tree_exists(one, _, R) :- !,
   R = one.
tree_exists(node3(Y,_,A,B), X, R) :- Y < X, !,
   tree_exists(A, X, C),
   tree_exists(B, X, D),
   tree_make(C, D, Y, R).
tree_exists(node3(X,_,A,B), X, R) :- !,
   tree_or(A, B, R).
tree_exists(N, _, N).

/* the choice quantifier tree_choice(A,X,R),
    gives the normal form R of X!A, aka choice X A */

tree_choice(zero, _, R) :- !,
   R = zero.
tree_choice(one, _, R) :- !,
   R = zero.
tree_choice(node3(Y,_,A,B), X, R) :- Y < X, !,
   tree_choice(A, X, C),
   tree_choice(B, X, D),
   tree_make(C, D, Y, R).
tree_choice(node3(X,_,A,B), X, R) :- !,
   tree_not(B, C),
   tree_and(A, C, R).
tree_choice(_, _, zero).

[Harry Stoteles]

Corr.: Beware of the parenthesis:

?- sat(X^((X=:=(Y=:=Z))*(~Y+(~Z+X)*(Z+ ~X))*(Y+(~Z+ ~X)*(Z+X)))).
Yes

[Harry Stoteles]

Here is a multi-variate example using the choice operator.
I am using your example here:

      A*X + B*Y =:= 1.

I first find a formula for X based on some choice for Y dependent on X.

?- sat(X!Y!(A*X+B*Y=:=1)).
No

So the choice for X would be X=0 (probably a result of the zero
preference of my choice operator). I am substituting this and
get a formula with fewer variables:

?- sat(X^((X=:=0)*(A*X+B*Y=:=1))).
B = 1,
Y = 1

?- sat(B*Y=:=1).
B = 1,
Y = 1

Here we are already done. We have Y=1. This is a result
of unit propagation. But if there were more parameters and
if the situation would be that clear,

you get the idea, you have a new equation with fewer variables,
and you can again do your thing...

Am Dienstag, 13. Februar 2018 00:18:10 UTC+1 schrieb Harry Stoteles:

[Harry Stoteles]

What I dunno yet is whether we get a triangular
solution schema, which would allow quick solving:

      f1(X1,X2,.....,Xn) =:= 0

           f2(X2,.....,Xn) =:= 0

                     ....

                       fn(Xn) =:= 0

Where f1 would be the input. We would then
first go down from f1 to fn, and then back again.
You, Kuniaki Mukai, did not yet say what elim_vars/4
and elim_one_var/3 do. They are kind of cryptic...

I guess a simple triangular schema based on
my choice operator could work. I tried the following
for the previous multivariate example, and get easily
the correct solution B=1 again:

?- sat(X^((X=:=0)*Y!(A*X+B*Y=:=1))).
B = 1

So the triangle would be just the progressive choices,
and then substituting everything back.

[Harry Stoteles]

My choice operator is probably a refinement of this nice trick
from Tarski (Th 66, 1923), just observe that one of the co-factors
is already a solution:

For any formula A and truth assignment M, it
seems we have:

      M |= A => M |= A[X/A[X/1]]

To see that, we can A[X/A[X/1]] translates to if-then-else(A[X/1],
A[X/1],A[X/0]), which is the same as A[X/1] v A[X/0], which is
the same as exists X A. For a mention of Tarskis trick see also:

   A Note on Satisfying Truth-Value Assignments
   of Boolean Formulas - Zbigniew Stachniak -2004
   http://www.satisfiability.org/SAT04/programme/52.pdf

Now we could also look at these alternative substitution, varying
Th 66 from Tarski, the first is using the negation of the other co-factor,
and the second is my choice function that prefers zero:

    A[X/~A[X/0]]

    A[X/(~A[X/0]&A[X/1])]

Both would translate again to A[X/1] v A[X/0] (Homework) and
hence also again to exists X A. Which would be a verification that
my choice operator works as well, and not only Tarskis idea.

It gives also evidence again that there are many many choices,
for example using the other co-factor as above works also in the
substition, but there are more possibilities.

But I dont know exactly whether the choice operator could
be used for something like WalkSAT, as in the above mentioned
paper by Zbigniew Stachniak.  If the problem is represented as

a single tree, this wouldn't be needed, all the work was
already put in the tree, and problem is practically solved.
On the other hand if the problem is represented as multiple trees,

DPLL like style, in some labeling search, we could of course apply
the choice operator to all such trees, but I dunno what to do
then, maybe the choices are conflicting then.

...this is really on another,not yet written, page...

[Kuniaki Mukai]

Hi,

I have learned theory and method on solving boolean equation
in the two text books below. I have implemented just what
is in it. It is elementary, and it was a little bit surprise to see
it is almost the same method as that for robdd/rozdd builder.

It is my impression that robdd is more suitable than rozdd
for the boolean equation solver, and it might be an easy task
for the solver to be built into the clpb library. I visited the
clpb lirbrary site. The clpb is really nice as others say.

It was a luck that one of the two is still
on my book shelf, but of course there must be
many excellant books in English and other languages.

(Written in Japanese. isbn=4785620471)
日高 達: 情報論理学 (情報系教科書シリーズ)
http://iss.ndl.go.jp/books/R100000002-I000002641396-00

(Written in Japanese. isbn=4535601186)
細井 勉: 情報科学のための論理数学 (日評数学選書)
http://iss.ndl.go.jp/books/R100000002-I000002179234-00

It may be time to put a period on my rozdd builder.
I have learned many things during this experiece:
b_getval/b_setval, array (functor/3 + arg/3),
setarg/3, term_hash/4. I had overlooked the power of the commands.
Thanks Jan W. and others for the input and efforts to make them available.

Kuaniki Mukai



> Hi,
>
> Is there any solution in clpb library for a popular logic puzzle heaven-hell:
>
> http://www.crazyforcode.com/heaven-hell-puzzle-2/
>
> As far as my reach of my knowledge on clpb, I am afraid it is not easy for us.
>
> I knew a general answer in a text book by Hidaka 1997 in Japanese written as an
> example of applications of solutions of system of boolean equations, which uses
> a well-known and fundamental but a little bit lengthy normal form theorem with
> heavy use of "co-factoring."
>
> As for me, with a little hope, I am trying to find a simple solution applying my rozdd builder
> without resorting to that theorem. It is a kind of brain storming.
>
> Kuniaki Mukai
>

[Harry Stoteles]

If I translate the table of contents of the first book, its not about
solving boolean equation.

第１章　命題論理
　１　形式化ということ
　２　命題と論理式
　３　論理式と真偽
　４　論理的に同値な論理式
　５　標準形
　６　形式体系における証明
　７　トートロジーと証明可能性
　８　cut除去定理
　９　ブール代数

第２章　述語論理
　１　一階の述語論理
　２　述語論理の論理式
　３　構造
　４　恒真な論理式
　５　古典述語論理の形式体系LK
　６　完全性定理
　７　コンパクト性定理
　８　一階の述語論理の拡張

第３章　エルブランの定理と導出原理
　１　スコーレム標準形
　２　エルブランの定理
　３　導出原理──命題論理の場合
　４　導出原理──述語論理の場合

第４章　様相論理
　１　様相論理
　２　いろいろな様相論理
　３　クリプキによるセマンティクス
　４　完全性定理
　５　有限モデル性と決定可能性
　６　時間論理
　７　様相論理の周辺
　８　様相代数

第５章　直観主義論理
　１　直観主義
　２　直観主義論理の体系
　３　直観主義論理のセマンティクス
　４　完全性定理と有限モデル性
　５　埋め込み定理
　６　ハイディング代数
　７　構造規則を除いた論理

第６章　自然演繹の体系
　１　自然演繹の考え方
　２　直観主義論理に対する体系NJ
　３　古典論理に対する体系
　４　証明図の正規化
　５　ラムダ計算
　６　カリー・ハワードの対応

This gives:

Chapter
   1 Proposition
   2 propositional and logical expressions
   3 logical expressions and Boolean
   4 logically equivalent logical expressions
   5 demonstrated in standard type
   6 formal system
   7 Tautology and provability
   8 cut removed Theorem
   9 Boolean algebra that logical 1 formalism

Expansion Chapter 2 predicate logic
    1 first-order predicate logic
    2 predicate logic formulas
    3 Structure
    4 HisashiShin logical expressions
    5 classical predicate logic of formal system LK
    6 completeness theorem
    7 compactness theorem
    8 first-order predicate logic

Chapter 3 theorem and deriving principles of Herbrand
   1 Skolem cases of 4 derived principles ──
   predicate logic of Theorem
   3 derived principles ──
   propositional canonical form 2 Herbrand

Chapter 4 modal logic
    1 the modal logic
    2 different modal logic
    3 Semantics
    4 completeness theorem
    5 finite model property and Decidability
    6 hours logic
    7 modal logic near
    8 aspects algebra by Kripke

5. intuitionistic logic
    1 intuitionism
    2 intuitionistic logic scheme
    3 intuitionistic logic semantics
    4 completeness theorem and finite model property
    5 embedded Theorem
    6 hiding algebraic
    7 logic except the structure rule

Chapter 6 natural deduction scheme
    1 natural deduction concept
    2 intuitionistic corresponding normalized
    5 lambda calculus
    6 Curry Howard systematic
    4 proofs for systematic NJ 3 classical logic for logic

Thats in no way solving boolean equation. Thats on par with
a many of the other intros into logic, with some extra about NJ,
maybe half of this:

http://www.springer.com/gp/book/9783642664755

Unfortunately for solving boolean equation you need other
specialized literature. I don't know exactly which one.
You need algebraic logic, not proof theory.

Or if you would stick to proof theory, you need at
least automated theorem proving with answer extraction.
I am still refering to your original post, where you

say you want to find a formula for a variable. Answer
extraction is as follows:

3. EXTENDING THEOREM-PROVING TO QUESTIONANSWERING
2. Constructing answers
The Resolution method of proving theorems allows us to produce correct
constructive answers. This means that if, for example, ( 3x)P(x) is a theorem
then the proof procedure can find terms t1, tz, ... , tn such that P( tl) V P( tz) V
... V P(tn) is a theorem.
http://ftp.kestrel.edu/home/people/green/publications/theorem-proving.pdf

Do you think your japanese books give some solution to
your initial solving boolean equation problem? But answer
extraction which is not terms, but formulas is a little

strange. Thats quite an uncovered territory. You need very
specialized literature, not some introductory text. A FOL
answer extraction can only do it, if you would meta represent

the boolean problem. Loosing direct access to the proving
of the boolean problem. Not sure how to do it. Your problem
is very exotic and non trivial.

[Harry Stoteles]

A Prolog interpreter can be viewed as a primitive answer extractor.
After all a Prolog interpreter doesn't say simply yes or no.
A Prolog interpreter can also give answers, like for example here:

?- append([1,2],[3],X).
X=[1,2,3]

You can view this as answer extraction for horn clauses. In a
resultion refutation prover this can be easily done, by instead
posting a goal as follows:

     <- B1,..,Bn

You post a horn clause, where X1,..,Xn are the variables
you want to know:

     answer(X1,..,Xn) <- B1,..,Bn

The termination condition of the algorithm is then not anymore
an empty clause, but a single answer literal. You can then just
read off the answer substitution from the answer literal,

that was meanwhile modified, by the resulution steps.

[Harry Stoteles]

CLP(X) has its own answer interpretation I guess. The answer
is not only substitutions, but also a set of constraints that remains
at the end of the of proof development.

You might view your "solving boolean equation" as the requirment
that you want SAT constraints at the end, for those variables that
you want to solve for, in the special "solved for variables" form:

     sat(X1=:=T1), ..., sat(X1=:=Tn)

I don't think CLP(B) SWI-Prolog will give you this form by
default. Maybe there is a way to do it, I dunno. You might need
choice, maybe some weighted search helps, dunno, dunno....

[Harry Stoteles]

I suggest its forbidden to give up on this problem, at least until
the end of 2018, until at least one working multi-variable solution is
found. That works successfully on a couple of understandable problems.

[Kuniaki Mukai]

One of the books, (the one by Hosoi) includes  a theorem below. 

I use some different mathematical symbols here for writing 

in standard letters.

Theorem 2.61   For a boolean algebra equation 

a * not(x) + b * x = 1   --- (Eq)

the following 1 and 2 are equivalent.

1) Eq has a solution

2) a + b = 1.

A general solution to x of (Eq) is  

 

c * b + not(a).

In addition in the book,  an obvious algorithm is explained how to use the theorem 

for solving boolean equations.  As the theorem is fairy elementary,  I believe everyone 

on the net can access to a similar text on  logics in each language, though so far I  could not 

access any related online article. I am not good at  search on the net.

Kuniaki Mukai

[Harry Stoteles]

You model the choice by a new variable c? Do you cover
all choices non redundantly? What if a and b are dependent?
Take for example:

      a = y

      b = ~y

Obviously we have for the side condition:

      exists x (a * ~x + b * x) = a + b = y + ~y = 1

So the pair is always a solution. Then your solutions are:

      x = c * ~y + ~y

        = ~y

No choice anymore. So you need to simplify in some
way your solution formula x = c * b + ~a, to get something
useful. How do you simplify c * b + ~a, what do you show

the end user. Some minimal implicants from ROZDD
or BDD? See my other post. Or some other form. How
does Theorem 2.61 generalize to multiple variables.

[Harry Stoteles]

Corr.:
So the pair (a,b) has always a solution x.

[Kuniaki Mukai]

Hi Harry, 

That simplest theorem (in Hosoi) seems to solve boolean equations with multi

indenendent variables and unknown variables as described.

?- time(solve_boole([A,B], [X,Y], A*X+B*Y=true, Res, Sol, [slim_boole(true)])), 

   writeln(res(Res)),

   writeln(sol(Sol)).

%@ % 5,733 inferences, 0.001 CPU in 0.001 seconds (97% CPU, 7008557 Lips)

%@ res(4+not(4)*3)

%@ sol([6-(5*4*3*2*1+5*4*3*not(2)*1+5*4*not(3)+5*not(4)*3*2*1+5*not(4)*3*not(2)*1+5*not(4)*not(3)+not(5)),5-(4*3*2+4*not(3)*2+not(4))])

<snip>

I am not sure what have I being asked to reply to you, 

to whom I have been paying respects  for his seemingly outstanding remarks 

on wide issues in this forum.  Unless some neutral  bystanders here kindly clarify the current “issue”, 

I have to keep silent to your posts.  Sorry for that.  I would like to be busy for cleaning codes for making it public 

in the near future for those who might be friendly interested in. 

Kuniaki Mukai

[Harry Stoteles]

Well let me explain. You can take analogue of linear algebra.
There can be also families or single solutions or no solutions,
to an equation A x = b. Now your equation:

     A*X + B*Y = 1

to a linear algebra problem, you could write it as:

      (A,B).(X,Y) = 1

Where _._ is skalar product. And you could also
go from vector coefficients to matrice cofficients.

Now there are plenty of questions:
- What does sol([6-(5*4*3*2*1+5*4*3*n mean, I cannot decipher it,
   some new variables in it, the old variables A,B,X,Y,etc.. in it?
- What if A,B are more concrete formulas, like for example A=Z
   and B=~Z, and if we have A*X+B*~X=1 as the input equation.
- What if there are multiple equations as an input, like in linear
   algebra we solve multiple equations.
- Is there not only an analogue to equations (=), but also to
  disequations (<, >, =<, >=) in boolean algebra?

[Harry Stoteles]

What do you recommend for multiple equations:

     E1 = 1

     ....

     En = 1

Just solving the single equation:

     E1*...*En = 1

Is this your recommendation or the one from ?Hosoi?.
Whats his full name?  Some T. Hoisoi?

[Kuniaki Mukai]

> Whats his full name? Some T. Hoisoi?

T. Hosoi

[Harry Stoteles]

Tsutomu Hosoi ?

[Harry Stoteles]

Hi,

It is yet another refinement of Tarski 1923 (see my post a few
days ago).  You can see this as follows. First we can identify a
and b as co-factors of a formula e. Namely take this formula e:

       e = a * not(x) + b * x

This is the same as the BDD tree:

       e = if-then-else(x,b,a)

The co-factors are:

      e[x/0] = a

      e[x/1] = b

The existential quantifer applied to e, gives the side condition:

      exists x e = e[x/0] + e[x/1] = a + b

Now you say:
 
      x = c * b + not(a)

         = c * e[x/1] + ~e[x/0]

This is works, but it is **incomplete**. Because this
here also works, another parameter d applied
somewhere else, namely:

     x = b + d * not(a)

        = e[x/1] + d * ~e[x/0]

You can check for yourself, both work:

   ?- sat(A*(~(C*B+ ~A))+B*(C*B+ ~A)).
   sat((A->1;B->1;0))

   ?- sat(A*(~(B+D* ~A))+B*(B+D* ~A)).
   sat((A->1;B->1;0))

How do you produce the d parametrization from the
c parameterization? I stepped over this problem with
your solution Kuniaki Mukai sinceI wanted to reproduce

Tarskis solution/choice, which is:

     x = e[x/1]
 
       = b

I can produce it with d=0, how do you produce it
with your parameter c. Do you know how?

How do we get a complete solution set. Your formula
c * b + not(a) is not complete.And my formula b + d * not(a)
will also not be complete. How can they be combined?

Have a nice day!

Am Donnerstag, 15. Februar 2018 04:01:39 UTC+1 schrieb Kuniaki Mukai:

[Harry Stoteles]

Here is a more complete solution:

     x = c  * b + d * not(a) + b * not(a)

Check for yourself:

  ?-  sat(A*(~(C*B+D* ~A+B* ~A))+B*(C*B+D* ~A+B* ~A)).

  sat((A->1;B->1;0))

It has two parameters c and d. And the formula b * not(a)
You get a few special cases namely you get these
special cases:

    c=1, d=0: Tarski,1923, x = b

    c=0, d=1: The other side of Tarski: x = not(a)

    c=0, d=0: My choice operator (2018, LoL)

    c varying, d=1: What you attributed to Theorem 2.61 Hosoi

    c varying, d varying: ??Could be the full solution space??

The question is difficult, since the problem is ill-posed. How
many parameters to you allow? Why do you need respectively
allow parameters at all?

[Harry Stoteles]

Hi Kuniaki Mukai,

Have you decided on an interface for your SAT solver? How
about the usual sat/1 and labeling/1 approach.

Here is a little kitchen planner:
https://stackoverflow.com/a/49354319/502187

The kitchen has 3 places, and we assign a freezer and a stove.
The freezer is not allowed to be near to the stove. The freezer
has code 0,1 and the stove has code 1,0. We make use of the
card constraint to place the freezer and the stove.

?- L=[_,_,_,_,_,_], kitchen(L), labeling(L).
L = [0,1,0,0,1,0] ;
L = [1,0,0,0,0,1] ;
No

Am Donnerstag, 15. Februar 2018 13:41:47 UTC+1 schrieb Kuniaki Mukai:

[Kuniaki Mukai]

I have no progress to post in reply to your hello message.

However here is one conceptual thing: finally I feel now I got a better

understanding the idea of the zero-suppress, which might be already

well-known to  experts like you. That is, given a

totally ordered set V, let  E = pow(pow(V)), i.e., E is the set of subsets of

the set of subsets of V.  E forms a binary graph in the standard way,

and E thus becomes a ROZDD because of extensionality of the

membership relation on sets, which is behind the following

cryptic queries. 

?-  Hell_Heaven_Problem =

  (not(Y) + (not(Z) + X)*(Z + not(X))) * (Y + (not(Z) + not(X))*(Z + X)),

solve_boole([X, Y], [Z], Hell_Heaven_Problem, Cond_for_sol, Sol,[]),

assoc_to_logic(Sol, Conj_of_eqns),

prop_to_basic(Conj_of_eqns * Cond_for_sol -> Hell_Heaven_Problem, Veri_cond),

solc(Veri_cond, Count).

 Hell_Heaven_Problem =  (not(3)+(not(1)+2)*(1+not(2)))*(3+(not(1)+not(2))*(1+2)),

 Y = 3,

 Z = 1,

 X = 2,

 Cond_for_sol = true(1),

 Sol = [1-(1*true(1)+not(1)*(2*(3*true(3)+not(3)*false)+not(2)*(not(3)*true(3))))],

 Conj_of_eqns =  (1=1*true(1)+not(1)*(2*(3*true(3)+not(3)*false)+not(2)*(not(3)*true(3))))*true,

 Veri_cond = 1*((\1+ \true(1))*(1+(\ ... + ... * ...)*(2+(... + ...))))+(1*true(1)+ \1*(2*(... + ...)+ \ ... * (... * ...)))* \1+false+ \true(1)+(\3+(\1+2)*(1+ \2))*(3+(\1+ \2)*(1+2)),

 Count = 8 .

 ?- solve([X = (proper(0)-proper(1))+proper(1)]), sets(X, P).

 X = proper(0),

 P = [proper(0)] .

 ?- solve([X = proper(2) * proper(5) +proper(2)]), sets(X, P).

 X = proper(2),

 P = [proper(2)].

 ?- solve([X = pow([1,2]), Y=pow([1]), Z = X-Y, U = Y+Z]),

sets(U, P),

sets(X, Q),

sets(Y, R).

 X = U, U = 7,

 Y = 4,

 Z = 8,

 P = Q, Q = [[], [2], [1], [1, 2]],

 R = [[], [1]] .

 ?- solve([X = [[1],[2]]]), sets(X, P), path_count(X, C).

 X = 3,

 P = [[2], [1]],

 ?- solve([X = pow([])]), path_count(X, C).

 X = true,

 C = 1 .

 ?- solve([X = pow([1,2])]), path_count(X, C).

 X = 7,

 C = 4 .

 ?- N=10, numlist(1, N, L), solve([X = pow(L)]), path_count(X, C).

 N = 10,

 L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],

 X = 3059,

 C = 1024 .

 ?- N=20, numlist(1, N, L), solve([X = pow(L)]), path_count(X, C), C =:= (1<<N).

 N = 20,

 L = [1, 2, 3, 4, 5, 6, 7, 8, 9|...],

 X = 3145705,

 C = 1048576 .

Kuniaki Mukai

[Harry Stoteles]

As I understand, by viewing a SAT Solver as an equation solving
problem, you try to return as an answer the most intensional
result. I.e. a formula that describes the solution space.

On the other hand another SAT Solver view, can be also to
give the most extensional result, i.e. the instantiations of all
variables, those instantiations that are in the solution space.

How would your intensional answer
look like for the Kitchen Planner case?

Problem is when you for example realize a Kitchen Planner,
how can a human understand the result? If its an intensional
result, it might be more difficult grasp, than an extensional result.

The distinction of intensional and extensional can be also
made when there is no parameter involved, as it is the case
in the kitchen planner problem. So what would you return?

[Harry Stoteles]

The kitchen planner example has extensionally only two
solution, what would your system intensionally return?

Do you have a card constraint?

[Kuniaki Mukai]

As I posted in another thread, I have implemented
a boolean algebra including negation on ROZDD.

So now boolean equations could be solved over ROZDD.
I have applied the new solver to the heaven-hell puzzle among other tiny cases.

The new codes seems work well, and is here, which is simpler in many ways
compared with the old one posted here before.

%
solve_boole_verify(Uvars, Problem):-
zdd_init,
index_atomic_prop(Uvars, U0),
register_vars(U0),
zdd([sat(Problem, Root)]),
elim_vars(U0, Root, Solutions, Residue),
verify_solution(Solutions, Residue, Root).
%
verify_solution(Sol, Residue, Problem):-
assoc_to_logic(Sol, SolProp),
Vericon = (SolProp*Residue->Problem), %<<== boolean form on ROZDD.
zdd([X = Vericon]),
varnum(N),
card(X, C),
( C =:= (1<<N) ->
format("Verified: dim = ~w, count = ~w.~n",[N, C])
; format("NOT verified: dim = ~w, count = ~w.~n",[N, C])
).

Kuniaki Mukai

[j4n bur53]

You say you implemented ROZDD. This is to understand I guess
that you implemented zero suppression.

Zero suppression can be only seen when negation is available,
since we have if(X,false,A) == ~X v A. So the negative literal ~X

is needed, and will be suppressed. Can you show an example
where we see zero suppression?

[j4n bur53]

ok, kms example seems to be indeed zero suppressed:

%@ 17=if(1,truth(1),truth(4))
%@ R = 17
https://groups.google.com/d/msg/swi-prolog/D_Cf7syQPOw/f47y2LL3CQAJ

My bad!
Probaly km is too modest, or he wanted to test me. :-) :-(