I am using cryptominisat 5.0. I have a file of DIMACS standard format having a mix of cnf clauses and xor clauses( an “x” in front of the line to make that line an XOR clause). I saved it with filename DIMAC.cnf. I gave this file as input to cryptominisat as follows: solver.read("/home/hridya/SageMath/DIMAC.cnf") I got the following error. ValueError: invalid literal for int() with base 10: 'x1'. What is the problem?
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).
EDIT this is now trac ticket 26329
Once this ticket will be merged, with the file you provided, you will be able to do:
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)The SageMath documentation page about CryptoMiniSat explains how to save to a file.
It would be nice if it also gave an example of how to read back such a file.
Especially, an example which has xor clauses.
Asked: 6 years ago
Seen: 1,124 times
Last updated: Sep 21 '18
Copyright Sage, 2010. Some rights reserved under creative commons license. Content on this site is licensed under a Creative Commons Attribution Share Alike 3.0 license.
Could you please provide the whole cnf file ?
That was a sample file: I will copy the contents here:
c filename DIMAC.cnf
p cnf 10 7
x1 2 8 9 0
3 -8 0
4 -8 0
5 -9 0
6 -9 0
9 -10 0
7 -10 0
Note: also asked as Stack Overflow question 52221410: Usage of CryptoMiniSat.
Note: also asked as Issue #527 on the CryptoMiniSat issue tracker.