From 09c898ff0b998438d4f6e5c7dba384e1d04339ee Mon Sep 17 00:00:00 2001 From: elteammate Date: Tue, 5 Sep 2023 22:05:12 +0300 Subject: [PATCH 1/4] Fix assignment with incremental addition of unit clauses with eliminated variable --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 2 ++ .../src/commonMain/kotlin/org/kosat/ReconstructionStack.kt | 4 +++- 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 3aba215..abbabd5 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/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() } diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/ReconstructionStack.kt b/kosat-core/src/commonMain/kotlin/org/kosat/ReconstructionStack.kt index 34709bb..0e18dad 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/ReconstructionStack.kt +++ b/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 + } } } From f0a543255a04afb9728f6a695b220040ea422bb0 Mon Sep 17 00:00:00 2001 From: elteammate Date: Wed, 6 Sep 2023 23:17:52 +0300 Subject: [PATCH 2/4] Implement public API --- README.md | 10 +- docs/interface.md | 14 +-- kosat-api/build.gradle.kts | 29 ++++++ kosat-api/src/commonMain/kotlin/Kosat.kt | 99 +++++++++++++++++++ .../src/commonTest/kotlin/KotlinApiTest.kt | 72 ++++++++++++++ .../src/commonMain/kotlin/org/kosat/Clause.kt | 2 +- settings.gradle.kts | 1 + 7 files changed, 215 insertions(+), 12 deletions(-) create mode 100644 kosat-api/build.gradle.kts create mode 100644 kosat-api/src/commonMain/kotlin/Kosat.kt create mode 100644 kosat-api/src/commonTest/kotlin/KotlinApiTest.kt diff --git a/README.md b/README.md index c88be20..418451a 100644 --- a/README.md +++ b/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() diff --git a/docs/interface.md b/docs/interface.md index 1828c1d..3c1425c 100644 --- a/docs/interface.md +++ b/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)` +- `newClause(literals: List)` Solve CNF without assumptions: - `solve(): Boolean` Solve CNF with the passed assumptions: -- `solve(assumptions: List): Boolean` +- `solve(assumptions: List): 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` +- `fun getModel(): List` **Note:** the solver should be in the SAT state. diff --git a/kosat-api/build.gradle.kts b/kosat-api/build.gradle.kts new file mode 100644 index 0000000..7e0d82e --- /dev/null +++ b/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")) + } + } + } +} diff --git a/kosat-api/src/commonMain/kotlin/Kosat.kt b/kosat-api/src/commonMain/kotlin/Kosat.kt new file mode 100644 index 0000000..1a278eb --- /dev/null +++ b/kosat-api/src/commonMain/kotlin/Kosat.kt @@ -0,0 +1,99 @@ +import org.kosat.CDCL +import org.kosat.Clause +import org.kosat.Lit +import org.kosat.SolveResult +import kotlin.math.abs + +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? = null + + private fun invalidateResult() { + result = null + model = null + } + + private fun checkLiterals(literals: Iterable) { + 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})" + ) + } + } + } + } + + fun reset() { + numberOfVariables = 0 + numberOfClauses = 0 + solver = CDCL() + invalidateResult() + } + + fun newVariable() { + invalidateResult() + numberOfVariables++ + solver.newVariable() + } + + fun newClause(clause: Iterable) { + checkLiterals(clause) + invalidateResult() + numberOfClauses++ + solver.newClause(Clause.fromDimacs(clause)) + } + + fun newClause(vararg literals: Int) { + newClause(literals.asIterable()) + } + + fun solve(vararg assumptions: Int): Boolean { + return solve(assumptions.asIterable()) + } + + fun solve(assumptions: Iterable): Boolean { + checkLiterals(assumptions) + result = solver.solve(assumptions.map { Lit.fromDimacs(it) }) + return result == SolveResult.SAT + } + + fun getModel(): List { + 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 } + } + + 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) + } +} diff --git a/kosat-api/src/commonTest/kotlin/KotlinApiTest.kt b/kosat-api/src/commonTest/kotlin/KotlinApiTest.kt new file mode 100644 index 0000000..d53e2a2 --- /dev/null +++ b/kosat-api/src/commonTest/kotlin/KotlinApiTest.kt @@ -0,0 +1,72 @@ +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() } + } + + @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()) + } +} diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt index f57c973..6c26d78 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt @@ -19,7 +19,7 @@ data class Clause( } companion object { - fun fromDimacs(dimacsLits: List): Clause { + fun fromDimacs(dimacsLits: Iterable): Clause { val lits = LitVec(dimacsLits.map { Lit.fromDimacs(it) }) return Clause(lits) } diff --git a/settings.gradle.kts b/settings.gradle.kts index db3cf86..34b8a58 100644 --- a/settings.gradle.kts +++ b/settings.gradle.kts @@ -19,3 +19,4 @@ fun myInclude(name: String) { myInclude("core") myInclude("cli") myInclude("web") +myInclude("api") From 36dd1e40c06b0f8af6a792e6d5db2cce5d3093a2 Mon Sep 17 00:00:00 2001 From: elteammate Date: Wed, 6 Sep 2023 23:22:16 +0300 Subject: [PATCH 3/4] Improve test --- kosat-api/src/commonMain/kotlin/Kosat.kt | 8 ++++++++ kosat-api/src/commonTest/kotlin/KotlinApiTest.kt | 14 ++++++++++++++ 2 files changed, 22 insertions(+) diff --git a/kosat-api/src/commonMain/kotlin/Kosat.kt b/kosat-api/src/commonMain/kotlin/Kosat.kt index 1a278eb..6a47fb2 100644 --- a/kosat-api/src/commonMain/kotlin/Kosat.kt +++ b/kosat-api/src/commonMain/kotlin/Kosat.kt @@ -96,4 +96,12 @@ class Kosat { return model!![varIndex] xor (literal < 0) } + + fun numberOfVariables(): Int { + return numberOfVariables + } + + fun numberOfClauses(): Int { + return numberOfClauses + } } diff --git a/kosat-api/src/commonTest/kotlin/KotlinApiTest.kt b/kosat-api/src/commonTest/kotlin/KotlinApiTest.kt index d53e2a2..5dea37c 100644 --- a/kosat-api/src/commonTest/kotlin/KotlinApiTest.kt +++ b/kosat-api/src/commonTest/kotlin/KotlinApiTest.kt @@ -44,6 +44,20 @@ class KotlinApiTest { 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 From 56e00025f545cc683fdbc95e0c7b411810cd32ae Mon Sep 17 00:00:00 2001 From: elteammate Date: Wed, 6 Sep 2023 23:27:00 +0300 Subject: [PATCH 4/4] Doc comments --- kosat-api/src/commonMain/kotlin/Kosat.kt | 65 +++++++++++++++++++++--- 1 file changed, 57 insertions(+), 8 deletions(-) diff --git a/kosat-api/src/commonMain/kotlin/Kosat.kt b/kosat-api/src/commonMain/kotlin/Kosat.kt index 6a47fb2..a8b0147 100644 --- a/kosat-api/src/commonMain/kotlin/Kosat.kt +++ b/kosat-api/src/commonMain/kotlin/Kosat.kt @@ -4,6 +4,14 @@ 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 @@ -33,6 +41,10 @@ class Kosat { } } + /** + * Resets the solver to its initial state, removing all variables and + * clauses. + */ fun reset() { numberOfVariables = 0 numberOfClauses = 0 @@ -40,12 +52,35 @@ class Kosat { 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) { checkLiterals(clause) invalidateResult() @@ -53,20 +88,38 @@ class Kosat { 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): 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 { if (result == null) { throw IllegalStateException("Model is not available before solving") @@ -77,6 +130,10 @@ class Kosat { 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") @@ -96,12 +153,4 @@ class Kosat { return model!![varIndex] xor (literal < 0) } - - fun numberOfVariables(): Int { - return numberOfVariables - } - - fun numberOfClauses(): Int { - return numberOfClauses - } }