clasp version 3.3.4

@BenKaufmann BenKaufmann released this Jun 27, 2018

Changes

  • Added internal interface for user-defined statistics
    (#23)
  • Extended ClingoPropagatorInit to support both global and per-solver watches.

Fixes

  • #22
  • #16
  • #18
  • #33
  • #34
  • Possible infinite loop in detection of problem type from input.
  • Atoms of incremental programs not always marked as frozen.

Note

The source code archives provided by github do not contain the libpotassco submodule. Please download
clasp-3.3.4-source.tar.gz for a complete source archive.

This release does not contain any clasp binaries. Prebuilt binaries of clasp are part of new
clingo releases.

clasp version 3.3.3

@BenKaufmann BenKaufmann released this Nov 5, 2017 · 21 commits to master since this release

Fixes

  • possible race condition in Windows alarm handling (libpotassco)
  • state not fully reset in incremental acyc check
  • facade progress state not reset after solving step
  • Issues #11 #12 #13

Note on source code archives

The source code archives provided by github do not contain the libpotassco submodule. Please download
clasp-3.3.3-source.tar.gz for a complete source archive.

Note on binaries

This release does not contain any clasp binaries. Prebuilt binaries of clasp-3.3.3 can be found in
clingo version 5.2.2.

clasp version 3.3.2

@BenKaufmann BenKaufmann released this Jul 29, 2017

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

clasp version 3.3.0

@BenKaufmann BenKaufmann released this Apr 28, 2017

New

  • switched to MIT license
  • added support for unsatisfiable core shrinking via option --opt-usc-shrink
  • added support for core-guided optimization algorithms K and ONE
  • removed dependency to Intel TBB (multithreading now only uses C++11 threads)

CLI changes:

  • changed syntax of option --opt-strategy (old syntax is still supported but deprecated)
    • First argument selects the overall strategy, i.e. model- or core-guided optimization
    • Second argument selects the algorithm, e.g. K or OLL for core-guided optimization
    • Further arguments enable additional tactics, e.g. "disjoint" for disjoint core
      preprocessing in core-guided optimization
  • option --pre now prints aspif by default (use --pre=smodels for smodels)
  • merged option --opt-bound into --opt-mode
  • merged option --counter-bump into --counter-restarts
  • replaced option --opt-sat with --parse-maxsat
  • merged option --dist-mode into --distribute
  • merged option --del-protect into --update-lbd
  • replaced numbers with named constants in various options
  • added support for specifying bitmask arguments as list of named constants, e.g.
    --forget-on-step=varScores,signs,lemmaScores instead of --forget-on-step=7

Integration/clingo:

  • switched to CMake for building clasp
  • moved libprogram_opts to libpotassco, which is now a submodule of clasp
  • added support for step-specific true var to simplify implementation of multishot propagators
  • simplified ClaspFacade solving interface

clasp version 3.2.3

@BenKaufmann BenKaufmann released this Apr 24, 2017 · 298 commits to master since this release

Fixes

  • possible crash on Cygwin because of non-increasing wall clock time
  • PB constraints not correctly initialized if added on decision levels > 0
  • spurious backtracking on integrating sat clauses from theory propagator
  • regression: unsupported atoms in minimize statements not added to program
  • regression: complementary atoms not correctly handled in enum mode domRec
  • regression: model heuristic (--opt-heuristic=2) not applied

clasp version 3.2.2

@BenKaufmann BenKaufmann released this Jan 23, 2017 · 310 commits to master since this release

News

  • experimental support for MiniCard's CNF+ format
  • stats key "summary.winner" for getting id of winner thread from clingo

Fixes

  • regression in sat/pb reader
  • regression in handling of unsatisfiable optimization problems
  • regression in component-wise shifting and preprocessing of disjunctive rules
  • ClaspFacade::startSolve() could produce duplicate and/or miss models
  • failed to handle empty clauses added from theory propagator
  • invalid logged lemmas due to buggy minimization in Solver::resolveToFlagged()
  • LogicProgram::dispose() must reset pointers
  • compilation problems on Cygwin and Alpha

clasp version 3.2.1

@BenKaufmann BenKaufmann released this Oct 13, 2016 · 328 commits to master since this release

  • added support for adding variables from theory propagator
  • fixed output of "--pre" wrt to externals in incremental setting
  • fixed regression in projective enumeration in incremental setting
  • fixed regression in handling of minimize statements containing only zero-weighted literals
  • fixed possible invalid access to empty input vector in ClaspAppBase::run()
  • added workaround to fix emcc code-gen bug
  • fixed type mismatch and warnings when compiled with x64 and _DEBUG
  • fixed compilation problems on MacOS and ARM