File: clasp.1

package info (click to toggle)
clasp 3.3.4-2
  • links: PTS, VCS
  • area: main
  • in suites: buster
  • size: 4,028 kB
  • sloc: cpp: 69,424; ansic: 207; xml: 182; sh: 92; makefile: 33
file content (61 lines) | stat: -rw-r--r-- 2,381 bytes parent folder | download | duplicates (4)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
.\"                                      Hey, EMACS: -*- nroff -*-
.\" First parameter, NAME, should be all caps
.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection
.\" other parameters are allowed: see man(7), man(1)
.TH CLASP 1 "March  4, 2010"
.\" Please adjust this date whenever revising the manpage.
.\"
.\" Some roff macros, for reference:
.\" .nh        disable hyphenation
.\" .hy        enable hyphenation
.\" .ad l      left justify
.\" .ad b      justify to both left and right margins
.\" .nf        disable filling
.\" .fi        enable filling
.\" .br        insert line break
.\" .sp <n>    insert n+1 empty lines
.\" for manpage-specific macros, see man(7)
.SH NAME
clasp \- a conflict-driven nogood learning answer set solver 
.SH SYNOPSIS
.B clasp
[\fInumber\fR] \fR[\fIoptions\fR]
.SH DESCRIPTION
This manual page documents briefly the
.B clasp
command.
.PP
.\" TeX users may be more comfortable with the \fB<whatever>\fP and
.\" \fI<whatever>\fP escape sequences to invode bold face and italics,
.\" respectively.
\fBclasp\fP is an answer set solver for (extended) normal logic
programs. It combines the high-level modeling capacities of answer set
programming (ASP) 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). Unlike other learning
ASP solvers, clasp does not rely on legacy software, such as a SAT
solver or any other existing ASP solver. Rather, clasp has been
genuinely developed for answer set solving based on conflict-driven
nogood learning. clasp can be applied as an ASP solver (on LPARSE
output format), as a SAT solver (on simplified DIMACS/CNF format), or
as a PB solver (on OPB format).
.SH OPTIONS
These programs follow the usual GNU command line syntax, with long
options starting with two dashes (`-').
A summary of options is included below.
For a complete description, see <http://www.potassco.org/clasp/>.
.TP
.B \-h, \-\-help
Show summary of options.
.TP
.B \-v, \-\-version
Show version of program.
.SH SEE ALSO
.BR gringo (1).
.br
.SH AUTHOR
clasp was written by Benjamin Kaufmann <kaufmann@cs.uni-potsdam.de>.
.PP
This manual page was written by Thomas Krennwallner <tkren@kr.tuwien.ac.at>,
for the Debian project (and may be used by others).