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

Request diff between arbitrary revisions / Display revisions graphically

added explanation at root level

back to preceeding version for ISolver interface.
explanations concern only pb-part now

added simple explanation for unsatisfiability

Fixed NPE.

Added a deterministic timeout based on the number of conflicts.

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

Added a new method in IProblem to allow the solver to return informations specific to a given problem.

Removed dependencies to Iterable.

Replaced StringBuilder by StringBuffer.

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.

Allow the isSatisfiable method to be called within a global timeout.

* new method expireTimeout for ISolver
* made Solver.underTimeout volatile in order to allow for
  modification from other Threads

Improved message for the timeout setting.

The solver nows display its internal timeout.

Fixed a few warnings.

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

Fixed many warnings.

Fixed typos in the javadoc comments (thanks Eclipse Europa :)).

Removed remaining restart framework debug display.

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

Removed assertion in Solver that was adding a dependency to constraints.cnf

Fixed PMD warnings.

Fixed findbugs warnings when necessary.
Added a comment DLB findbugs ok is the code is ok and the warning can be safely ignored.

Allows command line configuration of the restarts strategy.

Using luby style restarts by default.

Uses Armin Biere restart strategy.

Fixed number of decision stats.

Added a Restart strategy to test Armin Biere and Luby style restart strategies.

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).

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

Fixed NPE in regression tests.

Added Rsat like heuristics in VarOrderHeapRsat

Fixed assertions in Exp and Easy simplifications.

Removed commented lines.

Fixed FB warnings.

Made clear that reason simplification cannot because used with anything else than WL clauses.

Fixed PMD warnings.

Added back conflict based timer. Removed explicit call to GC.

Removed Conflict-based Timer.

Do memory checks every 500 conflicts.

Replace integer operation by a long operation in setTimeout(int)

Made ConflictTimer serializable.

Preliminary support for external reasons for backtracking.

Do memory checkup every 100 conflicts.

added time-independant memory management. The solver should be 100% deterministic now.

Added possibility to assign timeout in ms.

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

Added even more comments (classes + enum).

Fixed notification for wrong component property name.

Added support for modifying searchparams on the command line.

Fixed setSimplification method.

Added support for simplification.

Fixed problem with DimacsOutput.

Fixed PMD warnings.

Fixed findbugs warnings.

Fixed Class Cast exeption (Java generics limitation).

Tried to improve further the SAT solver (propagate, analyze,etc).

Tried to improve further the SAT solver (propagate, analyze,etc).

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

Ready for the internal evaluation.

Fixed Findbugs problems.
Changed a few things in Predicate.

Added back one call to c.setLearnt()

Removed minlevel in Expensive Simplification.

Added new WLClause subclasses in order to save memory when using large clauses.

The simplification is now exactly the one in MiniSAT 1.14.

Fixed ExpensiveSimplification.

Removed level abstraction in expensive simplification.

Added a method to clear learnt clauses.

Added a new method in IProblem, feature request from Chris Tucker.

Merged fixes from 1.6 branch.

Fixed properly the AtMost problem.

The solver now takes into account the expected number of clauses to fix constrs initial size.

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

Removed Expensive simplification code.

Fixed many pmd warnings.

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

a "protected" forgotten on addConstr() method

merged with PBCONSTR

merge with HEAD branches is done

AP : some methods are now protected

Fiwed assertion in ExpSimplification.
Added guard verifications in model.

Fixed the way the clauses were cleaned.

Fixed NLS problems.
Added Emina new methods in IProblem and ISolver interfaces.
Removed displayResults() in Launcher.

Add a start and an end method in the SearchListener interface.
The Solver class is changed in concequence. (call the start and the end method)

Removed some warnings and commented code.

ExpSimp related modifications (but still incorrect)..

Maybe a fix for expensiveSimplification?

Simplified reduceDB.

Removed call to simplifyDB() in solver, because it breaks the single solution test.

Fixed stats display.

Removed @SuppressWarning("serial")

The interface LearningStrategy is currently Serializable

Added a new feature: Max satisfiability!

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 PrintStream by PrintWriter in abstract launcher.
The ISolver.printStat(PrintStream,prefix) is now deprecated.
One should use ISolver.printStat(PrintWriter,prefix) instead.

AP : suite remarques FrŽdŽric

Fixed a few PMD warnings.

AP : version de travail vendredi 10 mars...

Fixed maybe a problem in Expensive Simplification.

Fix problem of reduceDB is another thread!!!

Fixed a problem in Expensive simplification.

Added stats on removed literals.

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

Added log message to be sure that memory management is done correctly.

Fixed the causes cleanup: the test was only done once. Now it is really done every 30s.

Fixed cleanup timer to really 30s (and not 300s!!!).

New clause cleanup policy.

The solver now cleanup the clauses each time it restarts. The problem is that cleanup and restarts are currently tight together. They should be independent.

Corrected bug in Solver.modelFound() discovered thanks to the changes in Lits.

Fixed CSP3 encoding. Unfortunately, now the encoding is really slow.
Some improvements is needed (avoiding creating too many objects for instance).

Fixed a bug in BinarySupportACEncoding. There is still one in GeneralizedSupportACEncoding.

Added a decorator to detect a single solution.

Fixed some problems detected by PMD.

Fixed code to mimic exactly RELEASE 1.5

Java 1.5 code base including some code from ubcsat port.

Back to OW2 Forge