simplify - Program Simplification of Non-Ground Programs
Abstract
The toolbox simplify provides a first a prototype for program
simplification of non-ground
disjunctive datalog programs with negation under the
stable model semantic.
The toolbox scans programs with respect to two potential replacements,
G-SUBS, G-LSH and indicates which rules are applicable to
those simplifications. Hereby,
- G-SUBS (rule subsumption) seeks for rules which can be eliminated from the input program, such that strong equivalence is preserved.
- G-LSH (local shifting) seeks for proper disjunctive rules which can be shifted into
normal rules, such that uniform equivalence is preserved.
Both replacement techniques are described in [E+06]. For a description of the implementations see Chapter 5.1 of [Traxler06], or [ETW06].
Installation
Download simpl-1.0.tar.gz and unpack it. You might need to change the variable $DLV in the perl scripts simplify_subs.pl and simplify_glsh.pl. This variable contains the location of your DLV system. Otherwise, make sure that the PATH variable of your command shell contains the location of your DLV system.
Requirements:
Description
At the moment our toolbox consists of two scripts which take as input
a program P in DLV syntax.
Both scripts are called by the simplify shell-script.
As an example take the file intro.dl.
After calling it with
on the command line it first outputs rules which apply for
subsumption and then rules which apply for shifting:
Scanning for Rule Subsumption...
b(X) v b(a) :- edge (X,Y), node(X), node(a), not r(X), not g(a), not g(X).
[subsumbed by r(Y) v b(Y) v g(Y) :- node(Y).]
Scanning for Local Shifting...
r(Y) v b(Y) v g(Y) :- node(Y).
|
For the exact definitions of G-SUBS and G-LSH please see [E+06] or [T06].
Benchmarks
The benchmarks reported in [ETW06] are the following
collections:
-
graphs.tar.gz contains 70 programs which encode
3-colorability as rule-subsumption problems.
-
sat.tar.gz contains 200 programs which encode
satisfiabiliy as rule-subsumption problems.
-
exp.tar.gz contains 12 proper disjunctive programs
which are tested for local shifting.
References
Feedback
Last update: 2006-04-27 by Stefan Woltran