clasp-3.2.0

clasp is an answer set solver for (extended) normal and disjunctive logic programs. Its primary algorithm relies on conflict-driven nogood learning, a technique that proved very successful for satisfiability checking (SAT). clasp is distributed under the GNU Public License and can also be applied as a SAT or a PB solver (on OPB format).

Below you can find a list of new features introduced in the current release. Please also consult the following files and directories of the release:

• CHANGES: Major changes between versions
• README : Installation instructions and requirements
• doc/ : Doxygen generatable source code documentation

For further information and downloads, please visit http://potassco.sourceforge.net/

What's New in version 3.2.0

Input & Output

• Support for the new asp intermediate format aspif
• Option --pre now takes an optional argument to force aspif format
• New option --parse-ext for enabling parsing of aspif extensions given
  • in the symbol table of Smodels input:
    • acyclicity constraint via _edge or _acyc_ predicate
    • domain heuristic via _heuristic predicate
  • in comment lines of Dimacs/OPB input:
    • acyclicity constraint via a graph/endgraph block as produced by lp2sat -g
    • domain heuristic via heuristic <type> <var> <bias> <prio> <lit_or_0>
    • #project-directive via project <var>...
    • #assumption-directive via assume <lit>...
    • #output-directive via output <lit> <string> (print <string> if <lit> is true in model)
    • #output range via output range <var_first> <var_last>
    • only in Dimacs: minimize constraint via minweight <lit>... 0
• Configurations in portfolio files can now extend an existing configuration by using
  • <name>(<config>): <options>, where <config> is one of clasp's predefined configurations
• Lemma logging via option --lemma-out now resolves lemmas to problem variables (and discards those for which this is not possible)
  • New option --lemma-out-dom for setting variable domain to either input or output variables
  • New option --lemma-out-txt for switching from aspif to ground text format
  • New option --lemma-out-max for limiting number of logged lemmas

Search

• Stratification heuristic for weights in core-guided optimization enabled via --opt-strategy=usc,<x = n|8>
• Average conflict-index decision scoring in vsids via option -vsids-acids
• Some search features from the glucose SAT Solver
  • decreasing decay scheme via option --vsids-progress
  • blocking of restarts via option --block-restarts
  • temporary freezing of learnt nogods via option --del-protect
• New default configuration for tester solvers in disjunctive asp solving
• New propagator for handling acyclicity constraint (#edge-directive)

Developer & Miscellaneous

• New library liblp for reading/writing aspif and for converting from and to smodels-format
• New iterative solve function for synchronous model generation that does not require threads
• Optional support for parallel solving via C++11 threads instead of Intel TBB library
• Support for updates of heuristic options (like --init-moms, --score-res, --dom-mod) in multishot solving
• Option --nant now also applies to lookback heuristics
• Option --dom-mod now supports modifiers factor and init and also applies to Dimacs/OPB problems
• New option --sign-def-disj for setting the default sign for atoms in disjunctions
  • Note: The old way of forcing true via --sign-def=4 is no longer supported
• Improved handling of extended rules in computation of loop nogoods
• Improved handling of equivalent and complementary atoms in domain heuristic
• Lock-free updates of lower bounds in parallel optimization
• More compact representation of input facts in smodels-format
• Many new interfaces and changes to internal interfaces to ease integration within clingo

Remarks

• The new search options are not yet used in clasp's predefined configurations
• The restructuring of (internal) interfaces is work in progress and currently tightly coupled to the evolution of clingo-5
• The goal of the new updated lemma logging is to eventually make xclasp obsolete