[ sat4j-Feature Requests-306483 ] Allow a programmatic way to ask the solver to backtrack

[<noreply@xxxxxxxxxxxxxxxxxxx>]

Feature Requests item #306483, was opened at 05/12/2006 22:24
You can respond by visiting: 
http://forge.objectweb.org/tracker/?func=detail&atid=350292&aid=306483&group_id=228

Category: SAT
Group: None
Status: Open
Priority: 7
Submitted By: Daniel Le Berre (leberre)
Assigned to: Daniel Le Berre (leberre)
Summary: Allow a programmatic way to ask the solver to backtrack

Initial Comment:
Some users would like to use side reasoners together with the SAT solver, a 
bit
in the spirit of SMT.

It is easy to receive the SAT solver events using the SearchListener 
interface.

However, there is currently no way for the side reasoner to ask the solver to
backtrack if it detects an inconsistency.

It would be nice to allow that feature, provided that the side reasoner can
provide a falsified set of literals for that backtrack.



----------------------------------------------------------------------

You can respond by visiting: 
http://forge.objectweb.org/tracker/?func=detail&atid=350292&aid=306483&group_id=228