[ sat4j-Bugs-305407 ] Minimize memory footprint of SAT solver

[<noreply@xxxxxxxxxxxxxxxxxxx>]

Bugs item #305407, was opened at 31/05/2006 07:05
You can respond by visiting: 
http://forge.objectweb.org/tracker/?func=detail&atid=350289&aid=305407&group_id=228

Category: core
Group: v1.7
>Status: Closed
Resolution: Fixed
Priority: 6
Submitted By: Daniel Le Berre (leberre)
Assigned to: Daniel Le Berre (leberre)
Summary: Minimize memory footprint of SAT solver

Initial Comment:
Some SAT benchmarks are really huge with million of variables.

A reference in Java is 4 bytes, so for a benchmark with 8 million of clauses,
we use roughtly 32 megabytes to keep a reference to the very same ILits object
in each constraint!

I have no clean solution yet to fix this, but it would be nice to find a
solution to that problem for the SAT Race final submission (end of June).


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

Comment By: Daniel Le Berre (leberre)
Date: 28/06/2006 22:25

Message:
connecté 
user_id=4369

The WLClause class is now Abstract:
-DefaultWLClause act as the former WLClause, i.e. contains a
boolean attribute learnt on which the register method relies
to properly watch the initial literals.
-OriginalWLClause represents clauses appearing in the
original problem.
-LearntWLClause represent clauses learnt during the search,
hence the two literals watched need to be chosen carefully.

In theory, using those two separate classes to represent
clauses should allow to save some memory on huge benchmarks.

It needs to be observed in practice. 

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

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