General API ergonomics improvements

[ChrisJefferson]

I have a situation where I need to keep recreating the solver. There is a significant amount of time spent cloning the cnf, because add_cnf, which calls add_clause, both take by value.

Looking at the implementations of add_clause, none of them seem to actually need the clause by value -- but changing add_clause to accept &Clause "breaks the world", as it would need changing every call to add_clause.

My best suggestion (assuming you are happy to improve it), would be to add add_cnf_ref and add_clause_ref to Solver. These will allow people (like me) to add cnf and clauses by reference, and will only require implementing add_clause_ref to each solver (which, from trying out with kissat, actually can be done by just renaming add_clause to add_clause_ref, and then making add_clause call add_clause_ref, because the add_clause implementations don't actually need the clause by value).

[suomela]

This would be awesome, I was also wondering if it is really necessary to pass by value. It wasn't a performance issue for me, but just led to a somewhat ugly code with lots of cloning. Also e.g. to_dimacs_path takes SatInstance by value, which shouldn't be necessary?

A somewhat related issue is that I'd often want to quickly print out the number of variables and clauses, and inst.n_clauses() works fine with a reference, but inst.var_manager().n_used() requires a mutable reference, which is often inconvenient.

[chrjabs]

Very insightful feedback, thanks. Since so far I have mostly been the only user of this library, I mainly wrote the API in a way that worked for me, trying to somewhat think about potential other use cases, but it's always better to get proper feedback.
Here are some thoughts on the API ergonomics mentioned so far:

• add_clause: I think I made this take by value thinking that in theory a Rust SAT solver could truly take ownership of a clause. Given that all supported solvers are external, copy clauses literal by literal, and don't even have the same concept of ownership, in hindsight that does not make that much sense. I agree that introducing add_clause_ref seems like an easy and very doable fix for this issue.
• var_manager(): I think introducing a similar var_manager_ref() to be able to access the variable manager without mutability is a good idea. This of course implies that the original method should rather have been named var_manager_mut(), which one could introduce as well and deprecate the original var_manager().
• to_dimacs_path: this one is slightly more tricky. to_opb_path can actually take by reference, but to_dimacs_path would at least need to take by mutable reference, which I think would be confusing. This is because SatInstance supports non-clausal constraints, while DIMACS CNF does not. So if the instance object contains PB constraints, to_dimacs_path will convert them to CNF, mutating the instance, before writing it to file. Rather than changing the signature of SatInstance::to_dimacs_path, one could introduce Cnf::to_dimacs_path, which would not need mutability.

How do these ideas sound to you for your usecases? Also, it would be great if you could drop any further inconveniences you run into in your applications here.

[suomela]

Maybe I can expand a bit on my typical use cases. For me it's often convenient to define something like

struct Foo {
    inst: SatInstance,
    // plus all kinds of parameters that specify what kind of an instance we are building
    // plus all kinds of things that help with mapping domain-specific objects to variables of "inst"
}

Then high-level code might look a bit like this:

let foo = Foo::new(...);
foo.build_instance(...);
foo.solve_instance(...);

And here it would be natural that build_instance() and all helper methods it calls take &mut self (as it will modify foo.inst and other structures), while solve_instance() and all helper methods it calls would only need to take &self, and solving could be even parallelized.

I understand the challenge that SatInstance ≠ Cnf. Maybe I should rethink the structure so that we have:

struct Foo {
    inst: SatInstance,
    cnf: Cnf,
    // ...
}

and the final step of build_instace() will also turn inst into cnf, and solve_instance would ignore inst and only use cnf. Is this closer to the way the library is intended to be used?

For this to work with external solvers one would indeed need to have Cnf::to_dimacs_path.

[chrjabs]

I see. Do you ever incrementally change the SatInstance after the initial build_instance call? If not, I would even suggest only keeping the Cnf around or (if you are not using any PB constraints when creating the instance) only ever working with a Cnf. I somewhat intentionally kept the Cnf struct simpler and more light weight, so that might mean a bit more manual work, but if you only have clausal constraints, it shouldn't be that much.

[suomela]

One small API inconvenience:

It's a common use case for me that I have e.g. lits: Vec<Lit> and I'd like to add it as a clause. Now it's something like inst.add_clause(lits.as_slice().into()), but maybe there could be a convenience method that would let me do e.g. inst.add_xxx(&lits) in this case? After all, we can conveniently use &[Lit] in e.g. add_clause_impl_clause, so this would be analogous. I do not know what would be a good naming convention here, though. Maybe add_nary so that it's following the pattern add_binary and add_ternary?

[ChrisJefferson]

Just for your information, I'll give you an overview of what I'm doing :)

I'm actually generating my SAT instance using an external program ( https://github.com/conjure-cp/conjure ), which takes a high-level language and turns it into SAT. I then I have a little structure like:

pub struct SatCore {
    pub solver: Arc<Mutex<Solver>>,
    pub cnf: Arc<Cnf>,
}

Then I create a thread local copy of this using the thread_local package, so every thread gets it's own solver.

I then use rayon to solve problems in parallel which require lots of solving SAT instances.
For boring technical reasons (I can explain, or at some point I'll write a paper :) ), I sometimes need to assign a bunch of literals, and then later I need to 'unassign' them which you can't really do, so I just recreate the solver from the Cnf (I know I could do this with assumptions, but I get much better performance by assigning for my problem), so I recreate the solve by doing:

          let mut solver = Solver::default();
            solver
                .add_cnf(self.cnf.as_ref().clone())
                .expect("FATAL: Solver bug");

Then pop it into the mutex:

            let mut mutex_solver = self.solver.lock().unwrap();
            *mutex_solver = solver;

Good news, this works really well! My laptop has 32 cores, which I can saturate fairly easily just using rayon's par_iter.

[chrjabs]

I assume neither of you are relying directly on the public API in rustsat::instances::fio, so if I make changes in that it won't cause significant work for you?

[ChrisJefferson]

No, but also in general as it's early days for the library, I'm happy to do any fixing -- one reason I've moved to using rust rather than pysat in Python (which is what I used to use, and is a well-written library) is that I just got annoyed that misuses of APIs in Python aren't caught until runtime, while in Rust when you change an API, you just whiz around in your editor and change all the places you call it, doesn't take long and I know I've fixed it :)

[chrjabs]

I merged a fairly large PR implementing these improvements just now. Please see the newly added migration guide for what changes will be necessary to be made. I am hoping to actually publish a proper release once I get something for #79 working as well (as something I would want to do related to that might lead to some more breaking changes).