1# clasp 2 3clasp is an answer set solver for (extended) normal and disjunctive logic programs. 4It is part of the [Potassco](https://potassco.org) project for *Answer Set Programming* (ASP). 5The primary algorithm of clasp relies on conflict-driven nogood learning, 6a technique that proved very successful for satisfiability checking (SAT). 7clasp has been genuinely developed for answer set solving but can 8also be applied as a (Max-)SAT or PB solver or as a C++ library in another program. 9It provides different reasoning modes and other advanced features including: 10 11 - [Enumeration][enum] and [Optimization][opt] of ([Projected][proj]) Solutions, 12 - Cautious and Brave Reasoning, 13 - [Advanced Disjunctive Solving][claspD2], 14 - [Parallel (multithreaded) solving][claspmt], 15 - [Domain heuristic][hclasp] modifications, 16 - [Unsatisfiable-core based optimization][unclasp], 17 - [ASP/SAT/PB modulo acyclicity][acyc], 18 - Different input formats including [smodels][smodels], [aspif][aspif], [dimacs][dimacs] and [opb][opb]. 19 20Detailed information (including a User's manual), source code, 21and pre-compiled binaries are available at: http://potassco.org/ 22 23## LICENSE 24 clasp is distributed under the MIT License. 25 26 See LICENSE for details regarding the license. 27 28## PACKAGE CONTENTS 29 LICENSE - The MIT License 30 CHANGES - Major changes between versions 31 README.md - This file 32 CMakeLists.txt - Configuration file for building clasp with CMake 33 cmake/ - Module directory for additional CMake scripts 34 app/ - Source code directory of the command-line interface 35 clasp/ - Header directory of the clasp library 36 src/ - Source code directory of the clasp library 37 tests/ - Unit tests of the clasp library 38 examples/ - Examples using the clasp library 39 libpotassco/ - Directory of the potassco library 40 tools/ - Some additional files 41 42 43## BUILDING & INSTALLING 44 The preferred way to build clasp is to use [CMake][cmake] version 3.1 or later 45 together with a C++ compiler that supports C++11. 46 47 The following options can be used to configure the build: 48 49 CLASP_BUILD_APP : whether or not to build the clasp application 50 CLASP_BUILD_TESTS : whether or not to build clasp unit tests 51 CLASP_BUILD_EXAMPLES : whether or not to build examples 52 CLASP_BUILD_WITH_THREADS: whether or not to build clasp with threading support 53 (requires C++11) 54 55 For example, to build clasp in release mode in directory `<dir>`: 56 57 cmake -H. -B<dir> 58 cmake --build <dir> 59 60 To install clasp afterwards: 61 62 cmake --build <dir> --target install 63 64 To set the installation prefix, run 65 `cmake` with option `-DCMAKE_INSTALL_PREFIX=<path>`. 66 67 Finally, you can always skip installation and simply copy the 68 clasp executable to a directory of your choice. 69 70## DOCUMENTATION 71 A User's Guide is available from http://potassco.org/ 72 73 Source code documentation can be generated with [Doxygen][doxygen]. 74 Either explicitly: 75 76 cd libclasp/doc/api 77 doxygen clasp.doxy 78 79 or via the `doc_clasp` target when using cmake. 80 81## USAGE 82 clasp reads problem instances either from stdin, e.g 83 84 cat problem | clasp 85 86 or from a given file, e.g 87 88 clasp problem 89 90 Type 91 92 clasp --help 93 94 to get a basic overview of options supported by clasp or 95 96 clasp --help={2,3} 97 98 for a more detailed list. 99 100 In addition to printing status information, clasp also 101 provides information about the computation via its exit status. 102 The exit status is either one or a combination of: 103 104 0 : search was not started because of some option (e.g. '--help') 105 1 : search was interrupted 106 10 : problem was found to be satisfiable 107 20 : problem was proved to be unsatisfiable 108 109 Exit codes 1 and 11 indicate that search was interrupted before 110 the final result was computed. Exit code 30 indicates that either 111 all models were found (enumeration), optimality was proved (optimization), 112 or all consequences were computed (cautious/brave reasoning). 113 Finally, exit codes greater than 32 are used to signal errors. 114 115[enum]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/lpnmr/GebserKNS07 116[proj]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/cpaior/GebserKS09 117[opt]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:journals/tplp/GebserKS11 118[claspmt]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:journals/tplp/GebserKS12 119[claspD2]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/ijcai/GebserKS13 120[hclasp]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/aaai/GebserKROSW13 121[unclasp]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/iclp/AndresKMS12 122[acyc]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:journals/fuin/BomansonGJKS16 123[aspif]: https://www.cs.uni-potsdam.de/wv/publications/#DBLP:conf/iclp/GebserKKOSW16x 124[smodels]: http://www.tcs.hut.fi/Software/smodels/lparse.ps 125[dimacs]: http://www.satcompetition.org/2009/format-benchmarks2009.html 126[opb]: https://www.cril.univ-artois.fr/PB09/solver_req.html 127[doxygen]: https://www.stack.nl/~dimitri/doxygen/ 128[cmake]: https://cmake.org/ 129