clasp is an answer set solver for (extended) normal and disjunctive logic programs. It is part of the Potassco project for Answer Set Programming (ASP). The primary algorithm of clasp relies on conflict-driven nogood learning, a technique that proved very successful for satisfiability checking (SAT). clasp has been genuinely developed for answer set solving but can also be applied as a (Max-)SAT or PB solver or as a C++ library in another program. It provides different reasoning modes and other advanced features including:
- Enumeration and Optimization of (Projected) Solutions,
- Cautious and Brave Reasoning,
- Advanced Disjunctive Solving,
- Parallel (multithreaded) solving,
- Domain heuristic modifications,
- Unsatisfiable-core based optimization,
- ASP/SAT/PB modulo acyclicity,
- Different input formats including smodels, aspif, dimacs and opb.
Detailed information (including a User's manual), source code, and pre-compiled binaries are available at: http://potassco.org/
clasp is distributed under the MIT License.
See LICENSE for details regarding the license.
LICENSE - The MIT License CHANGES - Major changes between versions README.md - This file CMakeLists.txt - Configuration file for building clasp with CMake cmake/ - Module directory for additional CMake scripts app/ - Source code directory of the command-line interface clasp/ - Header directory of the clasp library src/ - Source code directory of the clasp library tests/ - Unit tests of the clasp library examples/ - Examples using the clasp library libpotassco/ - Directory of the potassco library tools/ - Some additional files
BUILDING & INSTALLING
The preferred way to build clasp is to use CMake version 3.1 or later together with a C++ compiler that supports C++11.
The following options can be used to configure the build:
CLASP_BUILD_APP : whether or not to build the clasp application CLASP_BUILD_TESTS : whether or not to build clasp unit tests CLASP_BUILD_EXAMPLES : whether or not to build examples CLASP_BUILD_WITH_THREADS: whether or not to build clasp with threading support (requires C++11)
For example, to build clasp in release mode in directory
cmake -H. -B<dir> cmake --build <dir>
To install clasp afterwards:
cmake --build <dir> --target install
To set the installation prefix, run
cmake with option
Finally, you can always skip installation and simply copy the clasp executable to a directory of your choice.
A User's Guide is available from http://potassco.org/
Source code documentation can be generated with Doxygen. Either explicitly:
cd libclasp/doc/api doxygen clasp.doxy
or via the
doc_clasp target when using cmake.
clasp reads problem instances either from stdin, e.g
cat problem | clasp
or from a given file, e.g
to get a basic overview of options supported by clasp or
for a more detailed list.
In addition to printing status information, clasp also provides information about the computation via its exit status. The exit status is either one or a combination of:
0 : search was not started because of some option (e.g. '--help') 1 : search was interrupted 10 : problem was found to be satisfiable 20 : problem was proved to be unsatisfiable
Exit codes 1 and 11 indicate that search was interrupted before the final result was computed. Exit code 30 indicates that either all models were found (enumeration), optimality was proved (optimization), or all consequences were computed (cautious/brave reasoning). Finally, exit codes greater than 32 are used to signal errors.