Minimal Sat assignment

[Hao Zheng]

Minisat always returns a full assignment for all variables in a
formula when it is SAT. Is there any particular reason for doing that?
In many cases of model checking, a minimal assignment is highly
preferred to the full assignment. But the existing approach to finding
a reduced assignment requires some slow and awkward post-processing.
So how hard is it to modify the minisat for it to generate a reduced
assignment for a sat case.

Thanks,

Hao

[Michael Tautschnig]

You might want to try undoing decisions in reverse order - the last few of them
are possibly redundant in this respect. But other than implementing this in
minisat would simply mean implementing this "slow and awkward" process.

Best,
Michael

[Hao Zheng]

On Nov 14, 5:34 am, Michael Tautschnig

Thanks for the information. Before I spend time to actually modify
MiniSAT with you suggestion, is there any reason (implementation- or
algorithm-wise) that a fully assignment has to be returned in the
first place?

Thanks,
- Hao

[Daniel Le Berre]

Le 15/11/2011 15:53, Hao Zheng a �crit :

The SAT solver knows that is has found a satisfiable assignment when
there is no more variable to assign. Because the solvers use lazy data
structure, they do not know at some point if all the clauses are
satisfied or not.

Daniel

[Hao Zheng]

Thank you very much for the insights. It helps a lot.

Hao