Opened 8 months ago

Closed 3 weeks ago

#26552 closed enhancement (fixed)

interface glucose-syrup

Reported by: slabbe Owned by:
Priority: major Milestone: sage-8.8
Component: packages: optional Keywords: thursdaysbdx
Cc: Merged in:
Authors: Thierry Monteil Reviewers: Sébastien Labbé
Report Upstream: N/A Work issues:
Branch: cca5a2f (Commits) Commit: cca5a2f02aa95ebdb6a7344b648977d271cc1742
Dependencies: Stopgaps:

Description (last modified by slabbe)

As a follow-up of #26361 this ticket adds an interface to glucose-syrup (the parallel version of glucose):

Example:

sage: solver = SAT('glucose-syrup')
sage: solver.add_clause( (1,2,-3) )
sage: solver()
(None, True, False, False)

Change History (18)

comment:1 Changed 8 months ago by tmonteil

I guess this is a duplicate of #26361.

comment:2 follow-up: Changed 8 months ago by slabbe

Merde, je l'avais pas vu passer. If you agree I will move my changes to your ticket on top of your commits.

comment:3 in reply to: ↑ 2 ; follow-up: Changed 8 months ago by tmonteil

Replying to slabbe:

Merde, je l'avais pas vu passer. If you agree I will move my changes to your ticket on top of your commits.

Honestly, i wanted to touch the rest of the code minimally (of course the existing interface has to be fixed), because i first want to write a better interface, so that we can call tons of solvers without having to write a dedicated class for each (i would like to have a kind of database of available solvers in a json file, and you can solve the same problem with various solvers without having to rewrite the clauses as it is the case currently, i mean the problem will be defined independently of the solver when possible). In particular, i did not add a class for glucose-syrup to avoid useless back-work.

By the way, note that your code will not work for problems with lots of variables, since in such cases glucose-syrup will split the solution into many lines, hence the glucose parser has to be adapted. If you really want that feature for the short term, i can add my parser for it (it is written already, so there is no work on my side).

Please tell me what are your global plans about so that we can synchronize our whishes (for example, i plan to add an __iter__ method to loop over every solutions, etc).

comment:4 Changed 8 months ago by slabbe

  • Branch u/slabbe/glucose deleted
  • Commit 3477fd38ec69f24d6df7e521a297b0d4275aad8a deleted
  • Description modified (diff)
  • Summary changed from glucose SAT solver as optional package to interface glucose-syrup

Updating the goal of this ticket because its original goal was already done in #26361

comment:5 Changed 8 months ago by slabbe

  • Authors set to Sébastien Labbé
  • Branch set to u/slabbe/26552
  • Commit set to 45645d1a7415511508df07f3ab2d88d2df5f6bcd

Readding the interface to glucose-syrup (not working) because it writes an empty file to the output. I asked the question to Laurent Simon and I am waiting for an answer.


New commits:

0035b14#26361: package glucose SAT solver
1159e03#26361 : glucose depends on zlib
38d09eb#26361 : fix glucose interface + doctests
878769d#26361 : add a warning about the license of glucose-syrup
19ac7ecMerge branch 'u/tmonteil/glucose_sat_solver' into 8.5.beta0
521f59526361 adding doctests, adding glucose as an option to `SAT`
41fa42626361: adding optional tags
45645d126361: adding an interface to glucose-syrup

comment:6 in reply to: ↑ 3 Changed 8 months ago by slabbe

Replying to tmonteil:

Please tell me what are your global plans about so that we can synchronize our whishes (for example, i plan to add an __iter__ method to loop over every solutions, etc).

All my code is online now either here or on #26361. I also want a global interface to exist. This is why I added the possibility to SAT('glucose') in #26361 (if you agree, and if this does not interfere with your global plan). Also, this is why I am adding the possibility to SAT('glucose-syrup') here in this ticket.

Is the commit 45645d1 a problem for the goal your are aiming?

comment:7 Changed 8 months ago by slabbe

  • Description modified (diff)

comment:8 Changed 8 months ago by git

  • Commit changed from 45645d1a7415511508df07f3ab2d88d2df5f6bcd to 4408ea56b837288a801380210192c2b274bb8b86

Branch pushed to git repo; I updated commit sha1. This was a forced push. New commits:

4408ea526552: adding an interface to glucose-syrup

comment:9 Changed 8 months ago by slabbe

updated commit message (26361->26552)

comment:10 Changed 8 months ago by slabbe

  • Keywords thursdaysbdx added

comment:11 Changed 4 weeks ago by tmonteil

  • Branch changed from u/slabbe/26552 to u/tmonteil/26552

comment:12 Changed 4 weeks ago by tmonteil

  • Authors changed from Sébastien Labbé to Sébastien Labbé, Thierry Monteil
  • Commit changed from 4408ea56b837288a801380210192c2b274bb8b86 to dc5742a5b14c151cc72c0c4226f419974563c718
  • Status changed from new to needs_review

New commits:

dc5742a#26552 interface glucose-syrup

comment:13 follow-up: Changed 4 weeks ago by chapoton

please fix the python3-incompatible code, see patchbot plugin reports

comment:14 Changed 4 weeks ago by git

  • Commit changed from dc5742a5b14c151cc72c0c4226f419974563c718 to cca5a2f02aa95ebdb6a7344b648977d271cc1742

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

8a39a25Merge branch 'u/tmonteil/26552' of trac.sagemath.org:sage into HEAD
cca5a2f#26552 : code simplification.

comment:15 in reply to: ↑ 13 Changed 4 weeks ago by tmonteil

Replying to chapoton:

please fix the python3-incompatible code, see patchbot plugin reports

Done. Actually, there was no real reason to catch (and hide) an error that should not appear.

comment:16 Changed 4 weeks ago by slabbe

  • Authors changed from Sébastien Labbé, Thierry Monteil to Thierry Monteil
  • Reviewers set to Sébastien Labbé
  • Status changed from needs_review to positive_review

comment:17 Changed 4 weeks ago by chapoton

  • Milestone changed from sage-8.5 to sage-8.8

comment:18 Changed 3 weeks ago by vbraun

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