search

conjure-cp / conjure-oxide

Mozilla Public License 2.0
6 stars 8 forks source link

Discussion: Rust bindings for SAT solvers #2

Open lixitrixi opened 11 months ago

lixitrixi commented 11 months ago

In the spirit of rewriting as little existing code as possible for the Rust part of this project, I thought I would take a deeper look at various available bindings to Conjure's SAT solvers.

rustsat This is a Rust library which binds to many of the SAT solvers included with Conjure. It includes Kissat, Glucose, and MiniSAT. It's missing CaDiCaL and Lingeling. I'm not including SMT or MaxSAT solvers for now. License: MIT

kissat-sys This crate is a part of the high-level kissat-rs library and includes low-level bindings to the Kissat solver. We could potentially use this for Kissat if rustsat is a no-go. License: MIT

Using the IPASIR SAT interface with this project for increased compatibility was also discussed. Many of the solvers in Conjure themselves don't implement that interface; will part of the goal of this project be to resolve that?

  1. Kissat's interface - It seems full IPASIR compatibility is still under development, according to this issue.
  2. Lingeling's interface (see "main interface as in PicoSAT") - Since this is basically an older version of Kissat and probably no longer maintained, interface compatibility is probably not going to happen on their end. (Edit: see Dec 4 comment)
  3. These are just examples... let me know if I should provide any more!

If rustsat is a good fit I can start adding it to the project, we can discuss this on Wednesday as well!

lixitrixi commented 11 months ago

There is also a library for CaDiCaL under the MIT license. As far as I can tell there are no libraries available for Lingeling. I could potentially work on Lingeling and could pass the work of adding the existing interfaces to someone else.

@ozgurakgun what do you think would be best?

ChrisJefferson commented 11 months ago

Not already in Rust, but I will point out https://github.com/pysathq/pysat/ (A python SAT binding), just because it binds many solvers, and in some cases they have patched solvers so they can be used as libraries, so this code may be useful if you want to add more solvers later.

You can see the binding code here: https://github.com/pysathq/pysat/blob/master/solvers/pysolvers.cc -- obviously this is binding to Python so it is not at all useful directly, but shows how it is fairly simple to do the binding to many solvers.

lixitrixi commented 9 months ago

For future reference, here is the link to the IPASIR repository: https://github.com/biotomas/ipasir

It seems that Lingeling is supported, as well as MiniSAT.

lixitrixi commented 9 months ago

And here is a Rust crate for IPASIR, in case we go down this route when adding all of the SAT solvers: https://docs.rs/ipasir/latest/ipasir/

ozgurakgun commented 6 months ago

should we capture this (the options and what we are doing at the moment) in the wiki and close the issue? ping @lixitrixi