lpopt - A Rule Decomposition Tool for Answer Set Programming
Contents
News
Release of lpopt 2.2
2016-11-28Version 2.2 of the lpopt tool is now available (see Downloads). It uses a new version of the htd library.
Release of lpopt 2.1
2016-08-31Version 2.1 of the lpopt tool is now available (see Downloads). It no more depends on the SHARP library, but on htd.
Release of lpopt 2.0
2016-05-06Version 2.0 of the lpopt tool is now available (see Downloads). It can now read and preprocess the full ASP-Core-2 syntax, as well as some features of the Potassco system.
TopDocumentation
lpopt is a tool to decompose logic programming rules, given in the syntax of answer set programming, into smaller, more manageable rules, that are easier for current ASP solvers and grounders to handle. This is done via a tree decomposition of the original rule, where each node of the tree decomposition then induces a rule. All of the resulting rules combined can then replace the original rule, resulting in the same answer sets (up to some temporary atoms). The maximum size of the resulting rules is no larger than the treewidth of the original rule.
A description of the system, and some theoretical underpinnings, is described in this thesis.
Execution Example
Consider the simple program cousins.asp, which consists of a comment line and a single rule:
To decompose this program, run:
cat cousins.asp | lpopt
The output will look something like the file cousins.asp.lpopt:
The single rule gets decomposed into five shorter ones, introducing four new temporary predicates named temp_decomp_0_0, temp_decomp_0_1, temp_decomp_0_2, and temp_decomp_0_3. In order to check equivalence of the base program and the decomposed program (modulo temporary predicates), you may run an ASP solver with the windsor family example.
Your output may differ from the file cousins.asp.lpopt, since lpopt's tree decomposition heuristics depends on a random seed. Consecutive executions of the above command will result in different rule decompositions.
To tell lpopt to use a given randomization seed instead of randomly choosing one, use the -s option:
cat cousins.asp | lpopt -s 42
Different executions of this command will now result in exactly the same output, namely in the contents of cousins.asp.lpopt (which was created using the seed 42).
Note also that lpopt ignores the comment line.
To let lpopt read from a file instead of the standard input stream, use the -f option:
lpopt -f cousins.asp
Options and Flags
Most of lpopt's options not described in the execution example above are tailored for specific research purposes and thus have little to no probability of practical usage.
The flag -d just parses the input without performing optimizations and outputs the read program. Parsing, for example, already ignores comments.
The flag -i only treats body elements as bags for decomposition, not the head variables. This generally results in a less well optimized output.
The option -h allows to use a different treee decomposition heuristic than the default.
The option -s allows to initialize the random number generator with a specific seed instead of a randomly chosen one.
The option -f allows to read a program from a file instead of standard input.
The option -l allows, in addition to lpopt's default behaviour, to log the maximum treewidth (plus one) of the input rules to a specified file.
Accepted Language
lpopt accepts the full ASP-Core-2 language and some features of the Potassco system.
ASP-Core-2 features include:
- simple arithmetics (
+,-,*,/) - built-in atoms (
<,>,<=,>=,=,!=) - aggregate literals (
#count,#sum,#max,#min) - weak constraints and optimize statements
- anonymous variables
- choice rules
- comments
- strong negation
Potassco features include:
- pooling of terms (e.g.
1;3;5) - term intervals (e.g.
2..6) - the meta-statements
#showand#hide - bitwise arithmetics (
&,?,^,~) - modulo (
\), exponentiation (**) and absolute value (||)
Further Examples
This archive file contains a couple of ASP problem instances suitable for performance comparision of lpopt-driven versus "classical" ASP solving.
TopDownloads
The lpopt source code is available under the open-source GPLv3 license. For both compilation and execution, the htd library must be available on your system. Compilation requires bison version 3.0.4. To compile and install, run the usual ./configure && make && sudo make install.
A precompiled, stand-alone version for 64-bit Unix-like systems is also available, which includes all dependencies, including the htd library.
Version 2.2
- source code (gnu-zipped tar archive)
- precompiled standalone version for x86_64 Unix systems (gnu-zipped tar archive)
Version 2.1
- source code (gnu-zipped tar archive)
- precompiled standalone version for x86_64 Unix systems (gnu-zipped tar archive)
Version 2.0
- source code (gnu-zipped tar archive)
- precompiled standalone version for x86_64 Unix systems (gnu-zipped tar archive)
Contact
In case of questions, bug reports or comments, please send an e-mail to
.