```
/*
sat problem:
p cnf 3 3
-1 2 0
-1 3 0
1 -2 -3 0
solution:
(ins)$ picosat --all 003.cnf
s SATISFIABLE
v -1 2 -3 0
s SATISFIABLE
v -1 -2 3 0
s SATISFIABLE
v -1 -2 -3 0
s SATISFIABLE
v 1 2 3 0
s SOLUTIONS 4
*/
:- use_module(library(yall)).
:- use_module(library(clpq)).
:- use_module(library(clpfd)).
:- use_module(library(pita)).
:- pita.
:- begin_lpad.
rule1(L) : P :- L = [P1,_,_] , {P1 = ( 1 - P) }.
rule1(L) : P :- L = [_,P,_].
rule2(L) : P :- L = [P1,_,_] , {P1 = ( 1 - P) }.
rule2(L) : P :- L = [_,_,P].
rule3(L) : P :- L = [P,_,_].
rule3(L) : P :- L = [_,P2,_], {P2 = ( 1 - P) }.
rule3(L) : P :- L = [_,_,P3], {P3 = ( 1 - P) }.
cnf(L) :- rule1(L), rule2(L), rule3(L).
? :: vars([0,0,0]).
? :: vars([1,0,0]).
? :: vars([0,1,0]).
? :: vars([1,1,0]).
? :: vars([0,0,1]).
? :: vars([1,0,1]).
? :: vars([0,1,1]).
? :: vars([1,1,1]).
cnf :- vars(L), cnf(L).
utility( cnf, 1).
:- end_lpad.
print_all_solutions :- true
, GOAL1 = {L}/(length( L, 3) , L ins 0..1 , label(L))
, forall( GOAL1, ( GOAL2=prob(cnf(L), _), GOAL2, writeln(GOAL2)))
.
/*
(ins)?- dt_solve(A,B).
A = [[vars([0, 0, 0])]],
B = 1.0.
(ins)?- print_all_solutions.
prob(cnf([0,0,0]),1.0)
prob(cnf([0,0,1]),1.0)
prob(cnf([0,1,0]),1.0)
prob(cnf([0,1,1]),0.0)
prob(cnf([1,0,0]),0.0)
prob(cnf([1,0,1]),0.0)
prob(cnf([1,1,0]),0.0)
prob(cnf([1,1,1]),1.0)
true.
*/
```

What I could need in cplint is to write the predicates not directly but via assertz or something else. I would also appreciate when I were able to write the ‘? :: vars([0,0,0]).’ statements with variables like ‘? :: vars([V1,V2,V2]) :- … .’ . cplint does not support that currently.

In this exercise the ‘dt_solve(A,B)’ needed some time. But it finds a solution. Is there a possibility to find other solutions via dt_solve? And why does it take so much time?

Thanks in advance.