|
|
|---|
The Tool ccT (correspondence checking Tool), pronounced [ze-ze-Top],
implements the general framework for specifying program
correspondences under the answer-set semantics introduced by Eiter et al. ("On Solution Correspondences
in Answer-Set Programming", 2005, pdf). The
correspondence problem (program equivalence, program inclusion)
is reduced to a quantified Boolean formula (QBF) such that
the resulting QBF is true iff the correspondence problem holds. The reduction to QBFs was provided by
Hans Tompits and Stefan Woltran ("Towards Implementations for Advanced Equivalence Checking in
Answer-Set Programming", 2005, SpringerLink).
NEW: Recently, an important instantiation of the above
mentioned correspondence framework, namely uniform equivalence relative to a context set and
a projection set, was dealt with [6,7]. The resulting encodings are incooperated into the
implementation of ccT. For this type of correspondence problems, ccT can
generate not only QBFs to answer the decision problem whether correspondence holds but can also generate QBFs for
computing counterexamples in case correspondence does not hold.
Also, the test generator (see below) was adapted for problems of relativised uniform equivalence
with projection.
Remark:
At first, the tool was named eqcheck. If somewhere still occurs the old name, it refers
to the same tool.
Download ccT.tar.gz, unpack it, and call make in the
directory ccT.
In the implemented framework, the correspondence of two propositional disjunctive logic programs,
P and Q, is determined in terms of a context set A, a projection set
B, as well as a comparison relation (set equality or set inclusion).
In fact, ccT is capable of deciding two types of correspondence problems:
Programs P, Q, context set A, and projection set B are passed to ccT
as command line arguments.
Different encodings to QBFs (normal, compact), correspondence problems (inclusion, equivalence), and
output formats can be specified as options.
Moreover, it can be specified weather it should be checked for uniform or strong equivalence.
Type ccT -h for detailed usage.
The input format for programs is a subset of ground-DLV
syntax. See also http://www.dlvsystem.com
for DLV. The syntax for sets of atoms (context, projection) is simply a comma-separated list of atoms
within parentheses, e.g.,
( a1, b2, c3(a,b), e_4 ).
For two programs progP,
progQ, context set setA, and projection set setB
ccT -e progP progQ setA setB
generates the corresponding QBF for the equivalence problem (P == Q) with respect
to the context set and the projection set.
Output is written to the standard-output device. By default, the resulting QBF is
processible by the BDD-based solver boole. See
Model Checking at CMU
for boole. Hence, the QBF can be generated and solved in one step by piping it to
boole:
ccT -e progP progQ setA setB | boole
Deciding such correspondence problems in the general case is hard for the fourth level of the polynomial hierarchy for rel. strong equivalence (inclusion) with projection and hard for the third level of the PH for rel. uniform equivalence (inclusion) with projection. However, special cases as, e.g., strong equivalence, ordinary equivalence, and uniform equivalence, are located at a lower level of the PH. For the compact encoding, the number of quantifier alternations always reflects the intrinsic hardness of the correspondence problem. Regarding the prenex-normal form of the QBFs, the innermost quantifier might become the for-all quantifier. If this is the case, the tool encodes the complementary problem, thus, the innermost quantifier turns into an existential quantifier. If the innermost quantifier would be the for-all quantifier, our method to transform the formula into a prenex CNF (Tseitin 1968) would add an additional quantifier alternation in the prenex and we want to avoid this. The user will always be informed if the complementary problem was encoded by a message on the standard-error device.
Additional to ccT, the following tools may be of interest:
boole (binary) is a free available,
BDD-based solver. QBFs need not to be in any normal form.
For details and download see
Model Checking at CMU. The output of ccT is directly processible by boole.
Qst (Quantifier shifting tool), (binary), is a tool
for transforming
QBFs into prenex-normal form.
Different shifting strategies and output formats are supported.
Qst is part of the Traquasto Software Package. The package was developed by Martina
Seidl and Michael Zolda and is
described in Michael Zolda's master
thesis "Comparing Different Prenexing Strategies for Quantified Boolean Formulas" (pdf,
ps).
ccT-gen was developed to generate benchmark instances for ccT.
It generates parameterized
QBFs by random and exploits complexity results to reduce this QBFs to correspondence problems such that
the correspondence problem holds
iff the QBF is valid.
Download ccT-gen.tar.gz, unpack it, and call make in
the directory ccT-gen.
4_4_4_4_p12_q4.tar.gz
The archive is a test set generated with
ccT-gen -v "4 4 4 4" -p 12 -q 4 -i 1000 -w.
Therefore, it contains
1000 problem instances of inclusion problems. Each problem
corresponds to indexed files P, Q, A, B and a indexed file QBF that
contains a QBF in plain boole syntax. The number of clauses is set to 12 and the
number of literals per clause is set to 4. The ration positive to negative literals is 0.5.
The QBF is true iff the inclusion problem holds. In this test set 465 from 1000 QBFs are
true. Inclusion of programs can be verified by typing
ccT P Q A B
and evaluating the output QBF.
dlpeq which
is based on a reduction to
disjunctive logic programs, using gnt
as answer-set solver. The archive
contains the benchmark instances.
For a detailed description see
(E. Oikarinen and T. Janhunen. Verifying the equivalence of logic programs in the disjunctive case.
In Proceedings of the 7th International Conference on Logic Programming and Nonmonotonic Reasoning, 2004).
| Send an e-mail to Johannes Oetsch, oetsch[at]kr.tuwien.ac.at. |
|