Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
sagetrac-tmonteil mannequin opened this issue Sep 21, 2018 · 10 comments
Closed

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

sagetrac-tmonteil mannequin opened this issue Sep 21, 2018 · 10 comments

Comments

@sagetrac-tmonteil
Copy link
Mannequin

sagetrac-tmonteil mannequin commented Sep 21, 2018

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

@sagetrac-tmonteil sagetrac-tmonteil mannequin added this to the sage-8.4 milestone Sep 21, 2018
@sagetrac-tmonteil
Copy link
Mannequin Author

sagetrac-tmonteil mannequin commented Sep 21, 2018

@sagetrac-tmonteil
Copy link
Mannequin Author

sagetrac-tmonteil mannequin commented Sep 21, 2018

Commit: 6712e18

@sagetrac-tmonteil
Copy link
Mannequin Author

sagetrac-tmonteil mannequin commented Sep 21, 2018

New commits:

6712e18#26329 : SatSolver.read can parse xor clauses

@tscrim
Copy link
Collaborator

tscrim commented Sep 21, 2018

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
Copy link
Collaborator

tscrim commented Sep 21, 2018

Reviewer: Travis Scrimshaw

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Sep 22, 2018

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

4b3cc1b#26329 : reviewer's comments

@sagetrac-git
Copy link
Mannequin

sagetrac-git mannequin commented Sep 22, 2018

Changed commit from 6712e18 to 4b3cc1b

@sagetrac-tmonteil
Copy link
Mannequin Author

sagetrac-tmonteil mannequin commented Sep 22, 2018

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
Copy link
Collaborator

tscrim commented Sep 22, 2018

comment:6

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

@vbraun
Copy link
Member

vbraun commented Sep 23, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants