Simple end-to-end example in Rust

[Coloquinte]

I'd like to use a pseudoboolean solver to optimize boolean function implementations in Volute. Rustsat seems like a nice option instead of implementing my own SAT encoding.

My issue is that I don't know where to start: tools in rustsat-tools seem to mostly use CNF/OPB files. The multi-objective solver that is linked from the doc is quite complex. I'd like a simple starting example to create a problem and solve it, like this one from cat_solver, but ideally for pseudo boolean as well.

Does such a simple API already exist? If so, could you point me to it?

Thank you, Gabriel

[chrjabs]

Thanks for your interest in rustsat. If you only want to solve pseudo-Boolean satisfiability, with a SAT silver backend, this should be possible to achieve with rustsat (more details below). At the moment, rustsat doesn't have a simple optimization (MaxSAT) backen.

Generally, you will want to create a Satin stance (these support pseudo-Boolean constraints) and build it up to the instance you want. (Using add_pb_constr.) After that, save the highest variable of the instance (if you don't know it already from somewhere else) and call as_cnf, which gives you a CNF formula to pass to the SAT solver. (The conversion to CNF introduces auxiliary variables, hence saving the number of variables before, to ignore them later.) Now pass the CNF to a solver (for this case, choose any, but the cadical interface is the most tested while kissat might be a bit better) and get your solution up to the variable you're interested in (or unsat of course).

After my Christmas break I can work on writing up an example for solving pseudo-Boolean satisfiability from an OPB file with a SAT solver backend in this way. (I'll leave the issue open till then.)

One more note, the encoding used for converting the pseudo-Boolean constraints in this way is the (Generalized) Totalizer encoding. If you need another encoding, you could use as_cnf_with_encoders instead, but I don't have many alternatives implemented yet. I'm mainly developing this library based on what I need for my own work.

[Coloquinte]

Thank you for the explanation and for your time!

I'll try and write a pull request with an example when I'm done with the implementation.

[Coloquinte]

I now use rustsat for logic optimization in volute. Thank you for the crate: it works flawlessly!

Right now my minimal example would look like this:

let mut instance: SatInstance<BasicVarManager> = SatInstance::new();
let l1 = instance.var_manager().new_var().pos_lit();
let l2 = instance.var_manager().new_var().pos_lit();
instance.add_clause(clause![l1, l2]);
instance.add_clause(clause![!l1, l2]);
let mut solver = rustsat_kissat::Kissat::default();
solver.add_cnf(instance.clone().as_cnf().0).unwrap();
assert_eq!(solver.solve().unwrap(), SolverResult::Sat);
let sol = solver.solution(instance.var_manager().max_var().unwrap()).unwrap();
assert_eq!(sol.lit_value(l1), TernaryVal::True);
assert_eq!(sol.lit_value(l2), TernaryVal::True);

It's a bit more verbose than I'd like, so I'd like to:

• Add SatInstance::new_var() and SatInstance::new_lit() methods as shortcuts
• Maybe doing away with the requirement to specify max_var in solution?

Would you be open to a PR for such changes?

[chrjabs]

Glad to hear that you got this to work. An overarching example like this would definitely be good to go on the main page of the documentation. In fact, I have a very similar example there now, see #49. In that PR I also implemented your suggestions for improvements, i.e., the shortcut methods and a full_solution method that doesn't require a specified maximum variable for solvers that implement SolveStats. (I very much welcome PRs, this just felt like a good task to get back into work today, which is why I implemented it myself.)

[Coloquinte]

I like it :) The other changes will help me quite a bit too, if you can make the CI work on macos and windows. I'm open to contribute, but I'm happy to have less work ;)

[chrjabs]

Turns out windows support for the solvers is not that simple #50. I'll work on that when I find some more time for it, for now I'm only checking linux and macos in ci.