Opened 2 years ago

Closed 2 years ago

#26329 closed enhancement (fixed)

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

Reported by: tmonteil Owned by:
Priority: major Milestone: sage-8.4
Component: linear programming Keywords:
Cc: Merged in:
Authors: Thierry Monteil Reviewers: Travis Scrimshaw
Report Upstream: N/A Work issues:
Branch: 4b3cc1b (Commits, GitHub, GitLab) Commit: 4b3cc1bfc511516bbcb5872742975ac8a7b417fd
Dependencies: Stopgaps:

Status badges

Description

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.

Change History (8)

comment:1 Changed 2 years ago by tmonteil

  • Branch set to u/tmonteil/allow_xor_clause_in_dimacs_files__format_extended_by_cryptominisat_

comment:2 Changed 2 years ago by tmonteil

  • Commit set to 6712e18de5180fce56258a225684ce36272e6783
  • Status changed from new to needs_review

New commits:

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

comment:3 Changed 2 years ago by tscrim

  • Reviewers set to Travis Scrimshaw

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.

comment:4 Changed 2 years ago by git

  • Commit changed from 6712e18de5180fce56258a225684ce36272e6783 to 4b3cc1bfc511516bbcb5872742975ac8a7b417fd

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

​4b3cc1b#26329 : reviewer's comments

comment:5 Changed 2 years ago by tmonteil

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.

comment:6 Changed 2 years ago by tscrim

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

comment:7 Changed 2 years ago by tscrim

  • Status changed from needs_review to positive_review

comment:8 Changed 2 years ago by vbraun

  • Branch changed from u/tmonteil/allow_xor_clause_in_dimacs_files__format_extended_by_cryptominisat_ to 4b3cc1bfc511516bbcb5872742975ac8a7b417fd
  • Resolution set to fixed
  • Status changed from positive_review to closed
Note: See TracTickets for help on using tickets.