From 733d9f648774c0c557a75b3d4201aa07a3526c3b Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Mon, 24 Jul 2023 11:06:13 +0300 Subject: [PATCH 01/22] Store substitution for variables for ELS --- kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index 399086c5..5045f427 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -9,6 +9,9 @@ data class VarState( /** Index of the variable in the trail */ var trailIndex: Int = -1, + + /** A literal which is used to substitute this variable after Equivalent Literal Substitution */ + var substitution: Lit? = null, ) class Assignment(private val solver: CDCL) { From 22f25426a7c342e412a0c74b16d35d9d347f45ef Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Mon, 24 Jul 2023 11:53:37 +0300 Subject: [PATCH 02/22] Use xor to find not-equal literal instead of ifs --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 12 +++--------- kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt | 4 ++++ .../src/commonMain/kotlin/org/kosat/SolverTypes.kt | 5 +++++ 3 files changed, 12 insertions(+), 9 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 8995d3d1..5d1a3c24 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -665,11 +665,7 @@ class CDCL { if (clause.deleted) continue if (clause.size != 2) continue - val other = if (clause[0].variable == lit.variable) { - clause[1] - } else { - clause[0] - } + val other = clause.otherWatch(lit.neg) when (value(other)) { // if the other literal is true, the @@ -772,13 +768,11 @@ class CDCL { if (assignment.trailIndex(lcaVar) > assignment.trailIndex(litVar)) { check(assignment.reason(lcaVar)!!.size == 2) val (a, b) = assignment.reason(lcaVar)!!.lits - // TODO: this can be done with xor, - // will fix after merging feature/assignment - lca = if (a == lca) b.neg else a.neg + lca = lca.differentAmong2(a, b).neg } else { check(assignment.reason(litVar)!!.size == 2) val (a, b) = assignment.reason(litVar)!!.lits - lit = if (a == lit) b.neg else a.neg + lit = lit.differentAmong2(a, b).neg } } } diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt index 8fcbc454..c6d67cf7 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt @@ -21,6 +21,10 @@ data class Clause( return lits.map { it.toDimacs() } } + fun otherWatch(lit: Lit): Lit { + return lit.differentAmong2(lits[0], lits[1]) + } + companion object { fun fromDimacs(clause: List): Clause { val lits = clause.map { Lit.fromDimacs(it) }.toMutableList() diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt b/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt index 87adc8ac..9b4e741c 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt @@ -64,6 +64,11 @@ value class Lit(val inner: Int) { return if (isPos) v else -v } + fun differentAmong2(lit1: Lit, lit2: Lit): Lit { + check(this == lit1 || this == lit2) + return Lit(inner xor lit1.inner xor lit2.inner) + } + companion object { fun fromDimacs(lit: Int): Lit { val v = abs(lit) - 1 // 0-based variables index From ee965428a15cde19a764692f75dd8c624a4f0999 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Mon, 24 Jul 2023 15:46:22 +0300 Subject: [PATCH 03/22] Potential ELS implementation --- .../commonMain/kotlin/org/kosat/Assignment.kt | 25 +++ .../src/commonMain/kotlin/org/kosat/CDCL.kt | 197 +++++++++++++++--- .../kotlin/org/kosat/SolverTypes.kt | 4 + .../kotlin/org/kosat/VariableSelector.kt | 6 +- .../src/commonMain/kotlin/org/kosat/util.kt | 4 + .../jvmTest/kotlin/org/kosat/ManualTest.kt | 7 +- 6 files changed, 206 insertions(+), 37 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index 5045f427..fe7fb6be 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -18,6 +18,9 @@ class Assignment(private val solver: CDCL) { val value: MutableList = mutableListOf() val varData: MutableList = mutableListOf() val trail: MutableList = mutableListOf() + val numberOfVariables get() = value.size + private var numberOfSubstitutions = 0 + val numberOfActiveVariables get() = numberOfVariables - numberOfSubstitutions var decisionLevel: Int = 0 var qhead: Int = 0 @@ -31,6 +34,28 @@ class Assignment(private val solver: CDCL) { return value[lit.variable] xor lit.isNeg } + fun valueAfterSubstitution(v: Var): LBool { + val substitution = varData[v].substitution + return if (substitution != null) { + value(substitution) + } else { + value(v) + } + } + + fun valueAfterSubstitution(lit: Lit): LBool { + return valueAfterSubstitution(lit.variable) xor lit.isNeg + } + + fun markSubstituted(variable: Var, substitution: Lit) { + check(varData[variable].substitution == null) + varData[variable].substitution = substitution + } + + fun fixNestedSubstitutions() { + + } + // fun assign(v: Var, value: LBool) { // value[v] = value // } diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 5d1a3c24..7610a609 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -1,6 +1,7 @@ package org.kosat import org.kosat.cnf.CNF +import kotlin.math.min /** * Solves [cnf] and returns @@ -54,12 +55,6 @@ class CDCL { */ val watchers: MutableList> = mutableListOf() - /** - * The number of variables. - */ - var numberOfVariables: Int = 0 - private set - /** * The maximum amount of probes expected to be returned * by [generateProbes]. @@ -71,7 +66,7 @@ class CDCL { /** * The branching heuristic, used to choose the next decision variable. */ - private val variableSelector: VariableSelector = VSIDS(numberOfVariables) + private val variableSelector: VariableSelector = VSIDS(assignment.numberOfVariables) /** * The restart strategy, used to decide when to restart the search. @@ -95,12 +90,12 @@ class CDCL { initialClauses: Iterable, initialVarsNumber: Int = 0, ) { - while (numberOfVariables < initialVarsNumber) { + while (assignment.numberOfVariables < initialVarsNumber) { newVariable() } initialClauses.forEach { newClause(it) } - polarity = MutableList(numberOfVariables + 1) { LBool.UNDEF } + polarity = MutableList(assignment.numberOfVariables) { LBool.UNDEF } } constructor(cnf: CNF) : this(cnf.clauses.map { Clause.fromDimacs(it) }, cnf.numVars) @@ -111,9 +106,7 @@ class CDCL { * The [newClause] technically adds variables automatically, * but sometimes not all variables have to be mentioned in the clauses. */ - fun newVariable(): Int { - numberOfVariables++ - + fun newVariable() { // Watch watchers.add(mutableListOf()) watchers.add(mutableListOf()) @@ -126,8 +119,6 @@ class CDCL { // Phase saving heuristics polarity.add(LBool.UNDEF) - - return numberOfVariables } fun value(lit: Lit): LBool { @@ -145,7 +136,7 @@ class CDCL { // Add not mentioned variables from the new clause val maxVar = clause.lits.maxOfOrNull { it.variable.index } ?: 0 - while (numberOfVariables < maxVar) { + while (assignment.numberOfVariables < maxVar) { newVariable() } @@ -232,7 +223,9 @@ class CDCL { * [SolveResult.SAT], [SolveResult.UNSAT], or [SolveResult.UNKNOWN]. */ fun solve(currentAssumptions: List = emptyList()): SolveResult { - assumptions = currentAssumptions.toMutableList() + assumptions = currentAssumptions.map { + assignment.varData[it.variable].substitution?.xor(it.isNeg) ?: it + }.toMutableList() // If given clauses are already cause UNSAT, no need to do anything if (!ok) return finishWithUnsat() @@ -245,10 +238,6 @@ class CDCL { if (assignment.decisionLevel > 0) backtrack(0) cachedModel = null - // If the problem is trivially SAT, simply return the result - // (and check for assumption satisfiability) - if (db.clauses.isEmpty()) return finishWithSatIfAssumptionsOk() - // Check for an immediate level 0 conflict propagate()?.let { return finishWithUnsat() } @@ -275,7 +264,7 @@ class CDCL { // Check if all variables are assigned, indicating satisfiability, // (unless assumptions are falsified) - if (assignment.trail.size == numberOfVariables) { + if (assignment.trail.size == assignment.numberOfActiveVariables) { return finishWithSatIfAssumptionsOk() } @@ -414,16 +403,17 @@ class CDCL { fun getModel(): List { if (cachedModel != null) return cachedModel!! - cachedModel = assignment.value.map { - when (it) { - LBool.TRUE, LBool.UNDEF -> true - LBool.FALSE -> false - } - }.toMutableList() + cachedModel = mutableListOf() for (assumption in assumptions) { - check(value(assumption) != LBool.FALSE) - cachedModel!![assumption.variable] = assumption.isPos + check(assignment.value(assumption) == LBool.TRUE) + } + + for (varIndex in 0 until assignment.numberOfVariables) { + cachedModel!!.add(when (assignment.valueAfterSubstitution(Var(varIndex))) { + LBool.TRUE, LBool.UNDEF -> true + LBool.FALSE -> false + }) } return cachedModel!! @@ -442,13 +432,20 @@ class CDCL { require(assignment.qhead == assignment.trail.size) dratBuilder.addComment("Preprocessing") + + dratBuilder.addComment("Preprocessing: Equivalent literal substitution") + + for (i in 1..10) { + equivalentLiteralSubstitution()?.let { return it } + } + dratBuilder.addComment("Preprocessing: Failed literal probing") failedLiteralProbing()?.let { return it } // Without this, we might let the solver propagate nothing // and make a decision after all values are set. - if (assignment.trail.size == numberOfVariables) { + if (assignment.trail.size == assignment.numberOfVariables) { return finishWithSatIfAssumptionsOk() } @@ -466,6 +463,144 @@ class CDCL { return null } + private fun impliedLiterals(lit: Lit): List { + check(value(lit) == LBool.UNDEF) + val implied = mutableListOf() + + for (watched in watchers[lit.neg]) { + if (watched.deleted) continue + if (watched.size != 2) continue + + val other = watched.otherWatch(lit.neg) + + check(value(other) != LBool.FALSE) + if (value(other) != LBool.UNDEF) continue + implied.add(other) + } + + return implied + } + + private fun equivalentLiteralSubstitution(): SolveResult? { + check(assignment.decisionLevel == 0) + + db.simplify() + + val marks = MutableList(assignment.numberOfVariables * 2) { 0 } + val num = MutableList(assignment.numberOfVariables * 2) { 0 } + val stack = mutableListOf() + var counter = 0 + + fun dfs(v: Lit): Int? { + check(value(v) == LBool.UNDEF) + check(marks[v] == 0) + + marks[v] = 1 + stack.add(v) + + counter++ + num[v] = counter + var lowest = counter + + for (u in impliedLiterals(v)) { + if (marks[u] == 0) { + val otherLowest = dfs(u) ?: return null + lowest = min(otherLowest, lowest) + } else if (marks[u] != 4) { + lowest = min(lowest, num[u]) + } + } + + marks[v] = 2 + + if (lowest == num[v]) { + val scc = mutableListOf() + while (true) { + val u = stack.removeLast() + marks[u] = 3 + scc.add(u) + if (u == v) { + for (w in scc) { + if (marks[w.neg] == 3) { + dratBuilder.addComment("Found UNSAT due to complement literals being in the same SCC") + dratBuilder.addClause(Clause(mutableListOf(w))) + dratBuilder.addClause(Clause(mutableListOf(w.neg))) + return null + } + marks[w] = 4 + } + break + } + assignment.varData[u.variable].substitution = v xor u.isNeg + } + } + + return lowest + } + + for (varIndex in 0 until assignment.numberOfVariables) { + val variable = Var(varIndex) + val lit = variable.posLit + + if ( + assignment.varData[variable].substitution != null || + (marks[lit] != 0 || marks[lit.neg] != 0) || + value(lit) != LBool.UNDEF + ) continue + + check(marks[lit] == 0) + dfs(lit) ?: return finishWithUnsat() + } + + for (varIndex in 0 until assignment.numberOfVariables) { + val variable = Var(varIndex) + val substitution = assignment.varData[variable].substitution ?: continue + val secondSubstitution = assignment.varData[substitution.variable].substitution ?: continue + assignment.varData[variable].substitution = secondSubstitution xor substitution.isNeg + } + + for (clause in db.clauses + db.learnts) { + if (clause.deleted) continue + + val willChange = clause.lits.any { assignment.varData[it.variable].substitution != null } + if (!willChange) continue + + val newLits = clause.lits.map { + assignment.varData[it.variable].substitution?.xor(it.isNeg) ?: it + }.toMutableList() + + val useless = sortDedupAndCheckComplimentary(newLits) + + if (!useless) { + val newClause = Clause(newLits, clause.learnt) + if (newClause.size == 1 || !clause.learnt) dratBuilder.addClause(newClause) + if (newClause.size == 1) { + if (!assignment.enqueue(newClause[0], null)) { + return finishWithUnsat() + } + } else { + attachClause(newClause) + } + } + + markDeleted(clause) + } + + propagate()?.let { return finishWithUnsat() } + + assumptions = assumptions.map { + assignment.varData[it.variable].substitution?.xor(it.isNeg) ?: it + }.toMutableList() + + if (sortDedupAndCheckComplimentary(assumptions)) { + return finishWithAssumptionsUnsat() + } + + variableSelector.initAssumptions(assumptions) + + return null + } + /** * Literal probing is only useful if the probe can lead * lead to derivation of something by itself. We can @@ -913,7 +1048,7 @@ class CDCL { // Keep track of the variables we have "seen" during the analysis // (see implementation below for details) - val seen = BooleanArray(numberOfVariables) + val seen = BooleanArray(assignment.numberOfVariables) // The list of literals of the learnt val learntLits = mutableListOf() diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt b/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt index 9b4e741c..bf3f78ce 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt @@ -69,6 +69,10 @@ value class Lit(val inner: Int) { return Lit(inner xor lit1.inner xor lit2.inner) } + infix fun xor(b: Boolean): Lit { + return Lit(inner xor b.toInt()) + } + companion object { fun fromDimacs(lit: Int): Lit { val v = abs(lit) - 1 // 0-based variables index diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt b/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt index e606267f..331927ca 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt @@ -214,8 +214,10 @@ class VSIDS(private var numberOfVariables: Int = 0) : VariableSelector() { return null } // if there is undefined assumption pick it, other way pick best choice - return assumptions.firstOrNull { assignment.value(it) == LBool.UNDEF } - ?: getMaxActivityVariable(assignment).posLit + return assumptions.firstOrNull { + assignment.value(it) == LBool.UNDEF && + assignment.varData[it.variable].substitution == null + } ?: getMaxActivityVariable(assignment).posLit } override fun backTrack(variable: Var) { diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/util.kt b/kosat-core/src/commonMain/kotlin/org/kosat/util.kt index 862e1fec..247b2b6a 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/util.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/util.kt @@ -9,3 +9,7 @@ fun Double.round(decimals: Int): Double { repeat(decimals) { multiplier *= 10 } return kotlin.math.round(this * multiplier) / multiplier } + +fun Boolean.toInt(): Int { + return if (this) 1 else 0 +} diff --git a/kosat-core/src/jvmTest/kotlin/org/kosat/ManualTest.kt b/kosat-core/src/jvmTest/kotlin/org/kosat/ManualTest.kt index a3b1c287..a9bc534e 100644 --- a/kosat-core/src/jvmTest/kotlin/org/kosat/ManualTest.kt +++ b/kosat-core/src/jvmTest/kotlin/org/kosat/ManualTest.kt @@ -10,7 +10,7 @@ import kotlin.test.Test internal class ManualTest { @Test fun testManual() { - val path = "src/jvmTest/resources/testCover/cover/cover0033.cnf".toPath() + val path = "src/jvmTest/resources/testCover/cover/cover0025.cnf".toPath() val cnf = CNF.from(path) val clauses = cnf.clauses.map { lits -> Clause(lits.map { Lit.fromDimacs(it) }.toMutableList()) @@ -20,9 +20,8 @@ internal class ManualTest { val model = solver.solve() println("${solver.getModel()}") println("model = $model") - val model2 = solver.solve(listOf(Lit.fromDimacs(1))) - val model3 = solver.solve(listOf(Lit.fromDimacs(2), Lit.fromDimacs(-1))) + val model2 = solver.solve(listOf(Lit.fromDimacs(22))) println("model = $model2") - println("model = $model3") + // println("${solver.getModel()}") } } From dfe0224a72d7de5a06b1be94403c27d43aca9ca9 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Mon, 24 Jul 2023 16:18:19 +0300 Subject: [PATCH 04/22] Embed substitution into simplifyAndCheckComplimentary --- .../commonMain/kotlin/org/kosat/Assignment.kt | 24 +++++++-- .../src/commonMain/kotlin/org/kosat/CDCL.kt | 53 ++++++++----------- 2 files changed, 44 insertions(+), 33 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index fe7fb6be..e789448f 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -47,13 +47,31 @@ class Assignment(private val solver: CDCL) { return valueAfterSubstitution(lit.variable) xor lit.isNeg } - fun markSubstituted(variable: Var, substitution: Lit) { - check(varData[variable].substitution == null) - varData[variable].substitution = substitution + fun markSubstituted(lit: Lit, substitution: Lit) { + check(varData[lit.variable].substitution == null) + varData[lit.variable].substitution = substitution xor lit.isNeg } fun fixNestedSubstitutions() { + for (varIndex in 0 until numberOfVariables) { + val variable = Var(varIndex) + val substitution = varData[variable].substitution ?: continue + val secondSubstitution = varData[substitution.variable].substitution ?: continue + varData[variable].substitution = secondSubstitution xor substitution.isNeg + } + } + + fun substitute(lit: Lit): Lit { + val substitution = varData[lit.variable].substitution + return if (substitution != null) { + substitution xor lit.isNeg + } else { + lit + } + } + fun isSubstituted(v: Var): Boolean { + return varData[v].substitution != null } // fun assign(v: Var, value: LBool) { diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 7610a609..eaad50c8 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -144,8 +144,8 @@ class CDCL { clause.lits.removeAll { value(it) == LBool.FALSE } // If the clause contains complementary literals, ignore it as useless, - // otherwise removes duplicate literals in it. - if (sortDedupAndCheckComplimentary(clause.lits)) return + // perform substitution otherwise + if (simplifyAndCheckComplimentary(clause.lits)) return when (clause.size) { // Empty clause is an immediate UNSAT @@ -168,11 +168,16 @@ class CDCL { } /** - * Takes a list of literals, sorts it and removes duplicates in place, + * Takes a list of literals, applies every variable substitution + * (see [VarState.substitution]), sorts it and removes duplicates in place, * then checks if the list contains a literal and its negation * and returns true if so. */ - private fun sortDedupAndCheckComplimentary(lits: MutableList): Boolean { + private fun simplifyAndCheckComplimentary(lits: MutableList): Boolean { + for (i in 0 until lits.size) { + lits[i] = assignment.substitute(lits[i]) + } + lits.sortBy { it.inner } var i = 0 @@ -223,16 +228,14 @@ class CDCL { * [SolveResult.SAT], [SolveResult.UNSAT], or [SolveResult.UNKNOWN]. */ fun solve(currentAssumptions: List = emptyList()): SolveResult { - assumptions = currentAssumptions.map { - assignment.varData[it.variable].substitution?.xor(it.isNeg) ?: it - }.toMutableList() + assumptions = currentAssumptions.toMutableList() // If given clauses are already cause UNSAT, no need to do anything if (!ok) return finishWithUnsat() // Check if the assumptions are trivially unsatisfiable, - // and remove duplicates along the way. - if (sortDedupAndCheckComplimentary(assumptions)) return finishWithAssumptionsUnsat() + // performing substitutions along the way if required + if (simplifyAndCheckComplimentary(assumptions)) return finishWithAssumptionsUnsat() // Clean up from the previous solve if (assignment.decisionLevel > 0) backtrack(0) @@ -435,7 +438,7 @@ class CDCL { dratBuilder.addComment("Preprocessing: Equivalent literal substitution") - for (i in 1..10) { + for (i in 1..1) { equivalentLiteralSubstitution()?.let { return it } } @@ -529,9 +532,11 @@ class CDCL { } marks[w] = 4 } + for (w in scc) { + if (w != v) assignment.markSubstituted(w, v) + } break } - assignment.varData[u.variable].substitution = v xor u.isNeg } } @@ -543,7 +548,7 @@ class CDCL { val lit = variable.posLit if ( - assignment.varData[variable].substitution != null || + assignment.isSubstituted(variable) || (marks[lit] != 0 || marks[lit.neg] != 0) || value(lit) != LBool.UNDEF ) continue @@ -552,26 +557,18 @@ class CDCL { dfs(lit) ?: return finishWithUnsat() } - for (varIndex in 0 until assignment.numberOfVariables) { - val variable = Var(varIndex) - val substitution = assignment.varData[variable].substitution ?: continue - val secondSubstitution = assignment.varData[substitution.variable].substitution ?: continue - assignment.varData[variable].substitution = secondSubstitution xor substitution.isNeg - } + assignment.fixNestedSubstitutions() for (clause in db.clauses + db.learnts) { if (clause.deleted) continue - val willChange = clause.lits.any { assignment.varData[it.variable].substitution != null } + val willChange = clause.lits.any { assignment.isSubstituted(it.variable) } if (!willChange) continue - val newLits = clause.lits.map { - assignment.varData[it.variable].substitution?.xor(it.isNeg) ?: it - }.toMutableList() + val newLits = clause.lits.toMutableList() + val containsComplementary = simplifyAndCheckComplimentary(newLits) - val useless = sortDedupAndCheckComplimentary(newLits) - - if (!useless) { + if (!containsComplementary) { val newClause = Clause(newLits, clause.learnt) if (newClause.size == 1 || !clause.learnt) dratBuilder.addClause(newClause) if (newClause.size == 1) { @@ -588,11 +585,7 @@ class CDCL { propagate()?.let { return finishWithUnsat() } - assumptions = assumptions.map { - assignment.varData[it.variable].substitution?.xor(it.isNeg) ?: it - }.toMutableList() - - if (sortDedupAndCheckComplimentary(assumptions)) { + if (simplifyAndCheckComplimentary(assumptions)) { return finishWithAssumptionsUnsat() } From 23f9e2023ce05eb38412081c8d23b7a63278195e Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Mon, 24 Jul 2023 17:56:36 +0300 Subject: [PATCH 05/22] ELS Optimization and integration with FLP --- .../commonMain/kotlin/org/kosat/Assignment.kt | 3 +- .../src/commonMain/kotlin/org/kosat/CDCL.kt | 44 ++++++++++++------- .../jvmTest/kotlin/org/kosat/DiamondTests.kt | 3 +- 3 files changed, 32 insertions(+), 18 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index e789448f..0c21de57 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -48,7 +48,6 @@ class Assignment(private val solver: CDCL) { } fun markSubstituted(lit: Lit, substitution: Lit) { - check(varData[lit.variable].substitution == null) varData[lit.variable].substitution = substitution xor lit.isNeg } @@ -61,7 +60,7 @@ class Assignment(private val solver: CDCL) { } } - fun substitute(lit: Lit): Lit { + fun getSubstitutionOf(lit: Lit): Lit { val substitution = varData[lit.variable].substitution return if (substitution != null) { substitution xor lit.isNeg diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index eaad50c8..5f110802 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -63,6 +63,12 @@ class CDCL { */ private val flpMaxProbes = 1000 + /** + * Amount of [equivalentLiteralSubstitution] rounds before and after + * [failedLiteralProbing] to perform. + */ + private val elsRounds = 5; + /** * The branching heuristic, used to choose the next decision variable. */ @@ -175,7 +181,7 @@ class CDCL { */ private fun simplifyAndCheckComplimentary(lits: MutableList): Boolean { for (i in 0 until lits.size) { - lits[i] = assignment.substitute(lits[i]) + lits[i] = assignment.getSubstitutionOf(lits[i]) } lits.sortBy { it.inner } @@ -438,7 +444,7 @@ class CDCL { dratBuilder.addComment("Preprocessing: Equivalent literal substitution") - for (i in 1..1) { + for (i in 0 until elsRounds) { equivalentLiteralSubstitution()?.let { return it } } @@ -446,6 +452,13 @@ class CDCL { failedLiteralProbing()?.let { return it } + dratBuilder.addComment("Preprocessing: Equivalent literal substitution (post FLP)") + + for (i in 0 until elsRounds) { + equivalentLiteralSubstitution()?.let { return it } + } + + // Without this, we might let the solver propagate nothing // and make a decision after all values are set. if (assignment.trail.size == assignment.numberOfVariables) { @@ -493,6 +506,7 @@ class CDCL { val num = MutableList(assignment.numberOfVariables * 2) { 0 } val stack = mutableListOf() var counter = 0 + var totalSubstituted = 0 fun dfs(v: Lit): Int? { check(value(v) == LBool.UNDEF) @@ -535,6 +549,7 @@ class CDCL { for (w in scc) { if (w != v) assignment.markSubstituted(w, v) } + totalSubstituted += scc.size - 1 break } } @@ -553,10 +568,11 @@ class CDCL { value(lit) != LBool.UNDEF ) continue - check(marks[lit] == 0) dfs(lit) ?: return finishWithUnsat() } + if (totalSubstituted == 0) return null + assignment.fixNestedSubstitutions() for (clause in db.clauses + db.learnts) { @@ -595,18 +611,10 @@ class CDCL { } /** - * Literal probing is only useful if the probe can lead + * Literal probing is only useful if the probe can * lead to derivation of something by itself. We can * generate list of possibly useful probes ahead of time. * - * TODO: Right now, this implementation is very naive. - * If there is a cycle in binary implication graph, - * we will generate a lot of useless probes that will - * propagate in exactly the same way and possibly - * produce a lot of duplicate/implied binary clauses. - * This will be fixed with the implementation of - * Equivalent Literal Substitution (ELS). - * * @return list of literals to try probing with */ private fun generateProbes(): List { @@ -618,13 +626,19 @@ class CDCL { if (clause.size == 2) { val (a, b) = clause.lits if (assignment.value(a) == LBool.UNDEF) probes.add(a.neg) - if (probes.size >= flpMaxProbes) break if (assignment.value(b) == LBool.UNDEF) probes.add(b.neg) - if (probes.size >= flpMaxProbes) break } } - return probes.toMutableList() + for (clause in db.clauses) { + if (clause.size == 2) { + val (a, b) = clause.lits + probes.remove(a) + probes.remove(b) + } + } + + return probes.take(flpMaxProbes).toMutableList() } /** diff --git a/kosat-core/src/jvmTest/kotlin/org/kosat/DiamondTests.kt b/kosat-core/src/jvmTest/kotlin/org/kosat/DiamondTests.kt index ac10a2e5..b5308fda 100644 --- a/kosat-core/src/jvmTest/kotlin/org/kosat/DiamondTests.kt +++ b/kosat-core/src/jvmTest/kotlin/org/kosat/DiamondTests.kt @@ -100,6 +100,7 @@ internal class DiamondTests { } println("MiniSat conflicts: ${backend.numberOfConflicts}") println("Minisat decisions: ${backend.numberOfDecisions}") + println("MiniSat result: $result") result } @@ -234,7 +235,7 @@ internal class DiamondTests { @ParameterizedTest(name = "{1}") @MethodSource("getBenchmarkFiles") - @Disabled + // @Disabled fun testOnBenchmarks(file: File, testName: String) { println("# Testing on: $file") runTest(file, CNF.from(file.toOkioPath())) From ad19bb2da65259b9b91423dd2b79c2fc5e7741b5 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Mon, 24 Jul 2023 18:39:44 +0300 Subject: [PATCH 06/22] Comments and refactoring --- .../src/commonMain/kotlin/org/kosat/CDCL.kt | 145 ++++++++++++++---- .../jvmTest/kotlin/org/kosat/DiamondTests.kt | 2 +- 2 files changed, 115 insertions(+), 32 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 5f110802..37351822 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -67,7 +67,7 @@ class CDCL { * Amount of [equivalentLiteralSubstitution] rounds before and after * [failedLiteralProbing] to perform. */ - private val elsRounds = 5; + private val elsRounds = 5 /** * The branching heuristic, used to choose the next decision variable. @@ -444,9 +444,10 @@ class CDCL { dratBuilder.addComment("Preprocessing: Equivalent literal substitution") - for (i in 0 until elsRounds) { - equivalentLiteralSubstitution()?.let { return it } - } + // Running ELS before FLP helps to get more binary clauses + // and remove cycles in the binary implication graph + // to make probes for FLP more effective + equivalentLiteralSubstitutionRounds()?.let { return it } dratBuilder.addComment("Preprocessing: Failed literal probing") @@ -454,9 +455,10 @@ class CDCL { dratBuilder.addComment("Preprocessing: Equivalent literal substitution (post FLP)") - for (i in 0 until elsRounds) { - equivalentLiteralSubstitution()?.let { return it } - } + // After FLP we might have gotten new binary clauses + // though hyper-binary resolution, so we run ELS again + // to substitute literals that are now equivalent + equivalentLiteralSubstitutionRounds()?.let { return it } // Without this, we might let the solver propagate nothing @@ -479,7 +481,13 @@ class CDCL { return null } - private fun impliedLiterals(lit: Lit): List { + /** + * Returns the list of literals that are directly implied by + * the given literal though binary clauses. + * + * @see equivalentLiteralSubstitution + */ + private fun binaryImplicationsFrom(lit: Lit): List { check(value(lit) == LBool.UNDEF) val implied = mutableListOf() @@ -497,58 +505,126 @@ class CDCL { return implied } - private fun equivalentLiteralSubstitution(): SolveResult? { - check(assignment.decisionLevel == 0) - + /** + * Performs multiple rounds of [equivalentLiteralSubstitution]. + * + * This is because ELS can be used to derive new binary clauses, + * which in turn can be used to derive new ELS substitutions. + */ + private fun equivalentLiteralSubstitutionRounds(): SolveResult? { + // This simplify helps to increase the number of binary clauses + // and allows to not think about assigned literals in ELS itself. db.simplify() - val marks = MutableList(assignment.numberOfVariables * 2) { 0 } + for (i in 0 until elsRounds) { + equivalentLiteralSubstitution()?.let { return it } + } + + // We must update assumptions after ELS, because it can + // substitute literals in assumptions, and even derive UNSAT. + if (simplifyAndCheckComplimentary(assumptions)) { + return finishWithAssumptionsUnsat() + } + + variableSelector.initAssumptions(assumptions) + + return null + } + + /** + * Equivalent Literal Substitution (ELS) is a preprocessing technique + * that tries to find literals that are equivalent to each other. + * + * Consider clauses (-1, -2), (2, 3) and (-3, 1). In every satisfying + * assignment, 1 is equal to -2, and -2 is equal to 3. This means that + * we can substitute, for example, -2 and 3 with 1 in every clause, + * and the problem will generally remain the same. + * + * This function tries to find such literals and substitute them. To do + * this, it searches for strongly connected components in the binary + * implication graph, selects one representative literal from each + * component, and substitutes all other literals in the component with + * the representative. + */ + private fun equivalentLiteralSubstitution(): SolveResult? { + require(assignment.decisionLevel == 0) + + // To find strongly connected components, we use Tarjan's algorithm. + // https://en.wikipedia.org/wiki/Tarjan%27s_strongly_connected_components_algorithm + + // Indicates that the literal is not visited yet + val markUnvisited = 0 + // Indicates that the literal is in the stack (from Tarjan's algorithm) + val markInStack = 1 + // Indicates that the literal got in the strongly connected component + // after stack unwinding, but not substituted yet + val markInScc = 2 + // Indicates that the literal is processed, and possibly substituted + val markProcessed = 3 + + // Marks for each literal, as above + val marks = MutableList(assignment.numberOfVariables * 2) { markUnvisited } + // Tarjan's algorithm counter per literal val num = MutableList(assignment.numberOfVariables * 2) { 0 } - val stack = mutableListOf() var counter = 0 + + // Stack for Tarjan's algorithm + val stack = mutableListOf() + + // Total number of literals substituted var totalSubstituted = 0 + // Tarjan's algorithm, returns the lowest number of all reachable nodes + // from the given node, or null if the node is in a cycle with the + // negation of itself, and the problem is UNSAT fun dfs(v: Lit): Int? { check(value(v) == LBool.UNDEF) check(marks[v] == 0) - marks[v] = 1 + marks[v] = markInStack stack.add(v) counter++ num[v] = counter var lowest = counter - for (u in impliedLiterals(v)) { - if (marks[u] == 0) { + for (u in binaryImplicationsFrom(v)) { + if (marks[u] == markUnvisited) { val otherLowest = dfs(u) ?: return null lowest = min(otherLowest, lowest) - } else if (marks[u] != 4) { + } else if (marks[u] != markProcessed) { lowest = min(lowest, num[u]) } } - marks[v] = 2 - if (lowest == num[v]) { val scc = mutableListOf() while (true) { val u = stack.removeLast() - marks[u] = 3 + marks[u] = markInScc scc.add(u) if (u == v) { for (w in scc) { - if (marks[w.neg] == 3) { - dratBuilder.addComment("Found UNSAT due to complement literals being in the same SCC") + // If two complementary literals are in the same SCC, + // the problem is UNSAT + if (marks[w.neg] == markInScc) { + dratBuilder.addComment( + "Discovered UNSAT due to complement literals being in the same SCC" + ) + // Adding unit clauses is required for the proof dratBuilder.addClause(Clause(mutableListOf(w))) dratBuilder.addClause(Clause(mutableListOf(w.neg))) return null } - marks[w] = 4 + marks[w] = markProcessed } + + // We can choose any literal from the SCC as a + // representative, so we choose v for (w in scc) { if (w != v) assignment.markSubstituted(w, v) } + // Note that there is no need to add clauses to the proof totalSubstituted += scc.size - 1 break } @@ -558,13 +634,18 @@ class CDCL { return lowest } + // We perform substitution for all reachable SCCs from every positive + // literal. There is no need to do it for negative literals, because + // those will just produce the same substitutions (the binary + // implication graph is symmetrical), and we are likely to visit both + // positive and negative literals anyway. for (varIndex in 0 until assignment.numberOfVariables) { val variable = Var(varIndex) val lit = variable.posLit if ( assignment.isSubstituted(variable) || - (marks[lit] != 0 || marks[lit.neg] != 0) || + (marks[lit] != markUnvisited || marks[lit.neg] != markUnvisited) || value(lit) != LBool.UNDEF ) continue @@ -575,6 +656,7 @@ class CDCL { assignment.fixNestedSubstitutions() + // Replace clauses which might have simplified due to substitution for (clause in db.clauses + db.learnts) { if (clause.deleted) continue @@ -583,9 +665,13 @@ class CDCL { val newLits = clause.lits.toMutableList() val containsComplementary = simplifyAndCheckComplimentary(newLits) - + // Note that clause cannot become empty, + // however, it can contain complementary literals. + // We simply remove such clauses. if (!containsComplementary) { val newClause = Clause(newLits, clause.learnt) + // Only learnt, non-unit clauses are added to the proof automatically, + // so we have to add the rest manually if (newClause.size == 1 || !clause.learnt) dratBuilder.addClause(newClause) if (newClause.size == 1) { if (!assignment.enqueue(newClause[0], null)) { @@ -599,14 +685,9 @@ class CDCL { markDeleted(clause) } + // Propagate all the new unit clauses which might have been discovered. propagate()?.let { return finishWithUnsat() } - if (simplifyAndCheckComplimentary(assumptions)) { - return finishWithAssumptionsUnsat() - } - - variableSelector.initAssumptions(assumptions) - return null } @@ -630,6 +711,8 @@ class CDCL { } } + // Remove probes that follow from binary clauses, + // leaving only roots of the binary implication graph for (clause in db.clauses) { if (clause.size == 2) { val (a, b) = clause.lits diff --git a/kosat-core/src/jvmTest/kotlin/org/kosat/DiamondTests.kt b/kosat-core/src/jvmTest/kotlin/org/kosat/DiamondTests.kt index b5308fda..d47ab6df 100644 --- a/kosat-core/src/jvmTest/kotlin/org/kosat/DiamondTests.kt +++ b/kosat-core/src/jvmTest/kotlin/org/kosat/DiamondTests.kt @@ -235,7 +235,7 @@ internal class DiamondTests { @ParameterizedTest(name = "{1}") @MethodSource("getBenchmarkFiles") - // @Disabled + @Disabled fun testOnBenchmarks(file: File, testName: String) { println("# Testing on: $file") runTest(file, CNF.from(file.toOkioPath())) From f0ea5af46ab62e238733bf8c4b54372cd7fe6939 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 10:44:30 +0300 Subject: [PATCH 07/22] Rename simplifyAndCheckComplimentary -> substituteAndCheckComplimentary --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 37351822..d6179783 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -151,7 +151,7 @@ class CDCL { // If the clause contains complementary literals, ignore it as useless, // perform substitution otherwise - if (simplifyAndCheckComplimentary(clause.lits)) return + if (substituteAndCheckComplimentary(clause.lits)) return when (clause.size) { // Empty clause is an immediate UNSAT @@ -179,7 +179,7 @@ class CDCL { * then checks if the list contains a literal and its negation * and returns true if so. */ - private fun simplifyAndCheckComplimentary(lits: MutableList): Boolean { + private fun substituteAndCheckComplimentary(lits: MutableList): Boolean { for (i in 0 until lits.size) { lits[i] = assignment.getSubstitutionOf(lits[i]) } @@ -241,7 +241,7 @@ class CDCL { // Check if the assumptions are trivially unsatisfiable, // performing substitutions along the way if required - if (simplifyAndCheckComplimentary(assumptions)) return finishWithAssumptionsUnsat() + if (substituteAndCheckComplimentary(assumptions)) return finishWithAssumptionsUnsat() // Clean up from the previous solve if (assignment.decisionLevel > 0) backtrack(0) @@ -522,7 +522,7 @@ class CDCL { // We must update assumptions after ELS, because it can // substitute literals in assumptions, and even derive UNSAT. - if (simplifyAndCheckComplimentary(assumptions)) { + if (substituteAndCheckComplimentary(assumptions)) { return finishWithAssumptionsUnsat() } @@ -664,7 +664,7 @@ class CDCL { if (!willChange) continue val newLits = clause.lits.toMutableList() - val containsComplementary = simplifyAndCheckComplimentary(newLits) + val containsComplementary = substituteAndCheckComplimentary(newLits) // Note that clause cannot become empty, // however, it can contain complementary literals. // We simply remove such clauses. From 8d5db5e3cae5e6732c38572c5abbc9c99e2d7469 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 10:47:22 +0300 Subject: [PATCH 08/22] Replace if with an assertion --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index d6179783..4a1caa81 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -674,9 +674,7 @@ class CDCL { // so we have to add the rest manually if (newClause.size == 1 || !clause.learnt) dratBuilder.addClause(newClause) if (newClause.size == 1) { - if (!assignment.enqueue(newClause[0], null)) { - return finishWithUnsat() - } + check(assignment.enqueue(newClause[0], null)) } else { attachClause(newClause) } From 0a61658745f34c978617082e74c2bc0189389d5c Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 10:48:32 +0300 Subject: [PATCH 09/22] Remove redundant guard in propagate --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 4 ---- 1 file changed, 4 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 4a1caa81..48b6520e 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -1050,10 +1050,6 @@ class CDCL { check(value(lit) == LBool.TRUE) - if (value(lit) == LBool.FALSE) { - return assignment.reason(lit.variable) - } - // Checking the list of clauses watching the negation of the literal. // In those clauses, both of the watched literals might be false, // which can either lead to a conflict (all literals in clause are false), From ffc877e4739f1967536ac29e47fa54e838087d10 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 10:49:20 +0300 Subject: [PATCH 10/22] Make value(lit) private --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 2 +- 1 file changed, 1 insertion(+), 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 48b6520e..6b8d4971 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -127,7 +127,7 @@ class CDCL { polarity.add(LBool.UNDEF) } - fun value(lit: Lit): LBool { + private fun value(lit: Lit): LBool { return assignment.value(lit) } From 6dd617fbdd994b856bf99fd52a9b7d9bb8a98092 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 11:08:42 +0300 Subject: [PATCH 11/22] Comments, checks and fixes --- .../commonMain/kotlin/org/kosat/Assignment.kt | 33 +++++++++++++++++++ .../src/commonMain/kotlin/org/kosat/CDCL.kt | 6 ++-- .../kotlin/org/kosat/SolverTypes.kt | 4 +++ .../kotlin/org/kosat/VariableSelector.kt | 4 +-- 4 files changed, 43 insertions(+), 4 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index 0c21de57..d9c7527e 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -26,14 +26,24 @@ class Assignment(private val solver: CDCL) { var qhead: Int = 0 var qheadBinaryOnly: Int = 0 + /** + * @return the value of the variable, assuming that it is not substituted. + */ fun value(v: Var): LBool { return value[v] } + /** + * @return the value of the literal, assuming that it is not substituted. + */ fun value(lit: Lit): LBool { return value[lit.variable] xor lit.isNeg } + /** + * @return the value of the variable, considering its substitution if + * needed. + */ fun valueAfterSubstitution(v: Var): LBool { val substitution = varData[v].substitution return if (substitution != null) { @@ -43,23 +53,43 @@ class Assignment(private val solver: CDCL) { } } + /** + * @return the value of the literal, considering its substitution if + * needed. + */ fun valueAfterSubstitution(lit: Lit): LBool { return valueAfterSubstitution(lit.variable) xor lit.isNeg } + /** + * Marks the literal as substituted by the given literal. + */ fun markSubstituted(lit: Lit, substitution: Lit) { + // FIXME: + // if (varData[lit.variable].substitution == null) numberOfSubstitutions++ varData[lit.variable].substitution = substitution xor lit.isNeg } + /** + * If a literal is substituted by another literal, which is then substituted + * by another literal, then the first literal is substituted by the last + * literal. This function removes such nested substitutions, up to the + * depth of 2. + */ fun fixNestedSubstitutions() { for (varIndex in 0 until numberOfVariables) { val variable = Var(varIndex) val substitution = varData[variable].substitution ?: continue val secondSubstitution = varData[substitution.variable].substitution ?: continue + check(varData[secondSubstitution.variable].substitution == null) varData[variable].substitution = secondSubstitution xor substitution.isNeg } } + /** + * @return the substitution of the literal, if it is substituted, or the + * literal itself otherwise. + */ fun getSubstitutionOf(lit: Lit): Lit { val substitution = varData[lit.variable].substitution return if (substitution != null) { @@ -69,6 +99,9 @@ class Assignment(private val solver: CDCL) { } } + /** + * @return true if the variable is substituted. + */ fun isSubstituted(v: Var): Boolean { return varData[v].substitution != null } diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 6b8d4971..3f3a7822 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -620,9 +620,11 @@ class CDCL { } // We can choose any literal from the SCC as a - // representative, so we choose v + // representative, so we choose the minimal one to + // avoid re-substitution to a different literal later + val repr = scc.minBy { it.inner } for (w in scc) { - if (w != v) assignment.markSubstituted(w, v) + if (w != repr) assignment.markSubstituted(w, repr) } // Note that there is no need to add clauses to the proof totalSubstituted += scc.size - 1 diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt b/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt index bf3f78ce..115945f2 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt @@ -64,6 +64,10 @@ value class Lit(val inner: Int) { return if (isPos) v else -v } + /** + * Returns a literal not equal to `this`, among two given literals, + * assuming that `this` is (at least) one of them. + */ fun differentAmong2(lit1: Lit, lit2: Lit): Lit { check(this == lit1 || this == lit2) return Lit(inner xor lit1.inner xor lit2.inner) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt b/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt index 331927ca..d1d0a670 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt @@ -215,8 +215,8 @@ class VSIDS(private var numberOfVariables: Int = 0) : VariableSelector() { } // if there is undefined assumption pick it, other way pick best choice return assumptions.firstOrNull { - assignment.value(it) == LBool.UNDEF && - assignment.varData[it.variable].substitution == null + assignment.varData[it.variable].substitution == null && + assignment.value(it) == LBool.UNDEF } ?: getMaxActivityVariable(assignment).posLit } From ef3114f51fa830c2ebdbede028d77ed44333311f Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 11:09:01 +0300 Subject: [PATCH 12/22] Redundant functions --- kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt | 8 -------- 1 file changed, 8 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index d9c7527e..3068f67f 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -106,10 +106,6 @@ class Assignment(private val solver: CDCL) { return varData[v].substitution != null } - // fun assign(v: Var, value: LBool) { - // value[v] = value - // } - fun unassign(v: Var) { value[v] = LBool.UNDEF varData[v].reason = null @@ -117,10 +113,6 @@ class Assignment(private val solver: CDCL) { varData[v].trailIndex = -1 } - // fun varData(v: Var): VarState { - // return varData[v] - // } - fun reason(v: Var): Clause? { return varData[v].reason } From 1b03347195963badd6d08dea4ce93ef71651dd2c Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 11:11:02 +0300 Subject: [PATCH 13/22] Make variable selector only choose non-substituted vars --- kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt | 3 +-- .../src/commonMain/kotlin/org/kosat/VariableSelector.kt | 5 ++--- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index 3068f67f..c1b03505 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -65,8 +65,7 @@ class Assignment(private val solver: CDCL) { * Marks the literal as substituted by the given literal. */ fun markSubstituted(lit: Lit, substitution: Lit) { - // FIXME: - // if (varData[lit.variable].substitution == null) numberOfSubstitutions++ + if (varData[lit.variable].substitution == null) numberOfSubstitutions++ varData[lit.variable].substitution = substitution xor lit.isNeg } diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt b/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt index d1d0a670..0cf6da57 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/VariableSelector.kt @@ -215,8 +215,7 @@ class VSIDS(private var numberOfVariables: Int = 0) : VariableSelector() { } // if there is undefined assumption pick it, other way pick best choice return assumptions.firstOrNull { - assignment.varData[it.variable].substitution == null && - assignment.value(it) == LBool.UNDEF + assignment.value(it) == LBool.UNDEF } ?: getMaxActivityVariable(assignment).posLit } @@ -231,7 +230,7 @@ class VSIDS(private var numberOfVariables: Int = 0) : VariableSelector() { while (true) { require(activityPQ.size > 0) val v = activityPQ.pop() - if (assignment.value(Var(v)) == LBool.UNDEF) { + if (assignment.varData[Var(v)].substitution == null && assignment.value(Var(v)) == LBool.UNDEF) { return Var(v) } } From 4c7a8cceebc13a393ea5c7afc64294994b53f2e6 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 11:19:20 +0300 Subject: [PATCH 14/22] Fix probe generation algorithm --- .../commonMain/kotlin/org/kosat/Assignment.kt | 3 +++ .../src/commonMain/kotlin/org/kosat/CDCL.kt | 24 ++++++++++--------- 2 files changed, 16 insertions(+), 11 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index c1b03505..7e46a19e 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -20,6 +20,8 @@ class Assignment(private val solver: CDCL) { val trail: MutableList = mutableListOf() val numberOfVariables get() = value.size private var numberOfSubstitutions = 0 + + /** The number of not substituted variables */ val numberOfActiveVariables get() = numberOfVariables - numberOfSubstitutions var decisionLevel: Int = 0 @@ -156,6 +158,7 @@ class Assignment(private val solver: CDCL) { fun uncheckedEnqueue(lit: Lit, reason: Clause?) { require(value(lit) == LBool.UNDEF) + require(varData[lit.variable].substitution == null) if (decisionLevel == 0) solver.dratBuilder.addClause(Clause(mutableListOf(lit))) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 3f3a7822..d11713f1 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -702,23 +702,25 @@ class CDCL { val probes = mutableSetOf() for (clause in db.clauses) { + if (clause.deleted) continue + if (clause.size == 2) continue + // (A | B) <==> (-A -> B) <==> (-B -> A) - // Both -A and -B can be used as probes - if (clause.size == 2) { - val (a, b) = clause.lits - if (assignment.value(a) == LBool.UNDEF) probes.add(a.neg) - if (assignment.value(b) == LBool.UNDEF) probes.add(b.neg) - } + // Both -A and -B can be used as probes, there is little need + // to choose both, however. + val (a, b) = clause.lits + probes.add(if (a.inner < b.inner) a.neg else b.neg) } // Remove probes that follow from binary clauses, // leaving only roots of the binary implication graph for (clause in db.clauses) { - if (clause.size == 2) { - val (a, b) = clause.lits - probes.remove(a) - probes.remove(b) - } + if (clause.deleted) continue + if (clause.size != 2) continue + + val (a, b) = clause.lits + probes.remove(a) + probes.remove(b) } return probes.take(flpMaxProbes).toMutableList() From 6fbd570d0faef9ccab988c87c4a9c59f3d1f64fd Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 11:22:00 +0300 Subject: [PATCH 15/22] Checks on value(...) --- kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index 7e46a19e..8227a026 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -32,6 +32,7 @@ class Assignment(private val solver: CDCL) { * @return the value of the variable, assuming that it is not substituted. */ fun value(v: Var): LBool { + check(varData[v].substitution == null) return value[v] } @@ -39,6 +40,11 @@ class Assignment(private val solver: CDCL) { * @return the value of the literal, assuming that it is not substituted. */ fun value(lit: Lit): LBool { + // TODO: It would be nice to have this assertion, + // however, there are too many moving pieces at the moment + // and enabling this will require a lot of additional + // isSubstituted checks. + // check(varData[lit.variable].substitution == null) return value[lit.variable] xor lit.isNeg } From edffce5a1125c976ff6e23f49f293b756efe0081 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Tue, 25 Jul 2023 11:22:31 +0300 Subject: [PATCH 16/22] Change check -> require --- kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt index 8227a026..ca66c88c 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Assignment.kt @@ -32,7 +32,7 @@ class Assignment(private val solver: CDCL) { * @return the value of the variable, assuming that it is not substituted. */ fun value(v: Var): LBool { - check(varData[v].substitution == null) + require(varData[v].substitution == null) return value[v] } @@ -44,7 +44,7 @@ class Assignment(private val solver: CDCL) { // however, there are too many moving pieces at the moment // and enabling this will require a lot of additional // isSubstituted checks. - // check(varData[lit.variable].substitution == null) + // require(varData[lit.variable].substitution == null) return value[lit.variable] xor lit.isNeg } From 23fb61ed4632a53915f9d4da9b81f3aaa1ba49c7 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Thu, 27 Jul 2023 16:23:44 +0300 Subject: [PATCH 17/22] Finalize FLP --- .../src/commonMain/kotlin/org/kosat/CDCL.kt | 53 ++++++++++--------- .../src/commonMain/kotlin/org/kosat/Clause.kt | 2 +- 2 files changed, 28 insertions(+), 27 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index d11713f1..7304c849 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -169,7 +169,7 @@ class CDCL { } } - else -> attachClause(clause) + else -> attachClause(clause, addToDrat = false) } } @@ -419,10 +419,12 @@ class CDCL { } for (varIndex in 0 until assignment.numberOfVariables) { - cachedModel!!.add(when (assignment.valueAfterSubstitution(Var(varIndex))) { - LBool.TRUE, LBool.UNDEF -> true - LBool.FALSE -> false - }) + cachedModel!!.add( + when (assignment.valueAfterSubstitution(Var(varIndex))) { + LBool.TRUE, LBool.UNDEF -> true + LBool.FALSE -> false + } + ) } return cachedModel!! @@ -672,9 +674,6 @@ class CDCL { // We simply remove such clauses. if (!containsComplementary) { val newClause = Clause(newLits, clause.learnt) - // Only learnt, non-unit clauses are added to the proof automatically, - // so we have to add the rest manually - if (newClause.size == 1 || !clause.learnt) dratBuilder.addClause(newClause) if (newClause.size == 1) { check(assignment.enqueue(newClause[0], null)) } else { @@ -838,25 +837,27 @@ class CDCL { // so we can learn a new clause val newBinary = hyperBinaryResolve(clause) + // Check that lit in either at index 0 of the clause and negated, + // or not in the clause at all. + check( + newBinary[0] == lit.neg || + lit.variable != newBinary[0].variable && lit.variable != newBinary[1].variable + ) + // The new clause may subsume the old one, rendering it useless - // TODO: However, we don't know if this clause is learned or given, - // so we can't let it be deleted. On the other hand, we can't - // allow just adding it to the list of clauses to keep, because - // this may result in too many clauses being kept. - // This should be reworked with the new clause storage mechanism, - // and new flags for clauses. Won't fix for now. - // TODO: this turns out to be more difficult than I expected and - // requires further investigation. - // if (newBinary[0] in clause.lits) { - // clause.deleted = true - // clausesToKeep.removeLast() - // newBinary.learnt = clause.learnt - // } - - attachClause(newBinary) + if (newBinary[0] in clause.lits) { + // We don't need to keep the clause in the watcher list + clausesToKeep.removeLast() + newBinary.learnt = clause.learnt + attachClause(newBinary) + markDeleted(clause) + } else { + // If not, simply add the new clause + attachClause(newBinary) + } // Make sure watch is not overwritten at the end of the loop - if (lit == newBinary[0]) clausesToKeep.add(newBinary) + if (lit.neg == newBinary[0]) clausesToKeep.add(newBinary) assignment.uncheckedEnqueue(clause[0], newBinary) // again, we try to only use binary clauses first @@ -1011,13 +1012,13 @@ class CDCL { /** * Add [clause] into the database and attach watchers for it. */ - private fun attachClause(clause: Clause) { + private fun attachClause(clause: Clause, addToDrat: Boolean = true) { require(clause.size >= 2) { clause } check(ok) db.add(clause) watchers[clause[0]].add(clause) watchers[clause[1]].add(clause) - if (clause.learnt) dratBuilder.addClause(clause) + if (addToDrat) dratBuilder.addClause(clause) } /** diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt index c6d67cf7..f723dc73 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt @@ -2,7 +2,7 @@ package org.kosat data class Clause( val lits: MutableList, - val learnt: Boolean = false, + var learnt: Boolean = false, ) { val size: Int get() = lits.size var deleted: Boolean = false From c5282028cddeca9b267495596da428ce6b6a4c7e Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Thu, 27 Jul 2023 16:26:51 +0300 Subject: [PATCH 18/22] Make learnt immutable as before --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 4 ++-- kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 7304c849..5e2dd175 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -835,7 +835,7 @@ class CDCL { } else if (firstNotFalse == -1) { // we deduced this literal from a non-binary clause, // so we can learn a new clause - val newBinary = hyperBinaryResolve(clause) + var newBinary = hyperBinaryResolve(clause) // Check that lit in either at index 0 of the clause and negated, // or not in the clause at all. @@ -848,7 +848,7 @@ class CDCL { if (newBinary[0] in clause.lits) { // We don't need to keep the clause in the watcher list clausesToKeep.removeLast() - newBinary.learnt = clause.learnt + newBinary = newBinary.copy(learnt = clause.learnt) attachClause(newBinary) markDeleted(clause) } else { diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt index f723dc73..c6d67cf7 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt @@ -2,7 +2,7 @@ package org.kosat data class Clause( val lits: MutableList, - var learnt: Boolean = false, + val learnt: Boolean = false, ) { val size: Int get() = lits.size var deleted: Boolean = false From e8cfaf15eab5ad6fbea461ecef800fe04e77262d Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Thu, 27 Jul 2023 18:20:49 +0300 Subject: [PATCH 19/22] Doc comment for CDCL.value. --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index 5e2dd175..a3491cb3 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -127,6 +127,12 @@ class CDCL { polarity.add(LBool.UNDEF) } + /** + * Return a value of the given literal, assuming it is not substituted. + * It is a shortcut for [Assignment.value]. + * + * @see Assignment.value + */ private fun value(lit: Lit): LBool { return assignment.value(lit) } From f9da66262eb11ca2033bec206bc628f045150c2c Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Thu, 27 Jul 2023 18:21:19 +0300 Subject: [PATCH 20/22] Comment on adding external clauses to the proof --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 2 ++ 1 file changed, 2 insertions(+) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index a3491cb3..a79b6af6 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -175,6 +175,8 @@ class CDCL { } } + // Clauses of size >2 are added to the database. + // We don't add externally provided clauses to the proof. else -> attachClause(clause, addToDrat = false) } } From 3ee96420a9c5a2967362af0346dd419b4c8b64e3 Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Fri, 28 Jul 2023 10:51:31 +0300 Subject: [PATCH 21/22] Remove differentAmong2 method and similar --- kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt | 8 ++++---- kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt | 4 ---- .../src/commonMain/kotlin/org/kosat/SolverTypes.kt | 9 --------- 3 files changed, 4 insertions(+), 17 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt index a79b6af6..b01220a4 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt @@ -505,7 +505,7 @@ class CDCL { if (watched.deleted) continue if (watched.size != 2) continue - val other = watched.otherWatch(lit.neg) + val other = Lit(watched[0].inner xor watched[1].inner xor lit.neg.inner) check(value(other) != LBool.FALSE) if (value(other) != LBool.UNDEF) continue @@ -901,7 +901,7 @@ class CDCL { if (clause.deleted) continue if (clause.size != 2) continue - val other = clause.otherWatch(lit.neg) + val other = Lit(clause[0].inner xor clause[1].inner xor lit.neg.inner) when (value(other)) { // if the other literal is true, the @@ -1004,11 +1004,11 @@ class CDCL { if (assignment.trailIndex(lcaVar) > assignment.trailIndex(litVar)) { check(assignment.reason(lcaVar)!!.size == 2) val (a, b) = assignment.reason(lcaVar)!!.lits - lca = lca.differentAmong2(a, b).neg + lca = Lit(lca.inner xor a.inner xor b.inner).neg } else { check(assignment.reason(litVar)!!.size == 2) val (a, b) = assignment.reason(litVar)!!.lits - lit = lit.differentAmong2(a, b).neg + lit = Lit(lit.inner xor a.inner xor b.inner).neg } } } diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt index c6d67cf7..8fcbc454 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt @@ -21,10 +21,6 @@ data class Clause( return lits.map { it.toDimacs() } } - fun otherWatch(lit: Lit): Lit { - return lit.differentAmong2(lits[0], lits[1]) - } - companion object { fun fromDimacs(clause: List): Clause { val lits = clause.map { Lit.fromDimacs(it) }.toMutableList() diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt b/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt index 115945f2..67538c47 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt @@ -64,15 +64,6 @@ value class Lit(val inner: Int) { return if (isPos) v else -v } - /** - * Returns a literal not equal to `this`, among two given literals, - * assuming that `this` is (at least) one of them. - */ - fun differentAmong2(lit1: Lit, lit2: Lit): Lit { - check(this == lit1 || this == lit2) - return Lit(inner xor lit1.inner xor lit2.inner) - } - infix fun xor(b: Boolean): Lit { return Lit(inner xor b.toInt()) } From cdf2bb2d3fccd0f86b237713c8229e4521d2ea1f Mon Sep 17 00:00:00 2001 From: Nikolay Stepanov Date: Fri, 28 Jul 2023 10:57:52 +0300 Subject: [PATCH 22/22] Fix merge issue --- kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt | 4 ---- 1 file changed, 4 deletions(-) diff --git a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt index c6d67cf7..8fcbc454 100644 --- a/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt +++ b/kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt @@ -21,10 +21,6 @@ data class Clause( return lits.map { it.toDimacs() } } - fun otherWatch(lit: Lit): Lit { - return lit.differentAmong2(lits[0], lits[1]) - } - companion object { fun fromDimacs(clause: List): Clause { val lits = clause.map { Lit.fromDimacs(it) }.toMutableList()