Mutually exclusive clp(BNR) constraints

Hi,

I’m trying to compute constraints on a list of boolean pairs.

Essentially, I want this, but yielding clp(BNR) constraints instead of enumerating solutions:

core_([],0,0).
core_([K-V|T],Tp,Fp):-
    [K,V]::boolean,
    {(K and V),Tp==Tpn+1},
    core_(T,Tpn,Fp).
core_([K-V|T],Tp,Fp):-
    [K,V]::boolean,
    {(K > V),Fp==Fpn+1},
    core_(T,Tp,Fpn).
core(P,Tp,Fp):-
    length(P,L),
    [Tp,Fp]::integer(0,L),
    core_(P,Tp,Fp).
?- P=[1-1,1-_],core(P,Tp,Fp),{Ppv==Tp/(Tp+Fp)}.
P = [1-1, 1-1],
Tp = 2,
Fp = 0,
Ppv = 1 ;
P = [1-1, 1-0],
Tp = Fp, Fp = 1,
Ppv = 1r2 ;
false.

I tried rewriting as below:

core([],0,0).
core([K-V|T],Tp,Fp):-
    [K,V]::boolean,
    {
               Btp==(K,V),Tp==Tp1+Btp,
               Bfp==(K > V),Fp==Fp1+Bfp
    },
    core(T,Tp1,Fp1).

The conditions on K and V are mutually exclusive, so I would expect: Ppv::real(1r2, 1)

… but in fact, this happens: Ppv::real(0.3333333333333333, 2)

?- P=[1-1,1-_],core(P,Tp,Fp),{Ppv==Tp/(Tp+Fp)}.
P = [1-1, 1-_A],
Tp::real(1, 2),
Fp::real(0, 1),
_A::boolean,
Ppv::real(0.3333333333333333, 2).

While giving Ppv as input yields expected results in cases :

?- P=[1-1,1-_],core(P,Tp,Fp),Ppv=1r3,{Ppv==Tp/(Tp+Fp)}.
false.

?- P=[1-1,1-_],core(P,Tp,Fp),Ppv=1r2,{Ppv==Tp/(Tp+Fp)}.
P = [1-1, 1-0],
Tp = Fp, Fp = 1,
Ppv = 1r2.

?- P=[1-1,1-_],core(P,Tp,Fp),Ppv=2,{Ppv==Tp/(Tp+Fp)}.
false.

.. but misses that _A should be 1 in :

?- P=[1-1,1-_],core(P,Tp,Fp),Ppv=1,{Ppv==Tp/(Tp+Fp)}.
P = [1-1, 1-_A],
Ppv = 1,
Tp::real(1, 2),
Fp::real(0, 1),
_A::boolean.

Why are Ppv bounds 1r3->2 instead of 1r2->1 ?

Thanks !

Hello,
Again, @ridgeworks will be the best answer this question, but since I am in an earlier timezone than him, I can answer your question first ^^

Here is another formulation of what a true positive and what a false positive are:

tp(K-V, R) :-
   {R == (K and V)}.
fp(K-V, R) :-
   [K, V]::boolean,
   {R == (K > V)}.

% utility function for summing a list of variables
sum(L, Sum) :-
   foldl([B, A, B+A]>>true, L, 0, Expr),
   {Sum == Expr}.

You can now express your example like this:

?- P=[1-1,1-_], maplist(tp, P, Tps), sum(Tps, Tp),
   maplist(fp, P, Fps), append(Tps, Fps, TpsFps), sum(TpsFps, TpFp),
   {Ppv == Tp / TpFp}.
P = [1-1, 1-_A],
Tps = [1, _B],
Fps = [0, _C],
TpsFps = [1, _B, 0, _C],
_B::boolean,
_A::boolean,
Tp::real(1, 2),
_C::boolean,
TpFp::real(1, 3),
Ppv::real(0.3333333333333333, 2).

Although this does not solve your problem, I changed the formulation for Ppv a little by first summing true positives and false positives into a variable TpFp.
If you look at the interval for TpFp, you can see that it goes from [1, 3], which is too large.
You can ask clpBNR to try and reduce TpFp interval by using the solve predicate:

?- P=[1-1,1-_], maplist(tp, P, Tps), sum(Tps, Tp),
   maplist(fp, P, Fps), append(Tps, Fps, TpsFps), sum(TpsFps, TpFp),
   {Ppv == Tp / TpFp}, TpFp::integer, solve(TpFp).
P = [1-1, 1-_A],
Tps = [1, _B],
Fps = [0, _C],
TpsFps = [1, _B, 0, _C],
TpFp = 2,
_B::boolean,
_A::boolean,
Tp::real(1, 2),
_C::boolean,
Ppv::real(0.5, 1) ;
false.

But usually, when computing metrics like this, you actually know the number of predictions beforehand, that TpFp = 2, so basically:

?- N = 2, P=[1-1,1-A], maplist(tp, P, Tps), sum(Tps, Tp),
{Ppv == Tp / N}.
N = 2,
P = [1-1, 1-A],
Tps = [1, _A],
_A::boolean,
A::boolean,
Tp::real(1, 2),
Ppv::real(0.5, 1).

I’ll let @ridgeworks answer the difficult question why clpBNR does not take into account the mutually exclusive constraints when summing boolean variables.

Just skimming over this - I think you’re showing that clpBNR is not narrowing perfectly. This is already known, e.g. Impossible comparison succeeds · Issue #16 · ridgeworks/clpBNR · GitHub

Use the likes of solve/1 to actually get a solution, i.e. all the constraints properly satisfied. Anything else is speculative and includes only reasonable-efforts at narrowing the potential solutions, so could be actually false.

1 Like

Indeed, he tightest bounds are (1r2,1), as in:

?- P=[1-1,1-B],core(P,Tp,Fp),{Ppv==Tp/(Tp+Fp)}, enumerate(B).

B = 0,
Fp = Tp, Tp = 1,
P = [1-1, 1-0],
Ppv = 1r2 ;
B = Ppv, Ppv = 1,
Fp = 0,
P = [1-1, 1-1],
Tp = 2

The reason optimal narrowing isn’t achieved without enumerate/1 (or solve/1, as noted by @brebs), is the so-called dependancy issue fundamental to interval arithmetic. If there is more than one reference to the same variable in an expresssion, optimal narrowing may not occur. In the case of {Ppv==Tp/(Tp+Fp)}, Tp is mentioned twice. If you substitute the lower bound of Tp in the numerator and the higher bound in the denominator, you’ll see where the value 1r3 comes from. Therefore, you have to force the narrowing via some kind of search (labelling in clpfd terminology).

In this case a simple fix is to note that Tp+Fp is the length of the list P, so eliminating the reference in the denominator:

?- P=[1-1,1-B],length(P,N),core(P,Tp,Fp),{Ppv==Tp/N}.

N = 2,
P = [1-1, 1-B],
B::boolean,
Ppv::real(0.5,1),
Fp::real(0,1),
Tp::real(1,2)

While this may be true, this isn’t explicitly specified in a constraint, and the clpBNR constraint system, for various reasons, doesn’t perform any higher level analysis which could infer this across multiple constraints.

I think you could also simplify your constraint in core/3:

    {
               Tp==Tp1+(K and V),
               Fp==Fp1+(K > V)
    }

Thank you for your answer. I understand better now.

Just for future use, how would I specify explicitely that constraints are mutually exclusive ? I’ve attempted to do that with xor, but with limited success.

Not sure what you’ve tried, or what your objectives is, but xor would be my first guess, e.g., {(K and V) xor (K > V)}. While this constraint must always be true, nothing much can be done until one of the booleans is known. Use enumerate/1 to find all the cases when the constraint is true:

?- [K,V]::boolean, {(K and V) xor (K > V)}, enumerate([K,V]).
K = 1,
V = 0 ;
K = V, V = 1.

Note that K can never be 0, but that isn’t directly inferred by the constraint system. It doesn’t “reason” about the constraint, it just enforces that any variable values are consistent with the constraints.

A proper “oracle” could further reduce this to {(V == 1) xor (V==0)} which really doesn’t say anything (V is already a boolean), so this small example is a bit non-sensical; the real value is in how boolean constraints can be used to drive the propagation of other numeric constraints.