Finalize FLP #48
Finalize FLP #48
Conversation
| } | ||
|
|
||
| fun value(lit: Lit): LBool { | ||
| private fun value(lit: Lit): LBool { |
There was a problem hiding this comment.
This method is a part of public API
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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).
| } | ||
|
|
||
| else -> attachClause(clause) | ||
| else -> attachClause(clause, addToDrat = false) |
There was a problem hiding this comment.
This line requires a comment, since other two branches have them.
Also, explain why do we need "addToDrat = false" here?
There was a problem hiding this comment.
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".
There was a problem hiding this comment.
Why not just check if (clause.learnt) dratBuilder.addClause(clause)?
There was a problem hiding this comment.
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.
| /** | ||
| * The number of variables. | ||
| */ | ||
| var numberOfVariables: Int = 0 |
There was a problem hiding this comment.
This field is a part of public API
There was a problem hiding this comment.
Number of variables is complicated now because there are two counters for that: number of variables from the CNF, and number of non-substituted variables actually used in the problem. It will be worse after BVE. I can leave a public getter to assignment.numberOfVariables if needed, but I won't for now. We will cross that bridge once we get to it.
There was a problem hiding this comment.
Yea, this is also a "problem" in Minisat and Cadical: that numberOfVariables does not represent the number of variables in the original CNF. We either should make a distinction between "active" (decision-able) and "eliminated" variables, or just store the largest variable index. It depends on how this field (numVars) is going to be used by users. Personally, I would be happy with the second (just get the largest used variable index from the solver, in order to be able to rely on the "weak invariant" newVar() == numVars+1). In addition, if I ever need "number of active/eliminated variables", I would expect separate fields/getters to exist for this matter.
| * The branching heuristic, used to choose the next decision variable. | ||
| */ | ||
| private val variableSelector: VariableSelector = VSIDS(numberOfVariables) | ||
| private val variableSelector: VariableSelector = VSIDS(assignment.numberOfVariables) |
There was a problem hiding this comment.
Why pass numberOfVariables in VSIDS constructor? Anyway, it is 0 when the solver is created. Maybe simplify the interfaces and eliminate unnecessary functionality?
There was a problem hiding this comment.
Will do once I get to it. For now, it is not related to FLP, nor proof generation in FLP.
| return lits.map { it.toDimacs() } | ||
| } | ||
|
|
||
| fun otherWatch(lit: Lit): Lit { |
There was a problem hiding this comment.
I would prefer not to extract this as a method. Just calculate it when necessary and as necessary (xor'ing or if'ing), no need to complicate the API of a Clause.
The same goes for "Lit::differentAmong2" method.
|
Back-merge |
# Conflicts: # kosat-core/src/commonMain/kotlin/org/kosat/CDCL.kt # kosat-core/src/commonMain/kotlin/org/kosat/SolverTypes.kt
Fixes an old TODO from FLP. Depends on #46.