CVS log for sat4j/core/src/org/sat4j/minisat/SolverFactory.java
	Help

Request diff between arbitrary revisions / Display revisions graphically

Updated EPL headers (Pascal) + ref to Minisat paper.

Allow the use of optimisation solvers in SolverFactory thanks to the OptToSat adapter.

Added phase selection strategy.

The solver now displays the kind of benchmarks it works on.
Added a way to easily change the phase selection strategy in the main heuristics (VarOrderHeap).

Going Back to normal, stable code, hopefully.

Huge refactoring to allow a finer control of the type of constraints managed by the Solver.

Beware: the code is not stable at all. I will fix this tonight. Do not update until further notice.

Removed newMiniMaxSAT solver for the core SolverFactory.

Added a generic type to the solver decorator in order to avoid downcasting in PB code.

Added back newMiniMaxSAT in the solver factory.

Added a new generic parameter to Solver. Should not affect black box users.

Fixed many warnings.

Removed MaxSat solver.

Removed CSP and PB related code for the 2.0 release.

Removed dependency to MiniSATRestarts in Solver to break a last cycle in package dependencies.

The solvers returned by the factory methods are now fully typed (from a generics point of view).

Fixed learning scheme. Refactored existing classes.

Added PB solver with clause only learning.

Removed Rapid Restart Strategy.

Using Rapid restarts strategy.

Fix: use a full PB solver, not one using a reduction to clause.

Added a PB solver without learning.

Made the solver with Armin Biere rapid restart strategy the default solver.

Set parameters the same as the ones in picosat.

Added two new solvers: one with Armin Biere restarts strategy, one with a luby style strategy.

add a new pb-solver using merging rule

Used Generics to prevent the use of downcasting in the code.
See http://www.javaspecialists.eu/archive/newsletter.do?issue=123&print=yes&locale=en_US for details.

new solver added which uses PBSolverClause.
PBSolverClause : pb-constraints can be reduced to clause during resolution

replacing BigInteger by long

Changed the implementation (the reference is now shared using a static field).

Made access to vocabulary through static method in Solver: should save a lot of memory (4 bytes per constraint).

Added latest files from Anne's email.

Added Rsat like heuristics in default solver.

Added Rsat like heuristics in VarOrderHeapRsat

Changed MAX SAT solver paprameter: restarts starts at 100 000 conficts now.

Removed unused import.

Changed default solver for MAXSAT solving.

Fixed copyright headers and indentation/format (asked by Dieter).

warning suppressed

Useless ConflictArray* classes and subsequent classes have been deleted

Added missing getter and setters for command line configuration.

Fixed Javadoc comments.

Added back learning to PB solver.

Removed expensive simplification for PB solvers with resolution.

Added Expensive Simplification to all PB solvers.

ajout d'un solveur
newMiniLearningOPBClauseCardConstrMaxSpecificOrderIncremental

newMiniLearningOPBClauseCardConstrMaxSpecificOrder appelle PBSolverMapInitial par d?faut

Fixed memory problem.
Decoding the model directly in a PrintWriter.

nouveaux solveurs crŽŽs pour utiliser les diffŽrentes versions d'isAssertive()

Added a resolution based solver.

Moved DimacsOutput solver to org.sat4j.tools.

Made MiniLearningHeapEZSimp the default solver.

Added text output solver.

Made MiniLearningHeapEZSimp solver as default SAT solver.

Made SATRace2006 the default solver.

Added a new solver for the SAT race.

Fixed (again) singleton design pattern.

Fixed Singleton design pattern.

Removed SATRace decorator as default solver.

Added SATRaceDecorator.
Fixed launcher: usage displayed when no arguments are given.

Fixed JavaDoc comment.

Removed Expensive simplification code.

Ajout d'une heuristique prenant en compte la fonction objectif.

Fixed some Findbugs warnings.

Fixed many pmd warnings.

new solver added to use the new datastructure factory (with MinWatchPB, MinWatchCard and WLClause)

Made MiniLearningHeapEZSimp the default solver.

*** empty log message ***

Using the best version of MiniLearning for the No Restarts solver.

more precise comments are added.

merged with PBCONSTR

merge with HEAD branches is done

added 2 new solvers.

new solver to use the new datastructure

AP :
added a new solver 
- whith the pseudo-boolean solver with implied clauses
- with counter pb-constraints, watched cards and watched clauses

AP : new solvers have been added to use the new data structure factories.

Forgot to make the new methods static.

Added two static methods to easily access both default and light solver:
SolverFactory.newDefault()
SolverFactory.newLight()

Using SolverFactory as a singleton.

AP :
- attention : code temporaire, encore boguŽ! 
- crŽation d'une DataStructureFactory qui crŽŽ des PBconstr qui sont des clauses, des cardinalitŽs ou des PB-contraintes, suivant le cas;
- crŽation d'un solveur spŽcifique et des tests correspondants;
- spŽcial FrŽdŽric : lŽg�res modifs dans MapPb (mŽthode cuttingPlane peut �tre appelŽe avec le param�tre reducedCoefs null, suppression de l'introspection

Changed delay for memory checking.
Added solvers with full simplification.

Added new prebuilt solver: MiniSATHeapEZSimp

AP : modification du calcul des watched literals : proposition de Pueblo

Use Heap based heuristics in PB solvers. The solvers are almost twice as fast now.

Added new SAT to CSP translator.
Moved all CSP stuffs in a separate package.

Fixed code to mimic exactly RELEASE 1.5

Java 1.5 code base including some code from ubcsat port.

Back to OW2 Forge