What's new in clasp 3.3.2
Feb 23, 2018
- Fixes:
- missing lower bound output in unsat-core optimization for bounds < 0
- conflict clauses not always tagged with assumptions in unsat-core optimization
- invalid reallocation of vector during theory propagation
- Issue potassco/clingo#45
- Issue #10
- workaround for bug #81365 in gcc 7.1 (https://gcc.gnu.org/bugzilla/show_bug.cgi?id=81365)
- support for <EOL> as terminator for minweight constraint in dimacs input
New in clasp 3.0.6 (Jul 22, 2014)
- fixed: parallel unsat-core based enumeration of optimal models could skip valid models
- fixed: possible race condition in signal handling
- fixed: ABA-problem in parallel cb-enumerator could lead to duplicate models (regression in 3.0.x)
- fixed: "--share=auto" (default) failed to enable physical sharing in mt-mode (regression in 3.0.x)
- fixed: eq over complementary atoms not always correctly handled (regression in 3.0.x)
- fixed: incremental domain heuristic failed to apply values to atoms from previous steps
- fixed: eq over bodies of size 1 not always correctly handled
- fixed: typo in description of "--quiet"
New in clasp 3.0.5 (May 20, 2014)
- removed pointless "--del-init" option from config tweety
- fixed: non-hcf components not always correctly added in incremental disjunctive programs (clingo)
- fixed: empty soft clauses not correctly handled in MaxSAT frontend
- fixed: unfounded sets from 2nd level test not always correctly handled
- fixed: json output must not print NaN
- fixed: asp options not correctly set on configuration update (from clingo)
- fixed: regression in handling of (incremental) projection
New in clasp 3.0.4 (Apr 24, 2014)
- replaced "s SATISFIABLE" with "s UNKNOWN" when called with option "--opt-sat"
- improved handling of weight constraints containing incremental assumptions
- fixed: typo in output of "--help"
- fixed: unsatisfiable-core based optimization sometimes fails to assign all active assumptions
- fixed: superfluous rules for facts not always correctly handled
- fixed: assigned values for external atoms not always carried over to next step
- fixed: clasp sometimes fails on incremental problems if "--lookahead" is used with "--forget-on-step"
New in clasp 3.0.3 (Mar 29, 2014)
- fixed: AsyncResult destructor fails if called after destruction of ClaspFacade
- fixed: projective enumeration sometimes fails when used with option "--restart-on-model"
- fixed: regression in handling of negative lower bound in optimization
New in clasp 2.1.4 (Nov 27, 2013)
- Fixed a possible crash bug in handling of conditional constraints
- Fixed a regression in handling of physically shared clauses
New in clasp 2.1.3 (Apr 13, 2013)
- fixed a regression in the handling of choice rules in the unfounded set checker
New in clasp 2.1.1 (Mar 18, 2013)
- fixed regression: MaxSAT-frontend must not assert pure literals / relaxation variables
- fixed: spurious warning when using option "--no-lookback"
- fixed: "--shuffle" and "--counter-restarts" not working as intended with hierarchical optimization
- fixed: Backslashes in JSON output not correctly quoted
New in clasp 2.1.0 (Mar 18, 2013)
- restructured help and revised options and their defaults
- added "--help[={1..3}]" for showing basic, advanced, or all options
- added "--configuration" for selecting between prefabricated default configurations
- revised deletion options and grouped them via common prefix "--del-"
- revised thread options and added options for size-/topology-based lemma exchange
- added support for dynamic restarts via "--restarts=D,"
- added "--sign-def" for setting default sign used in decision heuristic * added "--sign-fix" for disabling sign-heuristic
- added "--init-moms" for enabling/disabling initialization of heuristic with MOMS-score
- added "--fast-exit" for forcing app exit without cleanup
- added "--update-act" for enabling LBD-based activity bumping
- added "--update-mode" for configuring when update/integrate messages are handled in parallel-search
- added "--learn-explicit" to disable usage of implication graph for learnt constraints * added "--share" for configuring physical constraint sharing
- added "--init-watches" for controlling initialization of watched literals
- added "--counter-restarts" and "--counter-bump" for enabling counter implication restarts
- added "--lemma-out-lbd" for restricting lemmas written via "--lemma-out"
- added "--lemma-in-lbd" for setting initial lbd of lemmas read via "--lemma-in"
- replaced "--loops-in-heu" with more general "--score-other"
- replaced "--rand-watches" with more general "--init-watches"
- replaced "--initial-lookahead" with "--lookahead=[,]"
- replaced "--recursive-str" with "--strengthen=[,]"
- replaced "--copy-problem" with more general "--share"
- removed options "--brave", "--cautious", "--solution-recording": all superseded by "--enum-mode="
- option "--restarts" now always requires a type; and the "limit" parameter now sets the (initial) length of the sequence
- disbaled signal handling during printing of models
- fixed: Overflow on parsing large opt-values (issue 3528852)
- fixed: Parallel bt-enumerator enumerated duplicate models under certain conditions
- fixed: Sat-Preprocessor failed to expand models correctly under very rare conditions
- fixed: Erroneous interplay between "otfs=2" and "reverse-arcs" could lead to the unjustified removal of problem constraints
- fixed: Incorrect ordering-predicate in MinimizeConstraint could lead to wrong optima
- fixed: Solve loop failed to handle restart on total assignment correctly resulting in an infinite loop on some optimization problems
- fixed: Duplicate key in JSON-Output of lemma stats
New in clasp 2.0.6 (Mar 18, 2013)
- added better error detection to portfolio parser and fixed a bug in the initialization of thread configs
- first attempt at decoupling learnt db growing from restart schedule using independent grow schedule configurable via (hidden) option "--dgrowS"
- added "--update-lbd=2" to enable usage of "strict" lbds
- added (experimental) support for counter implication restarts and dynamic restarts via hidden options
- fixed bugs in code for shared clause integration that could led to unpleasant results ranging from duplicate/missing models in enumeration to crashing if option "--otfs" was used
New in clasp 2.0.5 (Mar 18, 2013)
- fixed: Input parser for opb and (w)cnf failed to read 64bit integers.
- fixed: Outer bound of inner-outer-restarts sometimes remained constant because of integer arithmetic.
- fixed: Minimize constraint must not update optimum in enumeration-mode (opt-all). Bug introduced in version 2.0.3
- fixed: Minimize constraint must not update initial (user-set) bound until a model is found. Bug introduced in version 2.0.3
- fixed: Right hand side of minimize constraint not correctly initialized if "--opt-hierarch" was used.
- fixed: SharedMinimizeData assumed monotonicity of individual levels - could fail after merging complementary literals in multi-level minimize constraints. Added extra "adjustment"-values to represent values resulting from such merges.
New in clasp 2.0.4 (Mar 18, 2013)
- some cleanup in help output;
- moved general ASP-specific options to separate group
- moved "--opt-sat" to basic options
- simplified default command-line and made "input-dependent" defaults more explicit
- updated interface spec of ProgramBuilder to make it more robust w.r.t incremental update * fixed parsing of "--global-restarts"
- fixed: default value for option "--rand-watches" was not applied
- fixed: Enumerator did not broadcast last model/optimum of current GP in parallel search
- fixed: clauses simplified to binary/ternary are no longer counted twice in stats
- fixed: eq-preprocessor sometimes did not reorder head list after merging two bodies
- fixed: dimacs front-end failed to read empty dimacs file