Relax Dpll_core.add_clause requirement decision_level = 0
Brought to you by:
amit_goel,
jim_grundy
Menu
▾
▴
#1 Relax Dpll_core.add_clause requirement decision_level = 0
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.
Logged In: YES
user_id=1719425
Originator: YES
Feature added in 1.1 release.