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.

Release Notes - Sat4j - Version 2.3.1 <h2> Bug </h2> <ul> <li>[<a href='http://jira.ow2.org/browse/SAT-8'>SAT-8</a>] - Allow iterating over optimal solutions </li> <li>[<a href='http://jira.ow2.org/browse/SAT-14'>SAT-14</a>] - After a call to expireTimeout(), a solver cannot be relaunched </li> <li>[<a href='http://jira.ow2.org/browse/SAT-16'>SAT-16</a>] - Order of added constraints affects the results of RemiUtils </li> <li>[<a href='http://jira.ow2.org/browse/SAT-17'>SAT-17</a>] - Problem with isSatisfiable(VecInt) </li> <li>[<a href='http://jira.ow2.org/browse/SAT-18'>SAT-18</a>] - ISolver.isSatisfiable(VecInt) is affected by previous call </li> <li>[<a href='http://jira.ow2.org/browse/SAT-21'>SAT-21</a>] - Error in method toString() of OPBStringSolver for negative literals </li> <li>[<a href='http://jira.ow2.org/browse/SAT-26'>SAT-26</a>] - After adding and removing a clause in Xplain, subsequent addition of the clause are ignored </li> <li>[<a href='http://jira.ow2.org/browse/SAT-27'>SAT-27</a>] - PMaxSAT Solving </li> <li>[<a href='http://jira.ow2.org/browse/SAT-29'>SAT-29</a>] - Mus computation does not work when input file contains duplicated contiguous clauses (aka MUS competition bug) </li> <li>[<a href='http://jira.ow2.org/browse/SAT-32'>SAT-32</a>] - Tautological PB constraints with no literals incorrectly considered asempty clauses </li> <li>[<a href='http://jira.ow2.org/browse/SAT-35'>SAT-35</a>] - LexicoHelper constructors are incorrect when explain option is set to true </li> <li>[<a href='http://jira.ow2.org/browse/SAT-37'>SAT-37</a>] - Unit clauses not propagated again when doing multiple calls to the SAT solver </li> <li>[<a href='http://jira.ow2.org/browse/SAT-40'>SAT-40</a>] - Random Walk Decorator disable Objective Function based heuristics </li> <li>[<a href='http://jira.ow2.org/browse/SAT-66'>SAT-66</a>] - Incorrect explanations in PB </li> </ul> <h2> Improvement </h2> <ul> <li>[<a href='http://jira.ow2.org/browse/SAT-11'>SAT-11</a>] - Allow creation of ManyCore solver from a list/array of existing solvers instead of their name in a factory </li> <li>[<a href='http://jira.ow2.org/browse/SAT-12'>SAT-12</a>] - Use List instead of IVec in DependencyHelper.getSolution() </li> <li>[<a href='http://jira.ow2.org/browse/SAT-15'>SAT-15</a>] - Allow to reset the DependencyHelper </li> <li>[<a href='http://jira.ow2.org/browse/SAT-34'>SAT-34</a>] - Make sure that all solvers return a unit clause in addClause </li> <li>[<a href='http://jira.ow2.org/browse/SAT-39'>SAT-39</a>] - Add the possibility to create a constraint k among n in IProblem </li> <li>[<a href='http://jira.ow2.org/browse/SAT-41'>SAT-41</a>] - Use a specific data structure to locate efficiently the weight associated to a literal in a counter based constraint </li> <li>[<a href='http://jira.ow2.org/browse/SAT-42'>SAT-42</a>] - Allow Sat4j to use bunzip2 to uncompress on the fly bz2 (and possibly others) compressed files </li> <li>[<a href='http://jira.ow2.org/browse/SAT-43'>SAT-43</a>] - Allow the solver to be aware of the user defined max var id </li> <li>[<a href='http://jira.ow2.org/browse/SAT-45'>SAT-45</a>] - Separate MS and PWMS decorator from the optimization method </li> </ul> <h2> New Feature </h2> <ul> <li>[<a href='http://jira.ow2.org/browse/SAT-3'>SAT-3</a>] - Allow computation of prime implicants instead of models </li> <li>[<a href='http://jira.ow2.org/browse/SAT-10'>SAT-10</a>] - allow ability to clone a solver </li> <li>[<a href='http://jira.ow2.org/browse/SAT-31'>SAT-31</a>] - Add the ability to add weighted objective function to LexicoHelper </li> <li>[<a href='http://jira.ow2.org/browse/SAT-44'>SAT-44</a>] - add lower bound optimization strategy </li> </ul>