Updated Kosat, now you can only specify clauses

Author: korifey

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

@@ -16,6 +16,8 @@ fun solveCnf(cnf: CnfRequest): List<Int>? {
     return CDCL(clauses.map { Clause(it) }.toMutableList(), cnf.vars).solve()
 }
 
+fun solveCnf(clauses: List<List<Lit>>): List<Int> = Kosat(clauses, 0).apply { solve() }.getModel()
+
 enum class SolverType {
     INCREMENTAL, NON_INCREMENTAL;
 }
@@ -34,6 +36,7 @@ class CDCL(private val solverType: SolverType = SolverType.INCREMENTAL) {
     val learnts = mutableListOf<Clause>()
 
     var numberOfVariables: Int = 0
+        private set
 
     // for each variable contains current assignment, clause it came from and decision level when it happened
     val vars: MutableList<VarState> = MutableList(numberOfVariables) { VarState(VarValue.UNDEFINED, null, -1) }
@@ -79,7 +82,9 @@ class CDCL(private val solverType: SolverType = SolverType.INCREMENTAL) {
 
     // get value of literal
     fun getValue(lit: Lit): VarValue {
-        if (vars[variable(lit)].value == VarValue.UNDEFINED) return VarValue.UNDEFINED
+        if (vars[variable(lit)].value == VarValue.UNDEFINED)
+            return VarValue.UNDEFINED
+
         return if (lit % 2 == 1)
                 !vars[variable(lit)].value
             else
@@ -144,7 +149,7 @@ class CDCL(private val solverType: SolverType = SolverType.INCREMENTAL) {
 
         // add not mentioned variables from new clause
         val maxVar = clause.maxOfOrNull { variable(it) } ?: 0
-        while (numberOfVariables < maxVar) {
+        while (numberOfVariables <= maxVar) {
             addVariable()
         }
 

src/commonMain/kotlin/org/kosat/DPLL.kt

@@ -5,6 +5,7 @@ import kotlinx.collections.immutable.persistentListOf
 import kotlin.math.abs
 
 // DPLL
+@Deprecated("use solveCnf instead", replaceWith = ReplaceWith("solveCnf(clauses)"))
 fun solveCnfDPLL(cnf: CnfRequest): List<Int>? {
     val clauses = ArrayList(cnf.clauses.map { ArrayList(it.lits.toList()) })
     return dpll(clauses)?.sortedBy { abs(it) }

src/commonMain/kotlin/org/kosat/Kosat.kt

@@ -59,12 +59,12 @@ interface Solver {
     fun getModel(): List<Lit>
 }
 
-class Kosat(clauses: MutableList<MutableList<Lit>>, vars: Int = 0) : Solver {
+class Kosat(clauses: List<List<Lit>>, vars: Int = 0) : Solver {
     override val numberOfVariables get() = solver.numberOfVariables
     override val numberOfClauses get() = solver.constraints.size + solver.learnts.size
 
     private var model: List<Lit>? = null
-    private val solver = CDCL(clauses.map { Clause(it) }.toMutableList(), vars)
+    private val solver = CDCL(clauses.map { Clause(it.toMutableList()) }.toMutableList(), vars)
 
     override fun addVariable(): Int {
         solver.addVariable()
@@ -98,3 +98,4 @@ class Kosat(clauses: MutableList<MutableList<Lit>>, vars: Int = 0) : Solver {
         return model?.get(abs(lit) - 1) == lit
     }
 }
+

src/jvmTest/kotlin/TestSolver.kt

@@ -0,0 +1,28 @@
+import org.junit.jupiter.api.Test
+import org.junit.jupiter.api.TestInstance
+import org.kosat.Kosat
+import org.kosat.solveCnf
+
+@TestInstance(TestInstance.Lifecycle.PER_CLASS)
+internal class TestSolver {
+    @Test
+    fun `test example 1`() {
+
+        val solver = Kosat(listOf(
+            listOf(1, 2, -3), listOf(-1), listOf(-3)
+        ))
+
+        println(solver.solve())
+        println(solver.getModel().toString())
+    }
+
+    @Test
+    fun `test example 2`() {
+
+        val solution = solveCnf(listOf(
+            listOf(1, 2, -3, -4), listOf(-1), listOf(-3), listOf(3, -4)
+        ))
+
+        println(solution)
+    }
+}