SAT and MixedIntegerLinearProgram

[videlec]

We could have a much more friendly user interface to SAT solvers by following what has been done for MixedIntegerLinearProgram. We propose that for a given SAT solver created via solver = SAT() we

• allow any Python object as a variable, ie

sage: solver = SAT()
sage: x = solver.new_variable()
sage: solver.add_clause([x['hello'], -x[(1,2)], x[3]])

For compatibility with standard solvers, nonzero integers are also allowed, the variable x just provides an automatic translation from Python objects to integer.

• use solver.solve() instead of solver() (the result being either True or False)
• (unsure whether it is desirable) use solver.get_values(x) to get the values of the variables when the problem is SAT

CC: @sagetrac-tmonteil @mkoeppe

Component: combinatorics

Issue created by migration from https://trac.sagemath.org/ticket/24172

[videlec]

Description changed:

--- 
+++ 
@@ -7,5 +7,6 @@
 sage: x = solver.new_variable()
 sage: solver.add_clause([x['hello'], -x[(1,2)], x[3]])

• For compatibility with standard solvers, nonzero integers are also allowed, the variable x just provides an automatic translation from Python objects to integer.
  • use solver.solve() instead of solver() (the result being either True or False)
  • (unsure whether it is desirable) use solver.get_values(x) to get the values of the variables when the problem is SAT

[edd8e884-f507-429a-b577-5d554626c0fe]

comment:2

Someooooone suggested to support the pythonic syntax !x[(1,2)] for the negation of a variable ;)