Revision history [back]

This is due to the fact that the read method for the cryptominisat solver is inherited from the generic sat solver, see the last line of:

sage: s = SAT()
sage: s
CryptoMiniSat solver: 0 variables, 0 clauses.
sage: s.read??

Since the x is specific to cryptominisat and not part of the CNF specification, the parser can not handle it. It should be very easy to write a read method inside the CryptoMiniSat class that handles this, or just add a try-except statement in the SatSolver class depending on whether there exists a add_xor_clause method available.

This is due to the fact that the read method for the cryptominisat solver is inherited from the generic sat solver, see the last line of:

sage: s = SAT()
sage: s
CryptoMiniSat solver: 0 variables, 0 clauses.
sage: s.read??

Since the x is specific to cryptominisat and not part of the CNF specification, the parser can not handle it. It should be very easy to write a read method inside the CryptoMiniSat class that handles this, or just add a try-except statement in the SatSolver class depending on whether there exists a add_xor_clause method available.available (typically, one could imagine to add add_xor_clause method to the LP solver).

This is due to the fact that the read method for the cryptominisat solver is inherited from the generic sat solver, see the last line of:

sage: s = SAT()
sage: s
CryptoMiniSat solver: 0 variables, 0 clauses.
sage: s.read??

Since the x is specific to cryptominisat and not part of the CNF specification, the parser can not handle it. It should be very easy to write a read method inside the CryptoMiniSat class that handles this, or just add a try-except statement in the SatSolver class depending on whether there exists a add_xor_clause method available (typically, one could imagine to add add_xor_clause method to the LP solver).

sage: s = SAT()
sage: s.read('/tmp/your_file.dimacs')
sage: s
CryptoMiniSat solver: 10 variables, 7 clauses.
sage: s.clauses()
[((1, 2, 8, 9), True, True),
 ((3, -8), False, None),
 ((4, -8), False, None),
 ((5, -9), False, None),
 ((6, -9), False, None),
 ((9, -10), False, None),
 ((7, -10), False, None)]
sage: s()
(None, True, False, False, False, False, False, False, False, False, False)