search

pysathq / pysat

A toolkit for SAT-based prototyping in Python
https://pysathq.github.io/
MIT License
389 stars 71 forks source link

Minimal satisfiability solver #82

Closed migueltorrescosta closed 3 years ago

migueltorrescosta commented 3 years ago

Are any of the solvers optimized for minimal solutions, in the sense of minimizing the amount of literals set to true? I was considering something similar to this modification of pycosat: https://github.com/ContinuumIO/pycosat/pull/39

haz commented 3 years ago

Couldn't you just run maxsat with -1 weights on positive literals?

alexeyignatiev commented 3 years ago

@migueltorrescosta, a possible solution would be indeed the one suggested by @haz. Alternatively, a couple of solvers we have in PySAT should always respect the polarities you set using set_phases(). See the documentation on how this can be done.

migueltorrescosta commented 3 years ago

Yes, that is ideal. Thank you for the prompt reply!