[Question] enumerateAllModels() method - Is there an Option for order of output?

[axkr]

In the enumerateAllModels() methods, is there an option for the preferred "solution output order"?
I.e. if I would like to get the results with the most "True" values for the variables first or the results with the most "False" values for the variables?
Something like an "ascending" or "descending" sort order?

[d-bischoff]

Currently there is no option for a solution output order. (See https://github.com/logic-ng/LogicNG/blob/master/src/main/java/org/logicng/solvers/MiniSat.java for example)

The models are ordered the way the solver finds them, which is seemingly random, due to heuristics used. Changing this directly in the solver will greatly impact performance I believe.
You could however order them afterwards.

Why don't you go through the list of assignments you get and order them in the fashion you like?

[axkr]

How do heuristics work? Do they start with False values trying or with True values?

[czengler]

This behaviour of the solver can be configured for MiniSat in https://github.com/logic-ng/LogicNG/blob/master/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java with the configuration parameter initialPhase.

[axkr]

Java doc of the Setter method for initialPhase says that the default value should be true, but it seems to be false?

[d-bischoff]

Doesn't the "nextVariableToAssign" heuristic also play into that?

A positive choice could lead to a lot of negative assignments due to unit propagation.
Assigning true to a different literal could on the other hand imply a lot of unit propagations that are positive,

So this does not necessarily order the models in that way.
Am I correct here?

[axkr]

I sort the resulting list of assignments in reverse order now.

Thanks for your suggestions.