ASKSAGE: Sage Q&A Forum - Individual question feedhttps://ask.sagemath.org/questions/Q&A Forum for SageenCopyright Sage, 2010. Some rights reserved under creative commons license.Wed, 12 Sep 2018 05:27:55 -0500Usage of cryptominisathttps://ask.sagemath.org/question/43603/usage-of-cryptominisat/ 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?Thu, 06 Sep 2018 12:14:04 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/Comment by slelievre for <p>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?</p>
https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43628#post-id-43628Note: also asked as [Issue #527 on the CryptoMiniSat issue tracker](https://github.com/msoos/cryptominisat/issues/527).Sun, 09 Sep 2018 17:31:59 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43628#post-id-43628Comment by slelievre for <p>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?</p>
https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43620#post-id-43620Note: also asked as [Stack Overflow question 52221410: Usage of CryptoMiniSat](https://stackoverflow.com/q/52221410).Sat, 08 Sep 2018 08:35:21 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43620#post-id-43620Comment by Hridya for <p>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?</p>
https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43609#post-id-43609That 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 0Fri, 07 Sep 2018 00:16:39 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43609#post-id-43609Comment by tmonteil for <p>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?</p>
https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43604#post-id-43604Could you please provide the whole cnf file ?Thu, 06 Sep 2018 14:30:51 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43604#post-id-43604Answer by tmonteil for <p>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?</p>
https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?answer=43615#post-id-43615This 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](https://trac.sagemath.org/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)Fri, 07 Sep 2018 16:00:59 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?answer=43615#post-id-43615Comment by slelievre for <p>This is due to the fact that the <code>read</code> method for the cryptominisat solver is inherited from the generic sat solver, see the last line of:</p>
<pre><code>sage: s = SAT()
sage: s
CryptoMiniSat solver: 0 variables, 0 clauses.
sage: s.read??
</code></pre>
<p>Since the <code>x</code> 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 <code>read</code> method inside the <code>CryptoMiniSat</code> class that handles this, or just add a try-except statement in the <code>SatSolver</code> class depending on whether there exists a <code>add_xor_clause</code> method available (typically, one could imagine to add <code>add_xor_clause</code> method to the LP solver).</p>
<p><strong>EDIT</strong> this is now <a href="https://trac.sagemath.org/ticket/26329">trac ticket 26329</a></p>
<p>Once this ticket will be merged, with the file you provided, you will be able to do:</p>
<pre><code>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)
</code></pre>
https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43649#post-id-43649The [SageMath documentation page about CryptoMiniSat](https://doc.sagemath.org/html/en/reference/sat/sage/sat/solvers/cryptominisat.html)
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.Wed, 12 Sep 2018 05:27:55 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43649#post-id-43649Answer by slelievre for <p>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?</p>
https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?answer=43611#post-id-43611It would seem XOR clauses are not accepted in all versions of CryptoMiniSat.
On the dedicated page
- [XOR clauses](https://www.msoos.org/xor-clauses/)
one can read the following warning:
> *Note: XOR clauses are only supported in CryptoMiniSat 2*
Since you are using CryptoMiniSat 5.0, getting an error is maybe not unexpected.Fri, 07 Sep 2018 09:18:43 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?answer=43611#post-id-43611Comment by tmonteil for <p>It would seem XOR clauses are not accepted in all versions of CryptoMiniSat.</p>
<p>On the dedicated page</p>
<ul>
<li><a href="https://www.msoos.org/xor-clauses/">XOR clauses</a></li>
</ul>
<p>one can read the following warning:</p>
<blockquote>
<p><em>Note: XOR clauses are only supported in CryptoMiniSat 2</em></p>
</blockquote>
<p>Since you are using CryptoMiniSat 5.0, getting an error is maybe not unexpected.</p>
https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43614#post-id-43614This is not true, cryptominisat 5 accepts xor clause and there is an `add_xor_clause` mehod in the cryptominisat class, see https://git.sagemath.org/sage.git/tree/src/sage/sat/solvers/cryptominisat.py#n147 and https://www.msoos.org/cryptominisat5/ It is possible that the warning was done in comparison between version 1 and 2.Fri, 07 Sep 2018 15:53:43 -0500https://ask.sagemath.org/question/43603/usage-of-cryptominisat/?comment=43614#post-id-43614