[ sat4j-Bugs-304773 ] Expensive Simplification implementation is incorrect

[<noreply@xxxxxxxxxxxxxxxxxxx>]

Bugs item #304773, was opened at 13/03/2006 23:21
You can respond by visiting: 
http://forge.objectweb.org/tracker/?func=detail&atid=350289&aid=304773&group_id=228

Category: core
Group: ongoing version (cvs)
Status: Open
Resolution: None
Priority: 9
Submitted By: Daniel Le Berre (leberre)
Assigned to: Daniel Le Berre (leberre)
Summary: Expensive Simplification implementation is incorrect

Initial Comment:
The expensive reason simplification from MiniSAT 1.14 has been added to the
current Solver.

It can be enabled by using:
solver.setSimplifier(solver.EXPENSIVE_SIMPLIFICATION);

Two new solvers in the minisat factory are using that new feature:

MiniLearningHeapExpSimplification
MiniSATHeapExpSimplification

Those two solvers are currently reporting incorrect results on the SAT RAce
benchmarks (they answer UNSAT on SAT benchmarks :-()


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

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