simplify  Program Simplification of NonGround Programs
Abstract
The toolbox simplify provides a first a prototype for program
simplification of nonground
disjunctive datalog programs with negation under the
stable model semantic.
The toolbox scans programs with respect to two potential replacements,
GSUBS, GLSH and indicates which rules are applicable to
those simplifications. Hereby,
 GSUBS (rule subsumption) seeks for rules which can be eliminated from the input program, such that strong equivalence is preserved.
 GLSH (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 simpl1.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
shellscript.
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 GSUBS and GLSH please see [E+06] or [T06].
Benchmarks
The benchmarks reported in [ETW06] are the following
collections:

graphs.tar.gz contains 70 programs which encode
3colorability as rulesubsumption problems.

sat.tar.gz contains 200 programs which encode
satisfiabiliy as rulesubsumption problems.

exp.tar.gz contains 12 proper disjunctive programs
which are tested for local shifting.
References
Feedback
Last update: 20060427 by Stefan Woltran