No version for distro humble. Known supported distros are highlighted in the buttons above.
No version for distro iron. Known supported distros are highlighted in the buttons above.
No version for distro jazzy. Known supported distros are highlighted in the buttons above.
No version for distro rolling. Known supported distros are highlighted in the buttons above.
No version for distro noetic. Known supported distros are highlighted in the buttons above.
No version for distro ardent. Known supported distros are highlighted in the buttons above.
No version for distro bouncy. Known supported distros are highlighted in the buttons above.
No version for distro crystal. Known supported distros are highlighted in the buttons above.
No version for distro eloquent. Known supported distros are highlighted in the buttons above.
No version for distro dashing. Known supported distros are highlighted in the buttons above.
No version for distro galactic. Known supported distros are highlighted in the buttons above.
No version for distro foxy. Known supported distros are highlighted in the buttons above.
No version for distro lunar. Known supported distros are highlighted in the buttons above.
No version for distro jade. Known supported distros are highlighted in the buttons above.
No version for distro indigo. Known supported distros are highlighted in the buttons above.
Repository Summary
Checkout URI | https://github.com/utexas-bwi/clasp.git |
VCS Type | git |
VCS Version | master |
Last Updated | 2014-04-23 |
Dev Status | DEVELOPED |
CI status | No Continuous Integration |
Released | RELEASED |
Tags | No category tags. |
Contributing |
Help Wanted (0)
Good First Issues (0) Pull Requests to Review (0) |
Packages
Name | Version |
---|---|
clasp | 3.0.3 |
README
clasp-3.x
A conflict-driven nogood learning answer set solver
http://www.cs.uni-potsdam.de/clasp/
http://potassco.sourceforge.net/
OVERVIEW
clasp is an answer set solver for (extended) normal and disjunctive logic programs.
It combines the high-level modeling capacities of answer set programming
with state-of-the-art techniques from the area of Boolean constraint solving.
The primary clasp algorithm relies on conflict-driven nogood learning,
a technique that proved very successful for satisfiability checking (SAT).
Starting with version 2.0, clasp supports parallel (multithreaded) solving.
Starting with version 3.0, clasp supports
- disjunctive logic programs as in claspD-2
- domain heuristic modifications as in hclasp via option "--heuristic=domain"
- unsatisfiable-core based optimization as in unclasp via "--opt-strategy={4,5}"
clasp is written in (mostly) Standard-C++. It was successfully built and run
under Linux (x86-32, x86-64) using gcc/clang and Windows (x86-32, x86-64) using
either Microsoft Visual Studio or MinGW.
Detailed information (including a User's manual), source code,
and pre-compiled binaries are available at: http://potassco.sourceforge.net/
LICENSE
clasp is part of the Potassco project hosted at SourceForge.
It is distributed under the GNU Public License. See COPYING for
details regarding the license.
PACKAGE CONTENTS
COPYING - GNU Public License
CHANGES - Major changes between versions
README - This file
configure.{sh,bat}
- Simple script that creates Makefiles for building clasp (library and application)
app/ - Source code directory of the command-line interface
libclasp/ - Directory of the clasp (static) library (sources, documentation, unit tests)
libprogram_opts/
- Library for parsing command-line options (needed by app)
build_vc/ - Directory containing Visual Studio project files for building clasp
tools/ - Some additional files
BUILDING & INSTALLING
The preferred way to build clasp is to use make and the provided configure script.
You'll need to have the GNU Compiler Collection (GCC) version 3 or
better installed in order to build clasp. You'll also need GNU make 3.80 or better.
On Microsoft Windows, we recommend using MinGW available from http://www.mingw.org/ -
You may want to visit http://www.mingw.org/wiki/Getting_Started for detailed
instructions on installing MinGW. Make sure to also install MinGW-make.
In the following it is assumed that 'make' is an alias for the installed GNU make.
If this is not the case on your system, replace 'make' with the name of the GNU make
executable (e.g. gmake). Furthermore, on Microsoft Windows use ./configure.bat instead of
./configure.sh.
clasp's multithread support requires the Intel Threading Building Blocks library (version >= 3.x)
which is freely available at: http://threadingbuildingblocks.org/
After downloading and installing you may want to set and export the
TBB30_INSTALL_DIR environment variable.
Type
./configure.sh --help
to get an overview of all supported build configurations/options.
To build clasp:
./configure.sh
cd build/release
make
To build clasp with multithread support using TBB30_INSTALL_DIR:
./configure.sh --with-mt
cd build/release_mt
make
To build clasp with multithread support using custom directory structure:
./configure.sh --with-mt TBB_INCLUDE=<path_to_tbb_include> TBB_LIB=<path_to_tbb_lib>
cd build/release_mt
make
To install clasp:
make install
By default, 'make install' will install clasp in '/usr/local/bin'
You can specify an installation prefix other than '/usr/local'
by running the configure-script with the option '--prefix=PATH'.
Alternatively, use option '--bindir=PATH' to directly specify the
installation path.
Finally, you can always skip installation and simply copy the
clasp executable to a directory of your choice.
BUILDING WITH Microsoft Visual Studio
In the directory build_vc/ we provide Microsoft Visual Studio project files
for building clasp. You can download the freely available express edition
of Visual C++ from here:
http://www.microsoft.com/express/Downloads/
Once installed:
- open build_vc\vc9\clasp\clasp.sln
- select the desired solution configuration (typically release_static)
- build the "app" project
USAGE
clasp reads problem instances either from stdin, e.g
cat problem | clasp
or from a given file, e.g
clasp problem
Beside logic programs in SMODELS-format, clasp also supports SAT-problems in DIMACS-,
Max-SAT in (extended) DIMACS-, and PB-problems in OPB and WBO-format.
Type
clasp --help
to get an overview of the various options supported by clasp.
In addition to printing status information, clasp also
provides information about the computation via its exit status.
The exit status is:
10: if the problem was found to be satisfiable
20: if the problem was proved to be unsatisfiable
0 : if the satisfiability of problem is not known,
because search was either interrupted or not started
127: if clasp ran out of memory
Furthermore, the exit status of 1 indicates an error.
CONTRIBUTING
No CONTRIBUTING.md found.
No version for distro kinetic. Known supported distros are highlighted in the buttons above.
No version for distro melodic. Known supported distros are highlighted in the buttons above.