Release Notes - Sat4j - Version 2.3.1 - HTML format

Bug

  • [SAT-8] - Allow iterating over optimal solutions
  • [SAT-14] - After a call to expireTimeout(), a solver cannot be relaunched
  • [SAT-16] - Order of added constraints affects the results of RemiUtils
  • [SAT-17] - Problem with isSatisfiable(VecInt)
  • [SAT-18] - ISolver.isSatisfiable(VecInt) is affected by previous call
  • [SAT-21] - Error in method toString() of OPBStringSolver for negative literals
  • [SAT-26] - After adding and removing a clause in Xplain, subsequent addition of the clause are ignored
  • [SAT-27] - PMaxSAT Solving
  • [SAT-29] - Mus computation does not work when input file contains duplicated contiguous clauses (aka MUS competition bug)
  • [SAT-32] - Tautological PB constraints with no literals incorrectly considered asempty clauses
  • [SAT-35] - LexicoHelper constructors are incorrect when explain option is set to true
  • [SAT-37] - Unit clauses not propagated again when doing multiple calls to the SAT solver
  • [SAT-40] - Random Walk Decorator disable Objective Function based heuristics
  • [SAT-66] - Incorrect explanations in PB

Improvement

  • [SAT-11] - Allow creation of ManyCore solver from a list/array of existing solvers instead of their name in a factory
  • [SAT-12] - Use List instead of IVec in DependencyHelper.getSolution()
  • [SAT-15] - Allow to reset the DependencyHelper
  • [SAT-34] - Make sure that all solvers return a unit clause in addClause
  • [SAT-39] - Add the possibility to create a constraint k among n in IProblem
  • [SAT-41] - Use a specific data structure to locate efficiently the weight associated to a literal in a counter based constraint
  • [SAT-42] - Allow Sat4j to use bunzip2 to uncompress on the fly bz2 (and possibly others) compressed files
  • [SAT-43] - Allow the solver to be aware of the user defined max var id
  • [SAT-45] - Separate MS and PWMS decorator from the optimization method

New Feature

  • [SAT-3] - Allow computation of prime implicants instead of models
  • [SAT-10] - allow ability to clone a solver
  • [SAT-31] - Add the ability to add weighted objective function to LexicoHelper
  • [SAT-44] - add lower bound optimization strategy

Edit/Copy Release Notes

The text area below allows the project release notes to be edited and copied to another document.