\myheading{CSPLIB problem 018}

\url{https://github.com/csplib/csplib/blob/master/Problems/prob018/specification.md}:

\begin{lstlisting}
You are given an 8 pint bucket of water, and two empty buckets which can contain 5 and 3 pints respectively.
You are required to divide the water into two by pouring water between buckets (that is, to end up with
4 pints in the 8 pint bucket, and 4 pints in the 5 pint bucket).

What is the minimum number of transfers of water between buckets? The challenge is to solve this as 
a planning problem (encoded into satisfiability or constraint satisfaction) with an efficiency approaching 
(or exceeding) a simple enumeration.
\end{lstlisting}

I've reworked the Prolog code ( \url{https://github.com/csplib/csplib/blob/master/Problems/prob018/models/enumerate.pl} ) into this...

For another solution, see also: \url{https://github.com/YosysHQ/SymbiYosys/blob/master/docs/examples/puzzles/pour_853_to_4.sv}.

\begin{lstlisting}[style=custompy]
from z3 import *

def _try (POURINGS):
    print "* try %d" % POURINGS
    STATES=POURINGS+1

    A=[Int('A_%d' % i) for i in range(STATES)]
    B=[Int('B_%d' % i) for i in range(STATES)]
    C=[Int('C_%d' % i) for i in range(STATES)]
    op=[Int('op_%d' % i) for i in range(STATES)]

    def Z3_min(a,b):
        return If(a<b, a, b)

    s=Solver()

    # volumes (not states):
    jug_A, jug_B, jug_C = 8,5,3

    # "columns": If(And(op==..., preconditions), And(what next state will have), ...)
    for cur in range(STATES-1):
        next=cur+1
        s.add(If(And(op[cur]==0, A[cur]>0, B[cur]<jug_B), And(B[next]==Z3_min(jug_B, B[cur]+A[cur]), A[next]==A[cur]-(B[next]-B[cur]), C[next]==C[cur]),
            If(And(op[cur]==1, A[cur]>0, C[cur]<jug_C), And(C[next]==Z3_min(jug_C, C[cur]+A[cur]), A[next]==A[cur]-(C[next]-C[cur]), B[next]==B[cur]),
            If(And(op[cur]==2, B[cur]>0), And(A[next]==A[cur]+B[cur], C[next]==C[cur], B[next]==0),
            If(And(op[cur]==3, B[cur]>0, C[cur]<jug_C), And(A[next]==A[cur], C[next]==Z3_min(jug_C, C[cur]+B[cur]), B[next]==B[cur]-(C[next]-C[cur])),
            If(And(op[cur]==4, C[cur]>0), And(A[next]==A[cur]+C[cur], B[next]==B[cur], C[next]==0),
            If(And(op[cur]==5, C[cur]>0), And(A[next]==A[cur], B[next]==Z3_min(jug_B, B[cur]+C[cur]), C[next]==C[cur]-(B[next]-B[cur])),
            False)))))))

    # no state must repeat:
    for i in range(STATES):
        for j in range(i):
            s.add(Or(A[i]!=A[j], B[i]!=B[j], C[i]!=C[j]))

    # initial and final state:
    s.add(And(A[0]==8, B[0]==0, C[0]==0))
    s.add(And(A[STATES-1]==4, B[STATES-1]==4, C[STATES-1]==0))

    if s.check()==unsat:
        return

    m=s.model()

    ops_names=["A->B", "A->C", "B->A", "B->C", "C->A", "C->B"]
    for i in range(STATES):
        print "state %d, %d-%d-%d" % (i, m[A[i]].as_long(), m[B[i]].as_long(), m[C[i]].as_long())
        if i!=STATES-1:
            print "op_%d = %s" % (i, ops_names[m[op[i]].as_long()])
    exit(0)

#_try(7)
#exit(0)

for i in range(20):
    _try(i)
\end{lstlisting}

\begin{lstlisting}
state 0, 8-0-0
op_0 = A->B
state 1, 3-5-0
op_1 = B->C
state 2, 3-2-3
op_2 = C->A
state 3, 6-2-0
op_3 = B->C
state 4, 6-0-2
op_4 = A->B
state 5, 1-5-2
op_5 = B->C
state 6, 1-4-3
op_6 = C->A
state 7, 4-4-0
\end{lstlisting}