You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
@blyxxyz What are your thoughts on shipping the library with a SAT solver in tow? Having a decent one at the ready, it would open the door to greatly simplifying and speeding up many checks (which can be recast as a SAT/UNSAT call).
Going to open a branch doing this with kissat. It's an updated version of cadical that won the recently held contest. Compiles and runs nicely on Linux-based systems.
Just now coming to the realization that the wrap you have on D# might have been to keep the library viable on Windows as well. This the case? The CI/CD only considers Linux based systems, so I hadn't thought about it.
I'll continue with the modifications to ship with a SAT solver included, but can revert back to something similar to dsharp.py if it's best kept generic.
Not just on Windows, but also on weird distros (or even normal ones, portable Linux binaries are tricky), ARM, etc. Native code complicates things.
Bundling an executable could be ok, maybe there should be one for dsharp, but there should at least be an easy option to use your own executable instead. Maybe the bundled executable could be a fallback.
Calling external programs works but it's a little dirty. You have to know where it's installed and communicating with it is fiddly. The current nnf.dsharp is not ideal. Native modules are better, but harder to package.
I think pysat would be a great fit here. It compiles a bunch of SAT solvers into native modules with a consistent Python interface on top, so the trickiest work is already done. It doesn't support kissat, but it does have Cadical, and kissat support could perhaps be added.
pysat could then be an optional dependency of nnf, with a module nnf.pysat implementing an interface for it.
This would also work towards the "high-level support for arbitrary Boolean formulas" goal on their To-Do list.
I think the naive solve might be the best default, because it's the most shallow and predictable. Using a third party solver adds a translation step and leaves you at the mercy of its own bugs and design quirks (see e.g. this note for nnf.dsharp). If you don't need the performance it's a step down.
Defaulting to a shipped executable has additional problems. If it crashes, do you assume it's unusable on this platform and disable it for the rest of the run? Do you report the crash if you can figure out that's not it? If we're too clever with this a user might assume they're using kissat when it's actually being blocked because of something they could trivially fix if they knew about it.
I'm currently leaning towards letting the user opt in to a specific strategy. Then you don't have to be coy about showing crashes and it's easier to know what's going on.
But that's a decision to make later once we know how the implementations behave.
Maybe the bundled kissat should be put on hold from now? It looks like the advantage over the best pysat has to offer is fairly modest, and if kissat were added to pysat it would be near-obsolete.
My concern with leaving kissat to pysat isn't just on the slight improvement we'd get by using it over whatever's available, but rather the overhead in installing pysat to begin with. It naturally has some hoops to jump through since there are some binaries to obtain. For those on a Linux based system, then having the simple in would be extremely helpful.
The current use-case is an upcoming course -- it's unclear if I'll be able to manage a pysat installation given the systems the students will be using, but shipping a linux-based binary certainly works. They'll need decent SAT & KC solver access as part of it.
Point taken on the unexpected behaviour of 3rd party solvers. I guess I can use this as an opportunity to put in the dynamic library configuration. Eventually, the d4 compiler should be an equally swappable backend for what dsharp does, and the input / output should be roughly the same.
Ah. I thought earlier that pysat had Linux wheels, but I see now that it has only win and macosx wheels.
I don't know if the students' systems are uniform enough for self-built wheels to be an option, but at best that would still be less plug-and-play. Bundling kissat seems worth the trouble.
Linux wheels will be eventually added to pysat. The reason they are missing is that I though Linux was the least trouble-making platform. :) But I hear people sometimes complain about compiling it on Linux too... So it will be added for sure, at some point.
Thanks @alexeyignatiev ! It's particularly important when we need extremely turnkey setups like having students run stuff on repl.it -- essentially some quick and simple pip installations are the best bet there.
Thanks @alexeyignatiev . Doesn't seem to want to go on the setup we have -- https://repl.it/ . Eventually, I was able to get it going, but it took several tries to make it. My hunch is that the service is just very resource-constrained, and fails randomly when it hits a cap. If it allowed me to do something similar to a dockerized setup, then that would work, but as is the students will be unforgiving at the time/troubles with it.
Outside of the course context, integrating pysat into python-nnf still makes loads of sense (as discussed elsewhere).
Btw, you can give it a try yourself -- usage examples are loaded here.
What was the problem exactly? I tried it myself yesterday and got some issue of py-aiger-sat being in conflict with the latest version of PySAT. This is weird! There is no dependency on py-aiger-sat in PySAT. Anyway, I have already reported this issue.
Well currently that repl.it link seems to work but takes time (order of minutes). Previously, it was fussing around with numpy (which I don't think sits in the dependency chain at all). Ultimately, the system is fairly lightweight and seemingly brittle -- so the less I put in as a dependency for the repo they will be cloning, the better. This is a pretty specific use-case, though.
@haz it takes this long because it compiles PySAT.
In your case, you install version 0.1.5.dev13 - note that there is no binary wheel for this version. If you try the latest one (0.1.6.dev5), it will be installed quickly. But then it complains about py-aiger-sat, which has nothing to do with the dependencies of PySAT. Is this a bug in repl.it?
This is annoying. I don't get why it tries to install py-aiger-sat if I want to use python-sat - it is a third-party project and there is no dependency on it...
OK, @mvcisback kindly fixed this dependency issue very quickly. So if you want to use the latest version of PySAT on repl.it, you should be able to install it with no problem as the latest version (0.1.6.dev5) is available in the binary wheel for Linux.
Made a foolish late-night error in testing things -- pysat != python-sat. That's what was causing the heavy-hitting installation. This look about right?
Activity
haz commentedon Jul 24, 2020
@blyxxyz What are your thoughts on shipping the library with a SAT solver in tow? Having a decent one at the ready, it would open the door to greatly simplifying and speeding up many checks (which can be recast as a SAT/UNSAT call).
haz commentedon Jul 30, 2020
Going to open a branch doing this with kissat. It's an updated version of cadical that won the recently held contest. Compiles and runs nicely on Linux-based systems.
haz commentedon Jul 30, 2020
Just now coming to the realization that the wrap you have on D# might have been to keep the library viable on Windows as well. This the case? The CI/CD only considers Linux based systems, so I hadn't thought about it.
I'll continue with the modifications to ship with a SAT solver included, but can revert back to something similar to
dsharp.pyif it's best kept generic.blyxxyz commentedon Jul 30, 2020
Not just on Windows, but also on weird distros (or even normal ones, portable Linux binaries are tricky), ARM, etc. Native code complicates things.
Bundling an executable could be ok, maybe there should be one for
dsharp, but there should at least be an easy option to use your own executable instead. Maybe the bundled executable could be a fallback.Calling external programs works but it's a little dirty. You have to know where it's installed and communicating with it is fiddly. The current
nnf.dsharpis not ideal. Native modules are better, but harder to package.I think
pysatwould be a great fit here. It compiles a bunch of SAT solvers into native modules with a consistent Python interface on top, so the trickiest work is already done. It doesn't support kissat, but it does have Cadical, and kissat support could perhaps be added.pysatcould then be an optional dependency ofnnf, with a modulennf.pysatimplementing an interface for it.This would also work towards the "high-level support for arbitrary Boolean formulas" goal on their To-Do list.
haz commentedon Jul 30, 2020
Oy, absolutely that's the route to go.
pysathq/pysat#61
Will run with this cascade whenever someone calls for a satisfying assignment or satisfiability check:
pysatfirstkissatnextThat make sense?
blyxxyz commentedon Jul 30, 2020
I think the naive solve might be the best default, because it's the most shallow and predictable. Using a third party solver adds a translation step and leaves you at the mercy of its own bugs and design quirks (see e.g. this note for
nnf.dsharp). If you don't need the performance it's a step down.Defaulting to a shipped executable has additional problems. If it crashes, do you assume it's unusable on this platform and disable it for the rest of the run? Do you report the crash if you can figure out that's not it? If we're too clever with this a user might assume they're using
kissatwhen it's actually being blocked because of something they could trivially fix if they knew about it.I'm currently leaning towards letting the user opt in to a specific strategy. Then you don't have to be coy about showing crashes and it's easier to know what's going on.
But that's a decision to make later once we know how the implementations behave.
Maybe the bundled
kissatshould be put on hold from now? It looks like the advantage over the bestpysathas to offer is fairly modest, and ifkissatwere added topysatit would be near-obsolete.haz commentedon Jul 30, 2020
Aye, all too aware of that silly D# bug :P.
My concern with leaving
kissattopysatisn't just on the slight improvement we'd get by using it over whatever's available, but rather the overhead in installingpysatto begin with. It naturally has some hoops to jump through since there are some binaries to obtain. For those on a Linux based system, then having the simple in would be extremely helpful.The current use-case is an upcoming course -- it's unclear if I'll be able to manage a
pysatinstallation given the systems the students will be using, but shipping a linux-based binary certainly works. They'll need decent SAT & KC solver access as part of it.Point taken on the unexpected behaviour of 3rd party solvers. I guess I can use this as an opportunity to put in the dynamic library configuration. Eventually, the d4 compiler should be an equally swappable backend for what
dsharpdoes, and the input / output should be roughly the same.blyxxyz commentedon Jul 30, 2020
Ah. I thought earlier that
pysathad Linux wheels, but I see now that it has onlywinandmacosxwheels.I don't know if the students' systems are uniform enough for self-built wheels to be an option, but at best that would still be less plug-and-play. Bundling
kissatseems worth the trouble.alexeyignatiev commentedon Jul 31, 2020
Hi all,
Linux wheels will be eventually added to
pysat. The reason they are missing is that I though Linux was the least trouble-making platform. :) But I hear people sometimes complain about compiling it on Linux too... So it will be added for sure, at some point.haz commentedon Jul 31, 2020
Thanks @alexeyignatiev ! It's particularly important when we need extremely turnkey setups like having students run stuff on repl.it -- essentially some quick and simple pip installations are the best bet there.
alexeyignatiev commentedon Aug 4, 2020
Hi all, the latest version of
pysatshould be available in binary wheels for linux. Please, check if this works for you.haz commentedon Aug 5, 2020
Thanks @alexeyignatiev . Doesn't seem to want to go on the setup we have -- https://repl.it/ . Eventually, I was able to get it going, but it took several tries to make it. My hunch is that the service is just very resource-constrained, and fails randomly when it hits a cap. If it allowed me to do something similar to a dockerized setup, then that would work, but as is the students will be unforgiving at the time/troubles with it.
Outside of the course context, integrating
pysatintopython-nnfstill makes loads of sense (as discussed elsewhere).Btw, you can give it a try yourself -- usage examples are loaded here.
alexeyignatiev commentedon Aug 5, 2020
What was the problem exactly? I tried it myself yesterday and got some issue of
py-aiger-satbeing in conflict with the latest version of PySAT. This is weird! There is no dependency onpy-aiger-satin PySAT. Anyway, I have already reported this issue.haz commentedon Aug 5, 2020
Well currently that repl.it link seems to work but takes time (order of minutes). Previously, it was fussing around with numpy (which I don't think sits in the dependency chain at all). Ultimately, the system is fairly lightweight and seemingly brittle -- so the less I put in as a dependency for the repo they will be cloning, the better. This is a pretty specific use-case, though.
alexeyignatiev commentedon Aug 5, 2020
@haz it takes this long because it compiles PySAT.
In your case, you install version
0.1.5.dev13- note that there is no binary wheel for this version. If you try the latest one (0.1.6.dev5), it will be installed quickly. But then it complains aboutpy-aiger-sat, which has nothing to do with the dependencies of PySAT. Is this a bug in repl.it?alexeyignatiev commentedon Aug 5, 2020
This is annoying. I don't get why it tries to install
py-aiger-satif I want to usepython-sat- it is a third-party project and there is no dependency on it...alexeyignatiev commentedon Aug 5, 2020
OK, @mvcisback kindly fixed this dependency issue very quickly. So if you want to use the latest version of PySAT on repl.it, you should be able to install it with no problem as the latest version (
0.1.6.dev5) is available in the binary wheel for Linux.haz commentedon Aug 5, 2020
Made a foolish late-night error in testing things --
pysat!=python-sat. That's what was causing the heavy-hitting installation. This look about right?