Implemented an interface to BatSat

[nfbruns]

Description of the Contribution

Implemented an interface to the BatSat solver (https://github.com/c-cube/batsat)

Questions / Considerations

The add_clause_reuse(&mut c) function in fn add_clause(&mut self, clause: Clause) returns false if the Solver is in an UNSAT state. Should we handle that with an error message or just return Ok(()) as it is now?
My suggestion is that since we have no way to remove clauses from this solver, there cannot be a way to get the solver out of the UNSAT state, therefor, the return of Ok(()) is fine, even if the clause was not added.

PR Checklist

• I read and agree to CONTRIBUTING.md
• I have formatted my code with rustfmt / cargo fmt --all
• Commits are named following conventional commits
• I have added documentation for new features
• The test suite still passes on this PR
• I have added tests for new features / tests that would have caught the bug this PR fixes (please explain if not)

[chrjabs]

Without having time to look at this closely right now, for a solver that is purely written in rust, I wonder whether it makes more sense to implement the RustSAT traits either in the main RustSAT crate (behind a feature switch) or in the original solver crate. That would eliminate an additional crate in the dependency graph, enable more optimizations for the compiler and make the implementation a bit nicer by, e.g., allowing implementations of the From trait to convert between RustSAT and solver types. (Would for example be interesting here for the lbool <=> TernaryVal relationship.)
I mainly factored the C-based solvers out because of the required external C build.

[chrjabs]

@nfbruns, do you have where this implementation would make the most sense? Are there any specific reasons why you implemented this as a separate crate other than that that's what I did so far for solvers?
My thoughts on the different options of implementing the Solve trait (and related) for a solver implemented in Rust right now are the following:

• Implementation in rustsat-<solver> crate: seems a bit overkill for this little code "between" RustSAT and the actual solver
• Implement with the original solver: very dependent on the solver developer, whether they're interested to support RustSAT / how quickly they would make updates if the RustSAT API changes
• Implement in main rustsat crate behind feature with optional dependency on the solver crate: probably my favourite. As outlined above, this eliminates an unnecessary type, makes some of the implementation simpler and shouldn't really have any drawbacks for using RustSAT without the solver either (by not activating the feature). This also seems similar to what PyO3 seems to for example do to support anyhow / serde, even though arguably their usecase is more similar to implementing this in the solver crate behind a feature.

[nfbruns]

I went directly with implementing it using the rustsat-<solver> setup since I have understood that to be the preferred way. But I completely understand your thoughts. I will try to summarize my opinions for the different options:

• Implementation in rustsat-<solver> crate:
  I agree that for this "little" interface for batsat this is a bit of an overkill. Still i think it makes sense to handle it in this way since now anyone can implement a new solver interface in a separate crate and share it with the Opern Source world - and if you see it as "important enough", you can add it to the rustsat git repository or else it can continue to live as a seperate crate.

• Implement with the original solver
  Of cause it depends on the maintainers of the original solver crates and their willingness to cooperate. One further downside would be the handling of interface changes to rustsat. If a interface changes in rustsat, all the other creates would need to update too, which needs a lot of cumminication, the availaility of the maintainers and could lead to a mess of interface versions. (except if the current version is stable enough to be considered "unchanching")

• Implement in main rustsat crate behind feature
  Also possible. In my Solver implementation (which extends yours), I have handled it so that in the core crate rustsat-<solvers> are dev-dependencies used for testing. In the other crates I import the core crate and an applicable solver. This has so far worked really well. I think that feature flags kind of defeats the principle of "separation of concern" since the core rustsat crate defines the traits and the solvers implement it. Having the solvers in the rustsat core as features and other solvers as crates from the community would make it a bit inconsistent, i think.

I hope that helps, let me know what your thoughts are.

[chrjabs]

Thanks for laying out your thoughts. I agree that having all solvers structured in the same way has its advantages. Here are some more thoughts.

• At the current early stage of this library, it is probably indeed better to maintain the trait implementations in this project rather than in potential solver crates to avoid work for the solver developers to adjust to changes in the trait definitions.
• Regarding the wrapper type, I'm less thinking of performance (the type is transparent indeed, so that shouldn't be an issue, but of usability. Needing the wrapper type means that functionality of the core solver that is not available via RustSAT traits are not accessible any more. I guess as a workaround something along the lines Wrapper::core_mut(&mut self) -> &mut Core and the respective _ref can and should be available, but that is slightly less ergonomic.

Another open question about doing it this way that I still have is related to authorship and ownership on crates.io. In this PR you specified yourself as the author of the crate, which is definitely valid, since you wrote the code. If this makes it into the main repository, releases will be done through the CI and crates.io ownership will therefore have to be under my account. Are you find with that? I guess I might have to add something like that to the contribution guideline as well.

Related to your question about why you cannot extend foreign types with foreign traits: as explained here this might lead to conflicts if a crate depends on two traits that define a trait differently for the same type.

Let me know if you hear back from the BatSat devs, but as mentioned above, I guess we'll more likely end up with one of the different options.

[chrjabs]

It's been a while now. I think by now I'm settled on it being a pragmatic solution to go with the rustsat-<solver> crate indeed.
Are you still up for putting in the work to get this merged? Mainly, since this PR was opened, I introduced the solvertests crate to unify solver tests, this PR should be adapted to use that, and the workspace dependencies I introduced on the next-major branch.

[nfbruns]

Hi Christoph,
I am very sorry, i did not get notifications and the last weeks i have been on a trip around the world. But well I am happy with the pragmatic solution as well! I just fixed the merge conflicts from main. In terms of the authorship issue, i would write my name in the batsat toml but i am completely fine with publishing it under your name for the crates.io part.

And yes, I am up for putting in the work to get this merged! I will start to implement your new testing api and make it compatible for the next-major branch. Thanks a lot and i will rerequest review as soon as it is ready!

[nfbruns]

I added the new Test interface -which is a lot simpler to use-!

In terms of the workshop dependencies, should I address this with this PR already or should this be merged to the current main and then upgraded to next-major in a separate PR?

[chrjabs]

In terms of the workshop dependencies, should I address this with this PR already or should this be merged to the current main and then upgraded to next-major in a separate PR?

Even though I don't know yet when the next major release will happen, I think it would make sense to directly target next-major with this PR, rather than main and then have more work down the line. The other main change that I did on the next-major branch is to activate pedantic clippy linting, which will probably mean some adjustments in this code as well.
The downside is that releasing this interface will take a bit more time (only with the next major release of RustSAT). Are you fine with that?

[nfbruns]

I am fine with that!
I updated the target to merge to next-major and fixed the workspace dependencies as well as the linting warnings. From my side, this should be ready to merge now!

[chrjabs]

Thanks for continuing to work on this. There are some more things that I hadn't spelled out in detail before, most of them to do with the CI. In addition to the changes I marked here, please make the following changes in files that GitHub won't let me mark changes in:

• In .github/workflows/docs.yml, change line 35 to

  for dir in tools cadical kissat minisat glucose batsat ipasir capi pyapi; do
  

• In .github/workflows/semver-checks.yml add the following block at the bottom

        - name: BatSat
          uses: obi1kenobi/cargo-semver-checks-action@v2
          with:
            package: rustsat-batsat
  

• In release-plz.toml add the following at the bottom so that the crate isn't immediately release when this hits main. I'll remove this when it should be released. (I unfortunately don't know a nicer way of dealing with this.)

  [[package]]
  name = "rustsat-batsat"
  release = false
  git_release_enable = false
  

[nfbruns]

Thank you for the comments and suggestions to get the CI to work! I tried to address all the CI changes and also the clippy warnings and hope that it will work now. If there is anything left to change or not documented well, please let me know!

[chrjabs]

One more small thing, I forgot to tell you to add "BatSat" in the list of ignored named in clippy.toml.

[chrjabs]

Just so you know, the semver check failing is to be expected for the next-major branch. The failing doc test points out that the readme is not up-to-date with the crate documentation.

[nfbruns]

Just so you know, the semver check failing is to be expected for the next-major branch. The failing doc test points out that the readme is not up-to-date with the crate documentation.

Oh yes, i forgot to run cargo rdme after i added a comment! I pushed a now commit that shoud fix this issue.

[chrjabs]

Great. If you address the requested changes above, I think we should be pretty much ready to merge.

[nfbruns]

I addressed the clippy and documentation issues. I hope that it is so far ready to ship now!

[chrjabs]

Great. Thanks for sticking with this through all the details. I'll merge this soon, but I'll probably squash it down into fewer commits.

[nfbruns]

Thank you very much for taking the time to review and also for the interesting discussions along the way about how to approach the integration, how to deal with rust specifics and how to code certain parts!

[chrjabs]

I now (manually) merged this in 4d15c0f. I also did a little bit more work (98af54b) to generalize the interface to generic BatSat callbacks and to implement SolveStats, which is required for a solver to implement the CollectClauses trait that RustSAT encodings rely on.
Thanks again for your work on this.

[chrjabs]

For completeness, I now finally got to some housekeeping and this is now finally officially published. Thanks again for working on this.