Fastest, safest way to test that a goal has a unique solution?

General
1

I’m wondering about the fastest and safest way to implement something like

one(G)

(not once), that calls G, but only succeeds if G has exactly one solution.

At some point, I had done it with:

one(X) :- findall(X, X, [X]).

but recently found this (and similar) were incompatible with, and caused problems with attributed variables (SWI Prolog reported it as a problem).

This implementation ran without warnings, but produced strange results until I replaced copy_term with copy_term_nat. (Note that I’m only using attributed-variables for some debugging/tracing purposes at the moment so they aren’t strictly necessary).

one(X) :-
    copy_term(X, X0),
    X -> \+ ( X0, X0 \= X).

So currently I have:

one(X) :-
    copy_term_nat(X, X0),
    X -> \+ ( X0, X0 \= X).

If variables of a solution constrain each other, in a way not easily (or not yet) modelled with clp, I can still eagerly commit to some goals in certain cases.

Given that this seems useful and general but I haven’t seen it, and also that I’ve had some unexpected behaviours (with attributed variables), I wanted to double check that this implementation of one/1 looked reasonably correct, safe and fast.

2

Is this the same as “the goal succeeds deterministically”? If so, take a look here.

(well, the behavior depends on a flag and that flag currently does not have a “fail” option so that’s different for sure)

3

No. I’m not making any claims about the goal ahead of time. I’m just saying this goal might have more than one solution at this moment, but only succeed in the case that it has exactly one solution.

The det and $ stuff is more about debugging a program, where it’s a bug if a goal/predicate isn’t deterministic.

4

One thing about this is that you must find a second solution to know to fail. I wonder if a simplified implementation with limit/2 from library(solution_sequences) as a starting point would be a way to do it? Because the findall approach will find all solutions before failing?

1 Like
5

As I mentioned,

The idea is make a copy of the goal. Attempt the goal, immediately commit to the first solution, then fail if we can solve at least one other way.

I don’t suspect wrapping X with distinct(X) would matter. We commit to the first solution for X. And whatever equality work distinct(X0) could do, we’re doing instead at \=.

6

Yes, right, I missed that because there was no “call” :smiley: sorry. I admit I don’t quite understand the need for call/1 in all cases.

Either way, I still suspect that copying the goal is not the fastest way to go about it.

7

Hopefully helps:

one_soln(Goal, Soln) :-
    setof(Soln, Goal, [Soln]).

Examples:

?- one_soln(member(X, [1]), X).
X = 1.

?- one_soln(member(X, [1, 2]), X).
false.

Supporting attributed variables is impossible, is my knee-jerk reaction :grinning:

8

I don’t know if it’s the fastest, but you can use setup_call_cleanup/3 to test for deterministic results – the documentation is somewhat unclear but the examples on the webpage should help you do what you want.

1 Like
9

Does not work :frowning:

?- freeze(X, X = 2), one(between(1,3,X)).
false.

If you want this to work cleanly with all constraints it gets hard. But, you start with findall/3, which means you want to ensure there are not two derivations, while this one/1 is defined to allow for multiple derivations as long as they all produce the same answer. This too is not easily defined, is this under ==/2, =/2 or =@=/2? Note that =/2 is very likely wrong, as a goal resulting in f(1) and f(_) would succeed.

Apart from all this, the fastest way is probably to start checking for determinism after the first solution. If there, you are done. I’d imaging something like

one(X) :-
    call_nth(X, N),
    (   <det>
    ->  true
    ;   <here it gets hard>
    )

The <here it gets hard> depends on the desired semantics wrt multiple solutions as well as whether or not copying is allowed and what may be copied (the query or the answer, both or none).

For determinism testing there is deterministic/1 (used by the toplevel) or the portable call_cleanup(Goal, Det=true)

1 Like
11

Thank for these clarifications and ideas.

I realize now that I have more narrowly defined requirement than a general purpose one/1.
(==/2, and allowing multiple derivations)

12

An interesting improvement over findall/3 in the wild:

has_unique_answer(G) :- findnsols(2,G,G,Sols),!,Sols=[G].

https://arxiv.org/pdf/1709.04302

But SWI-Prolog does copy the goal G before it runs
findnsols/4. Is this necessary? I don’t find that the goal
G is copied in the ordinary findall/3. Only the template?

I think the above example gives a rational why copy is necessary.
Without copy the G might show a solution, depending on
implementation of findnsols maybe the 2nd or 3rd solution,

this might prevent binding G with the 1st solution.

BTW: Such abominations are not really necessary if the Prolog
system has a library(sequence). One can combine limit/2
with findall/3. There is also no goal copy issue:

has_unique_answer(G) :- findall(G,limit(2,G),Sols),!,Sols=[G].
13

Checked with git blame. The copy_term/2 is in the initial implementation. Thinking about it, it is probably there to avoid leaving Templ and Goal instantiated to the last result of the chunk. For findall/3 this is not required as it backtracks to the end, and thus no bindings remain. And no, you can’t just copy Templ as you need its variable sharing with Goal.

If you accept copying, I think the best way is to call call_nth/2, check that the result is deterministic (done), else copy the result and backtrack to see whether it produces a second. If so, there is an error, else copy the first result back. If you accept call_cleanup/2 as portable, this is a portable solution :slight_smile: