Improvements of CDCL public interface

README.md

@@ -43,10 +43,6 @@ fun main() {
     // Create the instance of KoSAT solver:
     val solver = CDCL()
 
-    // Allocate two variables:
-    solver.newVariable()
-    solver.newVariable()
-
     // Encode the TIE-SHIRT problem:
     solver.newClause(-1, 2)
     solver.newClause(1, 2)

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

@@ -115,8 +115,11 @@ class CDCL {
      *
      * The [newClause] technically adds variables automatically,
      * but sometimes not all variables have to be mentioned in the clauses.
+     *
+     * Returns 1-based index of the new variable, or, equivalently, number of
+     * variables in the solver after the call.
      */
-    fun newVariable() {
+    fun newVariable(): Int {
         // Watch
         watchers.add(ClauseVec())
         watchers.add(ClauseVec())
@@ -126,6 +129,8 @@ class CDCL {
 
         // Phase saving heuristics
         polarity.add(LBool.UNDEF)
+
+        return assignment.numberOfVariables
     }
 
     /**
@@ -138,6 +143,9 @@ class CDCL {
         return assignment.value(lit)
     }
 
+    /**
+     * Adds a new clause to the solver with the given literals in DIMACS format.
+     */
     fun newClause(vararg lits: Int) {
         newClause(Clause(LitVec(lits.map { Lit.fromDimacs(it) })))
     }
@@ -212,6 +220,21 @@ class CDCL {
      */
     private var assumptions: LitVec = LitVec()
 
+    /**
+     * Solves the CNF problem using the CDCL algorithm.
+     */
+    // Overload for Java
+    fun solve(): SolveResult {
+        return solve(emptyList())
+    }
+
+    /**
+     * Solves the CNF problem using the CDCL algorithm.
+     */
+    fun solve(vararg assumptions: Int): SolveResult {
+        return solve(assumptions.map { Lit.fromDimacs(it) })
+    }
+
     /**
      * Solves the CNF problem using the CDCL algorithm.
      *

kosat-core/src/jvmTest/kotlin/org/kosat/Example.kt

@@ -0,0 +1,29 @@
+package org.kosat
+
+import org.junit.jupiter.api.Assertions
+import kotlin.test.Test
+
+internal class Example {
+    @Test
+    fun testExample() {
+        // Create the instance of KoSAT solver:
+        val solver = CDCL()
+
+        // Encode the TIE-SHIRT problem:
+        solver.newClause(-1, 2)
+        solver.newClause(1, 2)
+        solver.newClause(-1, -2)
+        // solver.newClause(1, -2) // UNSAT with this clause
+
+        // Solve the SAT problem:
+        val result = solver.solve()
+        println("result = $result") // SAT
+
+        // Get the model:
+        val model = solver.getModel()
+        println("model = $model") // [false, true]
+
+        Assertions.assertEquals(SolveResult.SAT, result)
+        Assertions.assertEquals(listOf(false, true), model)
+    }
+}