Discussion: Rust bindings for SAT solvers

[lixitrixi]

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]

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]

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]

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]

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]

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

[ChrisJefferson]

One small comment, but I'll put it here so it will be picked up if anyone ever does some SAT work.

I have personally had a lot of success with rustsat ( https://github.com/chrjabs/rustsat/ ) , including making some PRs myself which fixed some issues I had.

I'd recommend enabling the ["ipasir-display"] feature. This makes the names of printed out SAT variable names line up with what is actually passed to the solver. The default is something nicer, but if we end up having to debug how the SAT solvers are actually behaving (which we probably will at some point), from experience I can tell you life is much easier if you can get the names for the variables the underlying solver is using.

The reason to turn this on early, and globally, is it's easy for these names to end up in tests, and then enabling the option would break tests, which is annoying.