Opened 4 months ago

Last modified 3 months ago

#26552 new enhancement

interface glucose-syrup

Reported by: slabbe Owned by:
Priority: major Milestone: sage-8.5
Component: packages: optional Keywords: thursdaysbdx
Cc: Merged in:
Authors: Sébastien Labbé Reviewers:
Report Upstream: N/A Work issues:
Branch: u/slabbe/26552 (Commits) Commit: 4408ea56b837288a801380210192c2b274bb8b86
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 (10)

comment:1 Changed 4 months ago by tmonteil

I guess this is a duplicate of #26361.

comment:2 follow-up: Changed 4 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 4 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 4 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 4 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 4 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 4 months ago by slabbe

  • Description modified (diff)

comment:8 Changed 4 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 4 months ago by slabbe

updated commit message (26361->26552)

comment:10 Changed 3 months ago by slabbe

  • Keywords thursdaysbdx added
Note: See TracTickets for help on using tickets.