Minimum true variables

[mkber...@gmail.com]

In my experiments with minisat(core), I observed that it assigns TRUE to a minimum number of boolean variables.

Is it the case that the tool OR the algorithm has been designed in such a way, or did I get these just by chance?

[Michael Tautschnig]

Hello,

The default polarity, which applies upon the first time a decision is taken, is
coded to be FALSE. If you look for "polarity" in the code base, you can rather
easily change that. There is also an option for randomising polarity (rnd_pol),
but this isn't exposed at the command-line interface at present.

Best,
Michael

[Allen Van Gelder]

> In my experiments with minisat(core), I observed that it assigns TRUE to a
> minimum number of boolean variables.

Be aware that this does not preclude the possibility of a different
satisfying assignment for the formula
that has fewer true variables than the assignment that minisat found.
--Allen