What is the "meaning" of leaf answers with residual goals? Is THIS answer "valid"?

[jjtolton]

After reading this comment from @triska and comparing to a GRAPHPLAN algorithm I'm working on:

?- plan([at(a,1),at(b,2),at(c,3),clear(4),clear(5),clear(6)], [at(a,3), at(b,1), at(c,2)], Plan).
%@    Plan = [[go(a,1,4)],[go(b,2,1),go(a,4,5)],[go(c,3,2),go(a,5,6)],[go(a,6,3)]], clpz:(_A in 0..1), clpz:(_A#>=_B), clpz:(_A#>=_C), clpz:(_B in 0..1), clpz:(_B#>=_D), clpz:(_E#>=_B), clpz:(_B#>=_F), clpz:(_D in 0..1), clpz:(_G#>=_D), clpz:(_G in 0..1), clpz:(_H#>=_G), clpz:(_H in 0..1), clpz:(_E in 0..1), clpz:(_F in 0..1), clpz:(_I#>=_F), clpz:(_I in 0..1), clpz:(_J#>=_I), clpz:(_J in 0..1), clpz:(_C in 0..1), clpz:(_C#>=_K), clpz:(_L#>=_C), clpz:(_C#>=_M), clpz:(_K in 0..1), clpz:(_N#>=_K), clpz:(_N in 0..1), clpz:(_O#>=_N), clpz:(_O in 0..1), clpz:(_L in 0..1), clpz:(_M in 0..1), clpz:(_P#>=_M), clpz:(_P in 0..1), clpz:(_Q#>=_P), clpz:(_Q in 0..1), clpz:(_R in 0..1), clpz:(_R#>=_S), clpz:(_R#>=_T), clpz:(_S in 0..1), clpz:(_U#>=_S), clpz:(_U in 0..1), clpz:(_T in 0..1), clpz:(_V#>=_T), clpz:(_V in 0..1), clpz:(_W in 0..1), clpz:(_W#>=_X), clpz:(_W#>=_Y), clpz:(_X in 0..1), clpz:(_Z#>=_X), clpz:(_Z in 0..1), clpz:(_Y in 0..1), clpz:(_A1#>=_Y), clpz:(_A1 in 0..1), clpz:(_B1 in 0..1), clpz:(_B1#>=_C1), clpz:(_B1#>=_D1), clpz:(_C1 in 0..1), clpz:(_E1#>=_C1), clpz:(_E1 in 0..1), clpz:(_D1 in 0..1), clpz:(_F1#>=_D1), clpz:(_F1 in 0..1), clpz:(_G1 in 0..1), clpz:(_G1#>=_H1), clpz:(_G1#>=_I1), clpz:(_H1 in 0..1), clpz:(_J1#>=_H1), clpz:(_J1 in 0..1), clpz:(_I1 in 0..1), clpz:(_K1#>=_I1), clpz:(_K1 in 0..1), clpz:(_L1 in 0..1), clpz:(_M1 in 0..1), clpz:(_N1 in 0..1), clpz:(_O1 in 0..1)
%@ ;  Plan = [[go(a,1,4)],[go(b,2,1),go(a,4,5)],[go(c,3,2),go(a,5,6)],[go(a,6,3)]], clpz:(_A in 0..1), clpz:(_A#>=_B), clpz:(_A#>=_C), clpz:(_B in 0..1), clpz:(_B#>=_D), clpz:(_E#>=_B), clpz:(_B#>=_F), clpz:(_D in 0..1), clpz:(_G#>=_D), clpz:(_G in 0..1), clpz:(_H#>=_G), clpz:(_H in 0..1), clpz:(_E in 0..1), clpz:(_F in 0..1), clpz:(_I#>=_F), clpz:(_I in 0..1), clpz:(_J#>=_I), clpz:(_J in 0..1), clpz:(_C in 0..1), clpz:(_C#>=_K), clpz:(_L#>=_C), clpz:(_C#>=_M), clpz:(_K in 0..1), clpz:(_N#>=_K), clpz:(_N in 0..1), clpz:(_O#>=_N), clpz:(_O in 0..1), clpz:(_L in 0..1), clpz:(_M in 0..1), clpz:(_P#>=_M), clpz:(_P in 0..1), clpz:(_Q#>=_P), clpz:(_Q in 0..1), clpz:(_R in 0..1), clpz:(_R#>=_S), clpz:(_R#>=_T), clpz:(_S in 0..1), clpz:(_U#>=_S), clpz:(_U in 0..1), clpz:(_T in 0..1), clpz:(_V#>=_T), clpz:(_V in 0..1), clpz:(_W in 0..1), clpz:(_W#>=_X), clpz:(_W#>=_Y), clpz:(_X in 0..1), clpz:(_Z#>=_X), clpz:(_Z in 0..1), clpz:(_Y in 0..1), clpz:(_A1#>=_Y), clpz:(_A1 in 0..1), clpz:(_B1 in 0..1), clpz:(_B1#>=_C1), clpz:(_B1#>=_D1), clpz:(_C1 in 0..1), clpz:(_E1#>=_C1), clpz:(_E1 in 0..1), clpz:(_D1 in 0..1), clpz:(_F1#>=_D1), clpz:(_F1 in 0..1), clpz:(_G1 in 0..1), clpz:(_G1#>=_H1), clpz:(_G1#>=_I1), clpz:(_H1 in 0..1), clpz:(_J1#>=_H1), clpz:(_J1 in 0..1), clpz:(_I1 in 0..1), clpz:(_K1#>=_I1), clpz:(_K1 in 0..1), clpz:(_L1 in 0..1), clpz:(_M1 in 0..1), clpz:(_N1 in 0..1), clpz:(_O1 in 0..1)
%@ ;  Plan = [[go(a,1,4)],[go(b,2,1),go(a,4,5)],[go(c,3,2),go(a,5,6)],[go(a,6,3)]], clpz:(_A in 0..1), clpz:(_A#>=_B), clpz:(_A#>=_C), clpz:(_B in 0..1), clpz:(_B#>=_D), clpz:(_E#>=_B), clpz:(_B#>=_F), clpz:(_D in 0..1), clpz:(_G#>=_D), clpz:(_G in 0..1), clpz:(_H#>=_G), clpz:(_H in 0..1), clpz:(_E in 0..1), clpz:(_F in 0..1), clpz:(_I#>=_F), clpz:(_I in 0..1), clpz:(_J#>=_I), clpz:(_J in 0..1), clpz:(_C in 0..1), clpz:(_C#>=_K), clpz:(_L#>=_C), clpz:(_C#>=_M), clpz:(_K in 0..1), clpz:(_N#>=_K), clpz:(_N in 0..1), clpz:(_O#>=_N), clpz:(_O in 0..1), clpz:(_L in 0..1), clpz:(_M in 0..1), clpz:(_P#>=_M), clpz:(_P in 0..1), clpz:(_Q#>=_P), clpz:(_Q in 0..1), clpz:(_R in 0..1), clpz:(_R#>=_S), clpz:(_R#>=_T), clpz:(_S in 0..1), clpz:(_U#>=_S), clpz:(_U in 0..1), clpz:(_T in 0..1), clpz:(_V#>=_T), clpz:(_V in 0..1), clpz:(_W in 0..1), clpz:(_W#>=_X), clpz:(_W#>=_Y), clpz:(_X in 0..1), clpz:(_Z#>=_X), clpz:(_Z in 0..1), clpz:(_Y in 0..1), clpz:(_A1#>=_Y), clpz:(_A1 in 0..1), clpz:(_B1 in 0..1), clpz:(_B1#>=_C1), clpz:(_B1#>=_D1), clpz:(_C1 in 0..1), clpz:(_E1#>=_C1), clpz:(_E1 in 0..1), clpz:(_D1 in 0..1), clpz:(_F1#>=_D1), clpz:(_F1 in 0..1), clpz:(_G1 in 0..1), clpz:(_G1#>=_H1), clpz:(_G1#>=_I1), clpz:(_H1 in 0..1), clpz:(_J1#>=_H1), clpz:(_J1 in 0..1), clpz:(_I1 in 0..1), clpz:(_K1#>=_I1), clpz:(_K1 in 0..1), clpz:(_L1 in 0..1), clpz:(_M1 in 0..1), clpz:(_N1 in 0..1), clpz:(_O1 in 0..1)
%@ ;  ... .

I am wondering, are these leaf answers "valid" or are they only valid if the residual goals can be satisfied? In the context of a planning algorithm, it feels like it might be better to force a concrete answer. But not entirely sure how to interpret this.

[triska]

As long as there are pending constraints, it is generally unclear whether an answer describes any solutions, especially for theories that are not decidable, such as integer arithmetic.

In the example above, we can find out whether there are solutions by searching for integers that satisfy all constraints. For instance, taking the residual goals of the first leaf answer, we find solutions even if all integers are between 0 and 1:

?-  Gs = [clpz:(_A in 0..1), clpz:(_A#>=_B), clpz:(_A#>=_C), clpz:(_B in 0..1), clpz:(_B#>=_D), clpz:(_E#>=_B), clpz:(_B#>=_F), clpz:(_D in 0..1), clpz:(_G#>=_D), clpz:(_G in 0..1), clpz:(_H#>=_G), clpz:(_H in 0..1), clpz:(_E in 0..1), clpz:(_F in 0..1), clpz:(_I#>=_F), clpz:(_I in 0..1), clpz:(_J#>=_I), clpz:(_J in 0..1), clpz:(_C in 0..1), clpz:(_C#>=_K), clpz:(_L#>=_C), clpz:(_C#>=_M), clpz:(_K in 0..1), clpz:(_N#>=_K), clpz:(_N in 0..1), clpz:(_O#>=_N), clpz:(_O in 0..1), clpz:(_L in 0..1), clpz:(_M in 0..1), clpz:(_P#>=_M), clpz:(_P in 0..1), clpz:(_Q#>=_P), clpz:(_Q in 0..1), clpz:(_R in 0..1), clpz:(_R#>=_S), clpz:(_R#>=_T), clpz:(_S in 0..1), clpz:(_U#>=_S), clpz:(_U in 0..1), clpz:(_T in 0..1), clpz:(_V#>=_T), clpz:(_V in 0..1), clpz:(_W in 0..1), clpz:(_W#>=_X), clpz:(_W#>=_Y), clpz:(_X in 0..1), clpz:(_Z#>=_X), clpz:(_Z in 0..1), clpz:(_Y in 0..1), clpz:(_A1#>=_Y), clpz:(_A1 in 0..1), clpz:(_B1 in 0..1), clpz:(_B1#>=_C1), clpz:(_B1#>=_D1), clpz:(_C1 in 0..1), clpz:(_E1#>=_C1), clpz:(_E1 in 0..1), clpz:(_D1 in 0..1), clpz:(_F1#>=_D1), clpz:(_F1 in 0..1), clpz:(_G1 in 0..1), clpz:(_G1#>=_H1), clpz:(_G1#>=_I1), clpz:(_H1 in 0..1), clpz:(_J1#>=_H1), clpz:(_J1 in 0..1), clpz:(_I1 in 0..1), clpz:(_K1#>=_I1), clpz:(_K1 in 0..1), clpz:(_L1 in 0..1), clpz:(_M1 in 0..1), clpz:(_N1 in 0..1), clpz:(_O1 in 0..1)],
    term_variables(Gs, Vs),
    Vs ins 0..1,
    label(Vs).
   Gs = (clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0#>=0),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0 in 0..1),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(...in...),... :(...),...,...), _A = 0, _B = 0, _C = 0, _D = 0, _E = 0, _F = 0, _G = 0, _H = 0, _I = 0, _J = 0, _K = 0, _L = 0, _M = 0, _N = 0, _O = 0, _P = 0, _Q = 0, _R = 0, _S = 0, _T = 0, _U = 0, _V = 0, _W = 0, _X = 0, _Y = 0, _Z = 0, _A1 = 0, _B1 = 0, _C1 = 0, _D1 = 0, _E1 = 0, _F1 = 0, _G1 = 0, _H1 = 0, _I1 = 0, _J1 = 0, _K1 = 0, _L1 = 0, _M1 = 0, _N1 = 0, _O1 = 0, Vs = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0|...]
;  Gs = (clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0#>=0),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0 in 0..1),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(...in...),... :(...),...,...), _A = 0, _B = 0, _C = 0, _D = 0, _E = 0, _F = 0, _G = 0, _H = 0, _I = 0, _J = 0, _K = 0, _L = 0, _M = 0, _N = 0, _O = 0, _P = 0, _Q = 0, _R = 0, _S = 0, _T = 0, _U = 0, _V = 0, _W = 0, _X = 0, _Y = 0, _Z = 0, _A1 = 0, _B1 = 0, _C1 = 0, _D1 = 0, _E1 = 0, _F1 = 0, _G1 = 0, _H1 = 0, _I1 = 0, _J1 = 0, _K1 = 0, _L1 = 0, _M1 = 0, _N1 = 0, _O1 = 1, Vs = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0|...]
;  Gs = (clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0#>=0),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0 in 0..1),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(...in...),... :(...),...,...), _A = 0, _B = 0, _C = 0, _D = 0, _E = 0, _F = 0, _G = 0, _H = 0, _I = 0, _J = 0, _K = 0, _L = 0, _M = 0, _N = 0, _O = 0, _P = 0, _Q = 0, _R = 0, _S = 0, _T = 0, _U = 0, _V = 0, _W = 0, _X = 0, _Y = 0, _Z = 0, _A1 = 0, _B1 = 0, _C1 = 0, _D1 = 0, _E1 = 0, _F1 = 0, _G1 = 0, _H1 = 0, _I1 = 0, _J1 = 0, _K1 = 0, _L1 = 0, _M1 = 0, _N1 = 1, _O1 = 0, Vs = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0|...]
;  Gs = (clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0#>=0),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0 in 0..1),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(0 in 0..1),clpz:(0#>=0),clpz:(...in...),... :(...),...,...), _A = 0, _B = 0, _C = 0, _D = 0, _E = 0, _F = 0, _G = 0, _H = 0, _I = 0, _J = 0, _K = 0, _L = 0, _M = 0, _N = 0, _O = 0, _P = 0, _Q = 0, _R = 0, _S = 0, _T = 0, _U = 0, _V = 0, _W = 0, _X = 0, _Y = 0, _Z = 0, _A1 = 0, _B1 = 0, _C1 = 0, _D1 = 0, _E1 = 0, _F1 = 0, _G1 = 0, _H1 = 0, _I1 = 0, _J1 = 0, _K1 = 0, _L1 = 0, _M1 = 0, _N1 = 1, _O1 = 1, Vs = [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0|...]
;  ... .

Now we are certain that all constraints can be satisfied, and hence a solution exists.

We can be certain that there are solutions if the answer is in solved form, i.e., consisting exclusively of constraints of the form Var_i = T_i, as in the case above.

[jjtolton]

Interesting! Isn't there some way using copy_term or one of those builtins that you can capture the residual constraints and apply labeling programmatically?

[triska]

When we formulate a constraint satisfaction problem, we usually know the variables that need to be subjected to search; by convention, we use the last argument of the core relation to describe the list of variables that need to be labeled!

[jjtolton]

Got it. I will continue the rewrite!