Feature request: make it easier to use other SAT solvers (e.g. kissat)

[fzaiser]

In some cases, kissat is an order of magnitude faster than minisat, which is the default used by CBMC. In one example, I've seen a reduction in running time by a factor of 15.

To use kissat currently, you need to build it yourself and run

kani --enable-unstable --cbmc-args --external-sat-solver path/to/kissat

It would be nice to be able to run kani --solver kissat instead.

Even better, we could even look into shipping Kani with kissat, so the user does not have to build it himself. The license of kissat (MIT) is compatible with Kani's.

As a further improvement, we could consider running multiple solvers in parallel and cancel the runs as soon as one of them finishes.

[weaversa]

Since different solvers have different capabilities, even better would be to allow for this configuration at the kani::proof level.

  #[kani::proof]
  fn my_fun() {
    kani::set_solver("kissat"); // or something
    ...
    assert_eq!(...);
  }

[fzaiser]

@weaversa I like that idea. But the solver would have to be set once per proof harness and cannot change within the harness. So something like #[kani::proof(solver = "kissat")] would make more sense, I think.

[weaversa]

@weaversa I like that idea. But the solver would have to be set once per proof harness and cannot change within the harness. So something like #[kani::proof(solver = "kissat")] would make more sense, I think.

Even better! And once that interface (at the proof level) works one could imagine passing in other prover tactics such as uninterpret this set of functions, or 'rewrite all instances of x with y', etc.