Hi,
i am currently packaging and interfacing a bunch of SAT solvers,
especially the ones that run in parallel.
Gulcose ships glucose-syrup which is parallel [1], and was ranked first in
the 2017 parallel track of the SAT competition.
However, while Glucose, which is based on MiniSat, is licensed under a MIT
license (which allows sublicensing), glucose-syrup is now MIT with the
additional condition:
- The parallel version of Glucose (all files modified since Glucose 3.0
releases, 2013) cannot be used in any competitive event (sat
competitions/evaluations) without the express permission of the
authors (Gilles Audemard / Laurent Simon). This is also the case for
any competitive event using Glucose Parallel as an embedded SAT engine
(single core or not).
I am not a lawyer, but i bet this is not GPL-compatible (is it ?). One
could argue that participating to SAT competitions is not part of Sage
mission statement.
Worse: painless [2], which won the 2018 parallel track, is released under
a GPL-3+ license, but it contains glucose-syrup (among other solvers).
Maybe they got permission to use glucose-syrup ?
My question is: what should i do ?
I could:
- package both glucose and glucose-syrup as if everything is OK
- add a warning with a Y/N question when installing glucose-syrup
- install only glucose (but then none of us benefit from the parallel
code)
- package painless, and pick glucose-syrup from there
- discuss with the developpers and try to convince them to release
glucose-syrup under a true MIT license.
Ciao,
Thierry
[1] http://www.labri.fr/perso/lsimon/glucose/
[2] https://www.lrde.epita.fr/wiki/PaInleSS
--
You received this message because you are subscribed to the Google Groups
"sage-devel" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to sage-devel+unsubscr...@googlegroups.com.
To post to this group, send email to sage-devel@googlegroups.com.
Visit this group at https://groups.google.com/group/sage-devel.
For more options, visit https://groups.google.com/d/optout.
