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
ccT. For this type of correspondence problems,
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
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
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).
ccT is capable of deciding two types of correspondence problems:
Programs P, Q, context set A, and projection set B are passed to
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.
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
progQ, context set
setA, and projection set
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
Model Checking at CMU
boole. Hence, the QBF can be generated and solved in one step by piping it to
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.
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
ccTis directly processible by
Qst(Quantifier shifting tool), (binary), is a tool for transforming QBFs into prenex-normal form. Different shifting strategies and output formats are supported.
Qstis 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-genwas 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
makein the directory
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
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.
dlpeqwhich is based on a reduction to disjunctive logic programs, using
gntas 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.|