[ 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: v1.7
>Status: Closed
Resolution: Fixed
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 :-()


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

Comment By: Daniel Le Berre (leberre)
Date: 28/06/2006 20:59

Message:
connecté 
user_id=4369

The problem was that if in SAT4J the code is very close to
MiniSAT, using "cut and paste" of MiniSAT 1.14 does not work:
in SAT4J, the level, reason, etc is provided for a literal,
i.e. the translation of a literal into a variable is hidden
in Lits, while in MiniSAT those methods apply for variables.

The MiniLearningHeapExpSimplification  and
MiniSATHeapExpSimplification look perfectly correct now.


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

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