Currently Dpll_core.add_clause requires that
decision_level is 0. This may require starting the
solver if you need to add clauses incrementally. This
need not be the case.
The solver may not need to backtrack at all if the clause
is not conflicting in the current state. Otherwise we
should backtrack the solver as needed to make an
inference or deduce a conflict.
It is possible to figure out how far to backtrack the solver in time linear in the number of clause literals.
Log in to post a comment.