Advanced - Powered by Google

Log In
New Account

The services provided by this GForge instance will stop on Jun/30. Please have a look at the information notice for more information

My Page
Project Tree
Project Openings
Posted By: Daniel Le Berre
Date: 2011-10-30 12:05
Summary: Sat 4j 2.3.1 released

The Sat4j team is proud to announce the release of a new version of its boolean satisfaction and optimization library. The main focus of that release is to fix the bugs found since the release of Sat4j 2.3.0. That release also contains some internal changes in the architecture to allow more flexibility and new usage of the library. Those changes should not affect users at the API level but may affect advanced users of the library (parallel solving, custom constraints, etc). All those changes are listed in the release notes.

We strongly encourage all Sat4j users to upgrade to that new release, unless their code is depending on Sat4j internals.

Release Notes - Sat4j - Version 2.3.1

** 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

** 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-31] - Add the ability to add weighted objective function to LexicoHelper
* [SAT-44] - add lower bound optimization strategy

Latest News
Joram 5.15 is released
    Andre Freyssinet - 2018-05-04 10:58
Joram 5.15 is released
    Andre Freyssinet - 2018-05-04 10:58
ASM 6.1 released
    Eric Bruneton - 2018-03-11 10:25
XWiki Release announcement moved
    Vincent Massol - 2018-02-26 16:34
ASM 6.1-beta released
    Eric Bruneton - 2018-01-06 15:03

Discussion Forums: Sat 4j 2.3.1 released

Start New Thread Start New Thread | Admin


Topic Topic Starter Replies Last Post

Copyright © 1999-2008, OW2 Consortium | contact | PS: You have a difficulty, a problem ? Please report an issue using your main OW2 account credentials