SAT solver wrappers for Kotlin

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.

Installation

build.gradle.kts

repositories {
    maven(url = "https://jitpack.io")
}
dependencies {
    implementation("com.github.Lipen.kotlin-satlib:core:${Versions.kotlin_satlib}")
}

Library usage

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.")
}

Native libs

In order to use wrappers for native SAT solvers (e.g., MiniSatSolver), you need two native libraries:

1. Shared library for SAT solver (e.g., libminisat.so).

2. 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 osx64 subfolder.

• On Windows, use win64 subfolder.

💡	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 using LD_LIBRARY_PATH.

• On macOS, you can set DYLD_LIBRARY_PATH environment variable with path to your .dylib files.

• 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, inside C:/Windows.

Manual build

If you want to compile everything yourself, consult build instructions and CI workflow.

Prebuilt libs

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:

build.gradle.kts

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)