crillab / d4

d4 Model Counter
GNU Lesser General Public License v3.0
14 stars 4 forks source link

Question on showing the values of projection variables #11

Open maliabd-al-majid opened 5 months ago

maliabd-al-majid commented 5 months ago

Hi

I want to ask whether it is possible to output the truth assignments corresponding to a model in the case of projected model counting. For instance, suppose the following CNF representation of AND Gate:

p cnf 3 3
-1 -2 3 0
1 -3 0
2 -3 0

Then, I wanted to compute the models w.r.t. 2 and 3: 2,3 Now the number of models w.r.t. these variables is correct but i want to write these values to a file. it should be something like:

1 0.
0 0.
1 1.

Is there a way to write these values from the solver?

Thanks in advance.