Finding all solutions by minisat

[Do]

Dear all,
I am trying to find all solutions by modifying minisat2.2.2 code.

In main function of minisat2.2.2/minisat/simp/main.cc I add a while
loop to find all solutions, in that I add a clause with the negation
of the literals (cl) found in the model (S.model). However it does not
return all solutions. In output file, only first solution is repeated
many time.

Any one can help me ? Thank you in advances

This is my code:

while (bret){
cl.clear(true);
S.model.clear(true);
cl.growTo(S.nVars());
bret = S.solve();

if (bret){
for (int i = 0; i < S.nVars(); i++)
if (S.model[i] != l_Undef){
fprintf(res, "%s%s%d", (i==0)?"":" ",
(S.model[i]==l_True)?"":"-", i+1);
cl[i] = ((S.model[i]==l_True) ?~mkLit(i):
mkLit(i)); //negation of literal
}//of if (S.model[i] != l_Undef)

fprintf(res, " 0\n");
S.addClause(cl);
}

}//while (bret ==true)

Bests,
Do Ngoc

[Niklas Een]

Try removing 'cl.growTo(...);' and replace 'c[i]' with 'c.push(...)'.
Right now, you may have undefined elements in 'cl' if some variable is
undefined in the model (not sure if that can happen; maybe Niklas S can
answer).

// Niklas

[Do]

Dear Niklas E
Thank you for your quick reply.
I already tried c.push(...), but the result did not change.

[Niklas Sörensson]

Hello,

I think the problem is that you are using the SimpSolver class that
does preprocessing and may eliminate variables. Variables that are
eliminated are not allowed to be mentioned in any future clause that
is added.

To check if this is the case, run with the "-no-pre" flag that turns
off preprocessing. To solve the problem in your application you can
turn off preprocessing like that, use the non-preprocessing solver
class, or freeze the variables that you want to enumerate solutions
over (this forbids the solver to eliminate particular variables; use
'setFrozen()' for that).

I hope this helps,

/Niklas

[Do]

Dear Niklas S,
You are right. I add " -no-elim" flag (it seems there is no "-no-pre"
flag in minisat2.2.2) and I can find all solutions now.
I will try 'setFrozen()' later.

Thank you very much!
Best regards,
Do Ngoc