ipasir-sys

A Rust crate that contains FFI bindings for IPASIR-compatible SAT solvers.

This crate exposes the minimal low-level C interface to Rust. No more, no less. It does not try to provide safe wrappers or high level abstractions. Those things can be built on top of this crate which is inline with the *-sys naming convention as discussed in this article. Alternatively, you can use the ipasir-rs crate which does provide these things.

This crate will helpfully try to build Cadical if no solver is specified and has integration tests to verify the bindings work.

What is IPASIR?

IPASIR is a standard interface for incremental SAT solvers. It is the reverse acronym for Re-entrant Incremental Satisfiability Application Program Interface and was introduced at the 2015 annual SAT competition.

More explanation can be found in section 6.2 of this paper.

How to use this crate

There are two ways to use this crate:

1. You can provide your own static library of a solver that implements IPASIR
2. You can do nothing and the crate will try to build and link Cadical

The end result is the same. The IPASIR functions can be called by wrapping them in unsafe blocks:

use ipasir_sys::*;

fn main() {
    unsafe {
      let solver = ipasir_init();

      ipasir_add(solver, 1);
      ipasir_add(solver, 0);

      let sat_status = ipasir_solve(solver);
      assert_eq!(sat_status, 10);
    }
}

For a more comprehensive example, see coloring_test.rs or refer to interface_test.rs.

Providing your own library

You can provide your own static library by setting the IPASIR environment variable at build time:

$ IPASIR=/path/to/libsolver.a cargo build

The crate will copy the library to its build directory and try to link against it. You must use an absolute path but the library's name does not matter. If your library has other dependencies it is recommended you inline them into your static library. Alternatively, you can try to pass additional link flags to cargo.

Using Cadical

If the IPASIR environment variable is not set, the crate will try to compile a version of Cadical that is vendored as part of the crate. If this doesn't work, please try cloning this crate from GitHub and running cargo test on its own. It may also be helpful to refer to the Travis CI build and its configuration.

If you can't get it work, please open an issue.

Ideas for improvement

• Vendor more solvers and switch between them easily
• Improve operating system support (e.g. Windows)
• Add automated tests against different solvers and platforms

License

This crate has the MIT License but please check the license restrictions of the vendored software before using it.