Probabilistic sat solver in cplint

Help! Pack
1 

/*

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.

2

What I could need in cplint is to write the predicates not directly but via assertz or something else.

Assertz and similar predicates are not supported by the semantics.
Moreover, predicates inside :- begin_lpad. and :- end_lpad. are modified through term expansion, so, even if you assert them during the execution, they will likely not work.

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.

Yes, variables in the head for decision clauses are currently not supported. I will try to implement it in the future.

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?

No, currently dt_solve/2 returns only 1 solution, even if there are multiple solutions with the same cost. Also this could be a possible extension I can implement.

And why does it take so much time?

Don’t know, I need to check it.

Let me know if you have further questions.

1 Like
3

I guess dt_solve probes some values and does a minimum search, because it takes some time. From my perspective I could imagine a list of different results with different probabilities would also be interesting. But it has also to take the utility settings into consideration. This makes it more complicated.

And there is another issue. Inside of one lpad block I can have lots of probability predicates but only one strategy computation.

How would it be to extend the ‘dt_solve’ mechanism for managing more than one strategy?

An example:


?(tag1) :: a.

utlity( tag1, a, 1).

...

solve(tag1, A, B).

or more sophisticated:


?(tag1) :: a.
?([tag1,tag2]) :: b.
?(tag2) :: c.

utlity( tag1, a, 1).
utlity( [tag1,tag2], b, 1).
utlity( tag2, c, 1).

...

solve(tag1, A, B).
solve(tag2, A, B).

Thanks in advance.