Skip to content

Finalize FLP #48

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 23 commits into from
Jul 28, 2023
Merged

Finalize FLP #48

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
23 commits
Select commit Hold shift + click to select a range
733d9f6
Store substitution for variables for ELS
elteammate Jul 24, 2023
22f2542
Use xor to find not-equal literal instead of ifs
elteammate Jul 24, 2023
ee96542
Potential ELS implementation
elteammate Jul 24, 2023
dfe0224
Embed substitution into simplifyAndCheckComplimentary
elteammate Jul 24, 2023
23f9e20
ELS Optimization and integration with FLP
elteammate Jul 24, 2023
ad19bb2
Comments and refactoring
elteammate Jul 24, 2023
f0ea5af
Rename simplifyAndCheckComplimentary -> substituteAndCheckComplimentary
elteammate Jul 25, 2023
8d5db5e
Replace if with an assertion
elteammate Jul 25, 2023
0a61658
Remove redundant guard in propagate
elteammate Jul 25, 2023
ffc877e
Make value(lit) private
elteammate Jul 25, 2023
6dd617f
Comments, checks and fixes
elteammate Jul 25, 2023
ef3114f
Redundant functions
elteammate Jul 25, 2023
1b03347
Make variable selector only choose non-substituted vars
elteammate Jul 25, 2023
4c7a8cc
Fix probe generation algorithm
elteammate Jul 25, 2023
6fbd570
Checks on value(...)
elteammate Jul 25, 2023
edffce5
Change check -> require
elteammate Jul 25, 2023
23fb61e
Finalize FLP
elteammate Jul 27, 2023
c528202
Make learnt immutable as before
elteammate Jul 27, 2023
e8cfaf1
Doc comment for CDCL.value.
elteammate Jul 27, 2023
f9da662
Comment on adding external clauses to the proof
elteammate Jul 27, 2023
3ee9642
Remove differentAmong2 method and similar
elteammate Jul 28, 2023
5cf3f23
Merge branch 'dev' into feature/flp
elteammate Jul 28, 2023
cdf2bb2
Fix merge issue
elteammate Jul 28, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
71 changes: 40 additions & 31 deletions kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This method is a part of public API

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Not anymore.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But it should be :)
How else are you going to extract values of literals after solving the SAT? "Build a model" is not a right answer to this: (1) model might be too large (consider the situation when you really need the value of only one literal out of 1kk variables), (2) in the model you replace LBool.Undef with true, basically losing the information about the literal state.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

While it is possible to correctly return LBool.Undef right now, things might get interesting soon.

"Build a model" is not a right answer to this

Hilariously, "build a model" might be the right answer to this. I don't know the details of how this is implemented in MiniSat, but in Cadical, before every call to External::ival, it checks if the assignment have been "extended" (External::extended), and if not, it "extends" it. By "extension" authors mean "reconstruction". This operation is pretty much identical to building the model in our solver.

Consider BVE. The only way to get the value of eliminated variable is to traverse back the clauses which got resolved and check if those are satisfied. This is process takes O(length of all resolved clauses), worse case, and there is no way around it. It is true that "model might be too large", but reconstruction takes O(see above), a pretty trivial one, actually, while the solving takes however long it needs. The current implementation with substitution is potentially even faster (but I'm going to get rid of it soon). I think there is no reason in trying to optimize out reconstruction.

in the model you replace LBool.Undef with true, basically losing the information about the literal state.

True, but this only triggers if the state of the solver is trivial (i.e. all clauses got simplified away). If we got to the search phase, we need the entire trail of assignments. I am willing to ignore that. From an API standpoint, I don't
see a point of exposing values of partial assignments: those are private to the solver. Finally, in Cadical, Solver::ival also returns either true or false (kind of).

return assignment.value(lit)
}
Expand Down Expand Up @@ -169,7 +175,9 @@ class CDCL {
}
}

else -> attachClause(clause)
// Clauses of size >2 are added to the database.
// We don't add externally provided clauses to the proof.
else -> attachClause(clause, addToDrat = false)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This line requires a comment, since other two branches have them.
Also, explain why do we need "addToDrat = false" here?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is actually a workaround, and a pretty ugly one. I don't like how current dratChecker interact with the solver at all, but to fix this, the DRAT builder needs to be passed as the constructor. I can just remove this parameter, it won't hurt, but for now I want to keep invariant "original clauses are not in the proof".

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why not just check if (clause.learnt) dratBuilder.addClause(clause)?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did that initially, but it turns out it only makes things difficult. During preprocessing we often need to modify non-learnt clauses, which means it has to be recorded in the proof. However, we cannot make new clause learnt because it is irredundant, so non-learnts have to be added to the proof manually. Even worse, this means that there is no way to distinguish irredundant and initially given clauses later, so those added irredundant clauses are permanently staying in the proof. I can either store separate flags in Clause for learnt (redundant) and added (not given in the CNF initailly), or just duplicate the initial CNF in proof. I find the second approach favourable because it removes the complexity of clause state entirely, but one may argue that it is more "hacky" and requires solver to have dratBuilder during every call to newClause (which is not the case right now because CNF can be provided in the constructor), adding some complexity.

}
}

Expand Down Expand Up @@ -419,10 +427,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!!
Expand Down Expand Up @@ -495,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
Expand Down Expand Up @@ -672,9 +682,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 {
Expand Down Expand Up @@ -836,27 +843,29 @@ 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.
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 = newBinary.copy(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
Expand Down Expand Up @@ -892,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
Expand Down Expand Up @@ -995,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
}
}
}
Expand All @@ -1011,13 +1020,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)
}

/**
Expand Down
4 changes: 0 additions & 4 deletions kosat-core/src/commonMain/kotlin/org/kosat/Clause.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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<Int>): Clause {
val lits = clause.map { Lit.fromDimacs(it) }.toMutableList()
Expand Down
9 changes: 0 additions & 9 deletions kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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())
}
Expand Down