CVS log for sat4j/core/src/org/sat4j/minisat/constraints/pb/Attic/PBSolver.java
	Help

Request diff between arbitrary revisions / Display revisions graphically

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.

Using Rapid restarts strategy.

Using normal restart strategy with PBSolver.

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.

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

Bug in PB-code fixed.

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

Rolled back to MapPB.

Uses an array for cutting planes operations.

Replaced conditional by assertions (noticed with clover).

Fixed string displayed.

Added precise information about inference scheme.

PBSolver utilise ConflictMap

PBSolver appelle par d?faut ConflictMapInitial

3 versions de isAssertive() et getBacktrackLevel().

PŠr dŽfaut, PBSolver appelle ConflictMap, qiu est une version completement incrŽmentale de isAssertive() et getBacktrackLevel()

pour faire des tests sur les diffŽrentes propositions pour isAssertive(), quatre nouvelles classes :
- ArrayPBInitial et ConflictArrayInitial : 
proposent les versions classiques (non incrŽmentales) pour isAssertive() et getBacktracklevel()
- ArrayPbIncrementEtParcours et ConflictArrayIncrementEtParcours :
proposent une version incrŽmentale pour isAssertive() et non incrŽmentale pour getBacktrackLevel().

c'est ConflictArrayIncrementEtParcours qui est choisi par dŽfaut dans PBSolver

isAssertive() est incrŽmental mais getBacktrackLevel() ne l'est plus.

une premiere version (presque) incrŽmentale de isAssertive(int decisionLevel)

PBSolver is using ConflictArray (and not ConflictMap).

Added heuristics incrementation as in the SAT solver.

Made MapPb and MapConflict the default implementation in PBSolver.

Fixed many pmd warnings.

Added comments to check that the solvers are using the expected components.

merged with PBCONSTR

2 new solvers are added : PBSolverClause and PBSolverCard
which reduce, respectively, to clause and to cardinality constraints involved in a conflict.

AP : 
- code cleaning in IDataStructurePB hierarchy
- AtLeastPB extends AtLeast and implements PBConstr. Can be learned

AP : 
- ConflicTab renamed in ConflictArray
- unused method removed in MinWatchCardPB

AP : ArrayPb used instead of MapPb

AP :
- Il y a maintenant une interface et deux classes d'implementation pour MapPb et Conflict : l'une basŽe sur un tableau, l'autre sur un HashMap

Removed @SuppressWarning("serial")

The interface LearningStrategy is currently Serializable

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

AP : suppression d'une var. locale inutile dans analyze()

Fixed issues with unremovable learnt pseudo boolean constraints. It is just a workaround for now: constraints removal is sort of "disabled" right now.

Fixed some problems detected by PMD.

Java 1.5 code base including some code from ubcsat port.

Back to OW2 Forge