Ever wondered how to efficiently use modern SAT solvers from the JVM world (Java/Kotlin/etc)?
This project provides the common interface for SAT solvers, various operations and primitives, and JNI wrappers for native C/C++ solvers, such as MiniSat or Cadical.
repositories {
maven(url = "https://jitpack.io")
}
dependencies {
implementation("com.github.Lipen.kotlin-satlib:core:${Versions.kotlin_satlib}")
}Examples can be found here.
with(MiniSatSolver()) {
val x = newLiteral()
val y = newLiteral()
val z = newLiteral()
println("Encoding exactlyOne(x, y, z)")
exactlyOne(x, y, z)
println("nVars = $numberOfVariables")
println("nClauses = $numberOfClauses")
println("Solving...")
check(solve())
println("model = ${getModel()}")
println("Solving with assumption x=true...")
check(solve(x))
println("model = ${getModel()}")
check(getValue(x))
println("Solving with assumption y=true...")
check(solve(y))
println("model = ${getModel()}")
check(getValue(y))
println("Solving with assumption z=true...")
check(solve(z))
println("model = ${getModel()}")
check(getValue(z))
println("Everything OK.")
}In order to use wrappers for native SAT solvers (e.g., MiniSatSolver), you need two native libraries:
-
Shared library for SAT solver (e.g.,
libminisat.so). -
Shared library for JNI wrapper (e.g.,
libjminisat.so).
When you use the solver (e.g. JMiniSat) first time, it loads the native library via Loader.load("jminisat") which tries to load them from 'resources' folder.
-
On Linux, place j-libs in
/path/to/kotlin-satlib/jni/src/main/resources/lib/linux64. -
On macOS, use
osx64subfolder. -
On Windows, use
win64subfolder.
|
💡
|
If you are using kotlin-satlib as a dependency for your project, place j-libs inside <your-project>/…​/resources/lib/<platform> folder.
|
Each j-lib depends on the SAT solver shared library, e.g., jminisat depends on libminisat.so.
Dependent libs are loaded transitively, so you just have to ensure they can be located in runtime.
-
On Linux, this implies calling
ldconfig -n <dir-with-libs>and/or usingLD_LIBRARY_PATH. -
On macOS, you can set
DYLD_LIBRARY_PATHenvironment variable with path to your.dylibfiles. -
On Windows, the standard way of ensuring discoverability of DLLs is placing them "in the current directory", but, from my experience, it does not work, so you have to place solver shared libs, e.g.,
minisat.dll, insideC:/Windows.
If you want to compile everything yourself, consult build instructions and CI workflow.
You can simply download prebuilt native libraries from GitHub Releases page. As an example, you can set up the following Gradle task in your project:
Example Gradle task which downloads shared libs:
import de.undercouch.gradle.tasks.download.DownloadAction
plugins {
id("de.undercouch.download") version "4.1.1"
}
fun Task.download(action: DownloadAction.() -> Unit) =
download.configure(delegateClosureOf(action))
val osArch: String = run {
val osName = System.getProperty("os.name")
val os = when {
osName.startsWith("Linux") -> "linux"
osName.startsWith("Windows") -> "win"
osName.startsWith("Mac OS X") || osName.startsWith("Darwin") -> "osx"
else -> return@run "unknown"
}
val arch = when (System.getProperty("os.arch")) {
"x86", "i386" -> "32"
"x86_64", "amd64" -> "64"
else -> return@run "unknown"
}
"$os$arch"
}
tasks.register("downloadLibs") {
doLast {
val urlTemplate = "https://github.com/Lipen/kotlin-satlib/releases/download/${Libs.Satlib.version}/%s"
val libResDir = projectDir.resolve("src/main/resources/lib/$osArch")
fun ensureDirExists(dir: File) {
if (!dir.exists()) {
check(dir.mkdirs()) { "Cannot create dirs for '$dir'" }
}
check(dir.exists()) { "'$dir' still does not exist" }
}
fun downloadLibs(names: List<String>, dest: File) {
ensureDirExists(dest)
download {
src(names.map { urlTemplate.format(it) })
dest(dest)
tempAndMove(true)
}
}
when (osArch) {
"linux64" -> {
val jLibs = listOf(
"libjminisat.so",
"libjglucose.so",
"libjcms.so",
"libjcadical.so"
)
downloadLibs(jLibs, libResDir)
val solverLibs = listOf(
"libminisat.so",
"libglucose.so",
"libcryptominisat5.so",
"libcadical.so"
)
val solverLibDir = rootDir.resolve("libs")
downloadLibs(solverLibs, solverLibDir)
}
"win64" -> {
val jLibs = listOf(
"jminisat.dll",
"jglucose.dll",
"jcadical.dll",
"jcms.dll"
)
downloadLibs(jLibs, libResDir)
val solverLibs = listOf(
"libminisat.dll",
"glucose.dll",
"cadical.dll",
"libcryptominisat5win.dll"
)
val solverLibDir = rootDir.resolve("libs")
downloadLibs(solverLibs, solverLibDir)
}
else -> {
error("$osArch is not supported, sorry")
}
}
}
}After downloading solver shared libs, update ld cache:
sudo ldconfig $(realpath libs)