 # Using QSAT to perform Abduction

Just a little note. There is an interesting relationship from
s(CAPS) to QSAT. If we split the propositonal variables V into
two camps, `V1` the abducible ones, and `V2` the normal ones,
we can do deduction and abduction in one go.

``````/* SWI-Prolog */
?- use_module(library(clpb)).

?- sat(V1 ~(V2^ ~(P =< Q))).
``````

But there are even more tricks in stock with a QSAT
solver, especially from within Prolog. Works also for
Jekejeke Prolog not only SWI-Prolog. Namely listing models.
We can list models when we ommit V1, here

the s(CAPS) `r` and `not r` example:

``````/* Two Models */
?- ﻿sat(~(R^ ~((P+Q)*(R>=P*Q)=<R))), labeling([P,Q]).
P = 0, Q = 0;
P = 1, Q = 1.
/* One Model */
?- ﻿sat(~(R^ ~((P+Q)*(R>=P*Q)=< ~R))), labeling([P,Q]).
P = 0, Q = 0.
``````

The later makes us think about completion. What if
a Prolog `r <- p & q` effectively means `r <-> p & q`. This is
called closed world assumption. We can also tinker with
closed world assumption by replacing (>=)/2 by (=:=)/2:

``````/* Two Models */
?- ﻿sat(~(R^ ~((P+Q)*(R=:=P*Q)=<R))), labeling([P,Q]).
P = 0, Q = 0;
P = 1, Q = 1.
/* Three Models */
?- ﻿sat(~(R^ ~((P+Q)*(R=:=P*Q)=< ~R))), labeling([P,Q]).
P = 0, Q = 0;
P = 0, Q = 1;
P = 1, Q = 0.
``````

In the above we listed all models, not only those where `p v q`
holds, but the QSAT query could be arranged to filter accordingly.

Cool!

1 Like