1 | initial version |

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.

2 | No.2 Revision |

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).

3 | No.3 Revision |

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)
```

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.