- Notifications
You must be signed in to change notification settings - Fork2
🗿 SAT solver wrappers for Kotlin
License
Lipen/kotlin-satlib
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
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 foundhere.
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 viaLoader.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 usingkotlin-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 onlibminisat.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, consultbuild instructions andCI workflow.
You can simply download prebuilt native libraries fromGitHub Releases page.As an example, you can set up the following Gradle task in your project:
Example Gradle task which downloads shared libs:
importde.undercouch.gradle.tasks.download.DownloadActionplugins { 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")funensureDirExists(dir:File) {if (!dir.exists()) { check(dir.mkdirs()) {"Cannot create dirs for '$dir'" } } check(dir.exists()) {"'$dir' still does not exist" } }fundownloadLibs(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)
About
🗿 SAT solver wrappers for Kotlin
Topics
Resources
License
Uh oh!
There was an error while loading.Please reload this page.
Stars
Watchers
Forks
Contributors3
Uh oh!
There was an error while loading.Please reload this page.