Hi folks, I want to present you a small, yet powerful, library (https://github.com/Lipen/kotlin-satlib) that provides an API for SAT solvers and implements some common operations for constraint programming, such as: handling finite-domain variables (e.g.: int in a small range; custom enum; set of values), storing named “variables” in the context, encoding common logic operations over SAT literals (Tseytin-encoded, when necessary), declaring cardinality constraints (for now, only Totalizer encoding is supported, but it works pretty well in general), solving AllSAT.
The generic interface of the SAT solver is not based on the standard IPASIR one, but is more pragmatic and user-friendly. It consists of the most commonly used operations performed with the SAT solver:
- you can allocate new literals,
- declare new clauses,
- reset the solver,
- solve the SAT problem itself (including solving under assumptions),
- query the resulting values of literals,
- query the whole model (the solution to the SAT problem) itself.
- Less common operations are implemented in a form of Kotlin extension functions, for example, the aforementioned encodings of logic ops form a DSL.
Alongside with the SAT solver interface and its extensions, `kotlin-satlib` provides wrappers for native SAT solvers (these days, most of them are written in C/C++) implemented using JNI technology. Currently, the solvers included are: MiniSat, Glucose, Cadical and CryptoMiniSat. Sadly, `kotlin-satlib` won’t work out-of-the-box, you have to provide it with some external SAT solver, either in the form of a library or a binary. Luckily, there are build instructions for each of the supported SAT solver, both for Linux and Windows. Checkout the README!
The project itself was originally based on https://github.com/mmaroti/jnisat.
Feel free to leave comments, suggestions and new ideas, I’d really appreciate them all! If you are using SAT solvers programmatically, tell me about your use cases, and I will try to add the useful functionality to kotlin-satlib.