sagemath / sage

Main repository of SageMath
https://www.sagemath.org
Other
1.38k stars 469 forks source link

Allow xor clause in DIMACS files (format extended by cryptominisat) #26329

Closed edd8e884-f507-429a-b577-5d554626c0fe closed 6 years ago

edd8e884-f507-429a-b577-5d554626c0fe commented 6 years ago

Cryptominisat accepts xor clauses but is currently not able to read DIMACS files with such clauses, see this ask question.

Since some other solvers might accept xor clauses, the parsing of such clauses is done on the generic solver.

Component: linear programming

Author: Thierry Monteil

Branch/Commit: 4b3cc1b

Reviewer: Travis Scrimshaw

Issue created by migration from https://trac.sagemath.org/ticket/26329

edd8e884-f507-429a-b577-5d554626c0fe commented 6 years ago

Branch: u/tmonteil/allow_xor_clause_in_dimacs_files__format_extended_bycryptominisat

edd8e884-f507-429a-b577-5d554626c0fe commented 6 years ago

Commit: 6712e18

edd8e884-f507-429a-b577-5d554626c0fe commented 6 years ago

New commits:

6712e18#26329 : SatSolver.read can parse xor clauses
tscrim commented 6 years ago
comment:3

Could you add a test showing the error is correctly raised? Should the file also be closed when the error message is raised?

Also a little nitpick, but error messages (following Python conventions) do not start with a capital letter.

tscrim commented 6 years ago

Reviewer: Travis Scrimshaw

7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 6 years ago

Branch pushed to git repo; I updated commit sha1. New commits:

4b3cc1b#26329 : reviewer's comments
7ed8c4ca-6d56-4ae9-953a-41e42b4ed313 commented 6 years ago

Changed commit from 6712e18 to 4b3cc1b

edd8e884-f507-429a-b577-5d554626c0fe commented 6 years ago
comment:5

Done.

Note that i used SatLP to test the error message, but in #26330 i plan to let SatLP accept xor clauses, so hopefully #26334 and #26335 will be accepted before so that i can use PicoSAT (which does not accept xor clauses) instead.

tscrim commented 6 years ago
comment:6

Thanks. I will review #26334 and #26335 now.

vbraun commented 6 years ago

Changed branch from u/tmonteil/allow_xor_clause_in_dimacs_files__format_extended_bycryptominisat to 4b3cc1b