Ask Your Question
3

Usage of cryptominisat

asked 2018-09-06 12:14:04 -0500

Hridya gravatar image

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?

edit retag flag offensive close merge delete

Comments

Could you please provide the whole cnf file ?

tmonteil gravatar imagetmonteil ( 2018-09-06 14:30:51 -0500 )edit

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

Hridya gravatar imageHridya ( 2018-09-07 00:16:39 -0500 )edit
slelievre gravatar imageslelievre ( 2018-09-08 08:35:21 -0500 )edit
slelievre gravatar imageslelievre ( 2018-09-09 17:31:59 -0500 )edit

1 answer

Sort by » oldest newest most voted
1

answered 2018-09-07 16:00:59 -0500

tmonteil gravatar image

updated 2018-09-07 16:02:11 -0500

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 flag offensive delete link more

Comments

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.

slelievre gravatar imageslelievre ( 2018-09-12 05:27:55 -0500 )edit

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

Stats

Asked: 2018-09-06 12:14:04 -0500

Seen: 78 times

Last updated: Sep 07