#1 Relax Dpll_core.add_clause requirement decision_level = 0

closed
None
7
2007-10-01
2007-03-07
Jim Grundy
No

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.

Discussion

  • Jim Grundy

    Jim Grundy - 2007-10-01
    • assigned_to: nobody --> amit_goel
    • status: open --> closed
     
  • Jim Grundy

    Jim Grundy - 2007-10-01

    Logged In: YES
    user_id=1719425
    Originator: YES

    Feature added in 1.1 release.

     

Log in to post a comment.

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks