Using SAT solver module from Symbolic Logic module

[equaeghe]

It seems (but I am not entirely sure) that currently the Symbolic Logic module does not (optionally) use the SAT solver module for the is_satisfiable() method. As this can make this method more efficient, it can be a useful addition. (And allow returning a satisfying instance of the variables.)

(N.B.: Both modules seem to have a method outputting DIMACS format.)

Links:

• related ticket (concerns efficient CNF encoding): ​http://trac.sagemath.org/ticket/15676
• symbolic logic docs: http://www.sagemath.org/doc/reference/logic/sage/logic/boolformula.html
• SAT solver docs: http://www.sagemath.org/doc/reference/sat