Add Negative Phase Search Option

[migueltorrescosta]

This MR adds a minimal keyword argument, which optimizes PicoSat for finding minimal solutions

Motivation

In many practical applications the literals are control flags. Due to the risk of unforeseen consequences in the presence of unnecessary changes, it is beneficial to minimize them.

Changes

• Adds a minimal keyword argument which defaults to False
• When minimal=False the code runs exactly as before.
• When minimal=True:
  • The default Phase is Negative instead of using the Jeruslow-Wang heuristic
  • When a solution is found, instead of adding the inverse of the current solution, it adds the inverse of an And join of the literals set with their Phase to true. This means that all solutions which are strictly larger than this one, in the superset sense, will not be returned, keeping to the idea of returning minimal solutions only.

Usage example

import pycosat
g = pycosat.itersolve([[2*i,2*i+1] for i in range(1,1000)], minimal=True)
next(g)

This imediately returns a solution with only 500 positive values, which is the least number needed for it to be true. The current implementation returns all variables set to True (i.e. all positive)

[github-actions]

Hi there, thank you for your contribution!

This pull request has been automatically marked as stale because it has not had recent activity. It will be closed automatically if no further activity occurs.

If you would like this pull request to remain open please:

1. Rebase and verify the changes still work
2. Leave a comment with the current status

NOTE: If this pull request was closed prematurely, please leave a comment.

Thanks!