Public Interface

README.md

@@ -30,18 +30,18 @@ repositories {
 }
 
 dependencies {
-    implementation("com.github.UnitTestBot.kosat:core:$version")
+    implementation("com.github.UnitTestBot.kosat:api:$version")
 }
 ```
 
 #### Usage example: Kotlin
 
 ```kotlin
-import org.kosat.CDCL
+import org.kosat.Kosat
 
 fun main() {
     // Create the instance of KoSAT solver:
-    val solver = CDCL()
+    val solver = Kosat()
 
     // Allocate two variables:
     solver.newVariable()
@@ -54,8 +54,8 @@ fun main() {
     // solver.newClause(1, -2) // UNSAT with this clause
 
     // Solve the SAT problem:
-    val result = solver.solve()
-    println("result = $result") // SAT
+    val result = solver.solve() // true (SAT)
+    println("result = $result")
 
     // Get the model:
     val model = solver.getModel()

docs/interface.md

@@ -1,23 +1,25 @@
 ## Solver's interface functions
 
-Add a variable to CNF and return its number:
-- `addVariable(): Int`
+All variables are numbered in DIMACS format.
+
+Add a variable to CNF:
+- `newVariable()`
 
 Add a clause to CNF as pure literals or list of literals:
-- `addClause(literals: List<Lit>)`
+- `newClause(literals: List<Int>)`
 
 Solve CNF without assumptions:
 - `solve(): Boolean`
 
 Solve CNF with the passed assumptions:
-- `solve(assumptions: List<Lit>): Boolean`
+- `solve(assumptions: List<Int>): Boolean`
 
 Query boolean value of a literal:
-- `getValue(lit: Lit): Boolean`
+- `value(lit: Int): Boolean`
 
 **Note:** the solver should be in the SAT state.
 
 Query the satisfying assignment (model) for the SAT problem:
-- `fun getModel(): List<Lit>`
+- `fun getModel(): List<Int>`
 
 **Note:** the solver should be in the SAT state.

kosat-api/build.gradle.kts

@@ -0,0 +1,29 @@
+import org.gradle.api.tasks.testing.logging.TestExceptionFormat
+import org.gradle.api.tasks.testing.logging.TestLogEvent
+import org.jetbrains.dokka.DokkaConfiguration
+import org.jetbrains.dokka.model.KotlinVisibility
+
+plugins {
+    kotlin("multiplatform")
+}
+
+kotlin {
+    jvm()
+    js {
+        browser()
+    }
+
+    sourceSets {
+        commonMain {
+            dependencies {
+                implementation(project(":core"))
+            }
+        }
+
+        commonTest {
+            dependencies {
+                implementation(kotlin("test"))
+            }
+        }
+    }
+}

kosat-api/src/commonMain/kotlin/Kosat.kt

@@ -0,0 +1,156 @@
+import org.kosat.CDCL
+import org.kosat.Clause
+import org.kosat.Lit
+import org.kosat.SolveResult
+import kotlin.math.abs
+
+/**
+ * Wrapper for the KoSAT solver.
+ *
+ * All the literals and variables are in DIMACS format (positive for variables,
+ * negative for negated variables, 1-based indexing).
+ *
+ * *This class is not thread-safe.*
+ */
+class Kosat {
+    private var numberOfVariables: Int = 0
+    private var numberOfClauses: Int = 0
+
+    private var solver: CDCL = CDCL()
+
+    private var result: SolveResult? = null
+    private var model: List<Boolean>? = null
+
+    private fun invalidateResult() {
+        result = null
+        model = null
+    }
+
+    private fun checkLiterals(literals: Iterable<Int>) {
+        for (lit in literals) {
+            if (lit == 0) {
+                throw IllegalArgumentException("Clause must not contain 0")
+            } else {
+                val varIndex = abs(lit) - 1
+                if (varIndex >= numberOfVariables) {
+                    throw IllegalArgumentException(
+                        "Variable of $lit is not defined (total variables: ${numberOfVariables})"
+                    )
+                }
+            }
+        }
+    }
+
+    /**
+     * Resets the solver to its initial state, removing all variables and
+     * clauses.
+     */
+    fun reset() {
+        numberOfVariables = 0
+        numberOfClauses = 0
+        solver = CDCL()
+        invalidateResult()
+    }
+
+    /**
+     * Return the number of variables in the solver.
+     */
+    fun numberOfVariables(): Int {
+        return numberOfVariables
+    }
+
+    /**
+     * Return the number of clauses in the solver.
+     */
+    fun numberOfClauses(): Int {
+        return numberOfClauses
+    }
+
+    /**
+     * Allocate a new variable in the solver.
+     */
+    fun newVariable() {
+        invalidateResult()
+        numberOfVariables++
+        solver.newVariable()
+    }
+
+    /**
+     * Add a new clause to the solver. The literals must be in DIMACS format
+     * (positive for variables, negative for negated variables, 1-based
+     * indexing). All variables must be defined with [newVariable] before adding
+     * clauses.
+     */
+    fun newClause(clause: Iterable<Int>) {
+        checkLiterals(clause)
+        invalidateResult()
+        numberOfClauses++
+        solver.newClause(Clause.fromDimacs(clause))
+    }
+
+    /**
+     * Add a new clause to the solver. The literals must be in DIMACS format
+     * (positive for variables, negative for negated variables, 1-based
+     * indexing). All variables must be defined with [newVariable] before adding
+     * clauses.
+     */
+    fun newClause(vararg literals: Int) {
+        newClause(literals.asIterable())
+    }
+
+    /**
+     * Solve the SAT problem with the given assumptions, if any. Assumptions are
+     * literals in DIMACS format.
+     */
+    fun solve(vararg assumptions: Int): Boolean {
+        return solve(assumptions.asIterable())
+    }
+
+    /**
+     * Solve the SAT problem with the given assumptions
+     */
+    fun solve(assumptions: Iterable<Int>): Boolean {
+        checkLiterals(assumptions)
+        result = solver.solve(assumptions.map { Lit.fromDimacs(it) })
+        return result == SolveResult.SAT
+    }
+
+    /**
+     * If the problem is SAT, return the model as a list of booleans. [solve]
+     * must be called before calling this method. The model is cached after the
+     * first call and reset when clause or variable is incrementally is added.
+     */
+    fun getModel(): List<Boolean> {
+        if (result == null) {
+            throw IllegalStateException("Model is not available before solving")
+        } else if (result != SolveResult.SAT) {
+            throw IllegalStateException("Model is not available if result is not SAT")
+        }
+
+        return solver.getModel().also { model = it }
+    }
+
+    /**
+     * If the problem is SAT, return the value of the given literal in the
+     * model. [solve] must be called before calling this method.
+     */
+    fun value(literal: Int): Boolean {
+        if (literal == 0) {
+            throw IllegalArgumentException("Literal must not be 0")
+        }
+
+        val varIndex = abs(literal) - 1
+
+        if (varIndex >= numberOfVariables) {
+            throw IllegalArgumentException(
+                "Variable of $literal is not defined (total variables: ${numberOfVariables})"
+            )
+        }
+
+        if (model == null) {
+            model = getModel()
+        }
+
+        return model!![varIndex] xor (literal < 0)
+    }
+}

kosat-api/src/commonTest/kotlin/KotlinApiTest.kt

@@ -0,0 +1,86 @@
+import kotlin.test.Test
+import kotlin.test.assertEquals
+import kotlin.test.assertFailsWith
+import kotlin.test.assertFalse
+import kotlin.test.assertTrue
+
+class KotlinApiTest {
+    @Test
+    fun tieShirtVarargs() {
+        val solver = Kosat()
+
+        assertFailsWith(IllegalArgumentException::class) { solver.newClause(1, 2) }
+
+        solver.newVariable()
+        solver.newVariable()
+
+        solver.newClause(-1, 2)
+        solver.newClause(1, 2)
+        solver.newClause(-1, -2)
+
+        assertFailsWith(IllegalStateException::class) { solver.getModel() }
+        assertFailsWith(IllegalStateException::class) { solver.value(1) }
+        assertFailsWith(IllegalArgumentException::class) { solver.value(0) }
+        assertFailsWith(IllegalArgumentException::class) { solver.value(-5) }
+
+        assertTrue(solver.solve())
+
+        assertFalse(solver.value(1))
+        assertTrue(solver.value(-1))
+        assertTrue(solver.value(2))
+        assertFalse(solver.value(-2))
+
+        assertFailsWith(IllegalArgumentException::class) { solver.value(0) }
+        assertFailsWith(IllegalArgumentException::class) { solver.value(-5) }
+
+        assertEquals(listOf(false, true), solver.getModel())
+
+        assertTrue(solver.solve(-1))
+        assertFalse(solver.solve(1))
+        assertTrue(solver.solve(-1, 2))
+        assertFalse(solver.solve(-1, -2))
+
+        solver.newClause(1, -2)
+        assertFalse(solver.solve())
+
+        assertFailsWith(IllegalStateException::class) { solver.getModel() }
+
+        solver.reset()
+
+        assertFailsWith(IllegalStateException::class) { solver.getModel() }
+
+        solver.newVariable()
+        solver.newVariable()
+        solver.newVariable()
+
+        assertTrue(solver.solve())
+
+        assertEquals(3, solver.numberOfVariables())
+        assertEquals(0, solver.numberOfClauses())
+        assertEquals(3, solver.getModel().size)
+    }
+
+    @Test
+    fun tieShirtIterables() {
+        val solver = Kosat()
+
+        solver.newVariable()
+        solver.newVariable()
+
+        solver.newClause(listOf(-1, 2))
+        solver.newClause(setOf(1, 2))
+        solver.newClause(listOf(-1, -2))
+
+        assertTrue(solver.solve())
+
+        assertEquals(listOf(false, true), solver.getModel())
+
+        assertTrue(solver.solve(setOf(-1)))
+        assertFalse(solver.solve(listOf(1)))
+        assertTrue(solver.solve(listOf(-1, 2)))
+        assertFalse(solver.solve(setOf(-1, -2)))
+
+        solver.newClause(listOf(1, -2))
+        assertFalse(solver.solve())
+    }
+}

kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt

@@ -238,6 +238,8 @@ class CDCL {
         for (assumption in this.assumptions) assignment.freeze(assumption)
         newClauses.clear()
 
+        if (!ok) return finishWithUnsat()
+
         // Check for an immediate level 0 conflict
         propagate()?.let { return finishWithUnsat() }
 

kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt

@@ -19,7 +19,7 @@ data class Clause(
     }
 
     companion object {
-        fun fromDimacs(dimacsLits: List<Int>): Clause {
+        fun fromDimacs(dimacsLits: Iterable<Int>): Clause {
             val lits = LitVec(dimacsLits.map { Lit.fromDimacs(it) })
             return Clause(lits)
         }

kosat-core/src/commonMain/kotlin/org/kosat/ReconstructionStack.kt

@@ -181,7 +181,9 @@ class ReconstructionStack {
             if (clause.size > 1) {
                 solver.attachClause(Clause(clause))
             } else {
-                check(solver.assignment.enqueue(clause[0], null))
+                if (!solver.assignment.enqueue(clause[0], null)) {
+                    solver.ok = false
+                }
             }
         }
 

settings.gradle.kts

@@ -19,3 +19,4 @@ fun myInclude(name: String) {
 myInclude("core")
 myInclude("cli")
 myInclude("web")
+myInclude("api")