Returning not only the first model of an cnf

[asibkamalsada]

Dear arminbiere,

thank you for the great CDCL solver!
Is it possible to make cadical return all models to a given cnf? Perhaps via command line option?
My specific use case is that I am trying to reduce the problem of finding extensions of an argumentation framework to SAT, in which case not only the first found model is of relevance.

Best regards.

[arminbiere]

There are some pending changes to the stand-alone solver for the next release and this will be revisited then (through the API this is easy to achieve).

[ajohnson1]

I like CadiCal and would find this feature useful as sometimes I want to find all (or a limited number) of solutions and choose the 'best' afterwards as what is 'best' is hard to directly describe in CNF. I can simulate this by adding the previous solutions as being disallowed in the CNF, but that wastes what the solver has learned from the first ones.

It is also a good test for solver performance as being 'lucky' finding the first solution doesn't help so much, so might be a more robust measure of the effect of making changes to the solver.