Verifying the Equivalence of Propositional Theories
[Related Publications and Software]
sateq is an implementation of a translation-based method
for the verification of propositional theories expressed as sets of
clauses in the DIMACS format.
Using the Software
sateq is invoked as follows:
sateq <options> <file1> <file2>
Command line options for
lpeq are the following:
E.g. the instances for checking the equivalence of n-queens encodings
(see below) have to be produced with the
--help: print help message
--version: print version information
-v: verbose mode (human readable)
-s: use symbolic names given in the comments
because atom numbers do not coincide:
sateq -s qx-04.cnf qy-04.cnf > test-04.cnf
For symmetry reasons there is no need to perform the test in the other
The software below is provided on "as is" basis, without
warranties of any kind or fitness for a particular purpose.
The copyright for the binaries is held by Tomi Janhunen. You may
freely use this software for academic and research purposes but not
- sateq-1.7: combines two cnfs,
say C1 and C2, given in the DIMACS format for equivalence testing.
The idea is that the resulting translation EQT(C1,C2) in cnf is
unsatisfiable iff every model of C1 is also a model of C2.
- dimacs-1.5: interpret
SMODELS program as a set of clauses. Symbolic
information is encoded in the comments of the resulting DIMACS
cnf file (entries of the form
c n name
n is the atom number and
gives the name of the atom). The translator is designed to be used with
lparse of the
- interpret-1.4: maps
atom numbers back to symbols
(extracted from DIMACS comments explained above).
- A wrapper script
for the minisat SAT solver shows how
INTERPRET is used.
- Source code for column-wise and
row-wise encodings. We use
LPARSE of the
smodels system for
instantiation. The result is a logic program whose
rules are then interpreted as clauses using
DIMACS (see below) and a command line like this:
lparse -dnone -cn=8 qx.lp | dimacs > qx-08.cnf
- All instances for column-wise
n-queens encoding (4<n<32,n=64,n=128); check the smallest
- All instances for row-wise
encoding (4<n<32,n=64,n=128); check the smallest
- All instances for
n-queens equivalence (4<n<32) produced with
check the smallest
These instances are quite hard, e.g.,
MINISAT solves n=13 in roughly 40 minutes.
Related Publications and Software
- T. Janhunen:
Modular Equivalence in General.
In Proc. of ECAI 2008, to appear.
- T. Janhunen and E. Oikarinen:
Automated Verification of Weak Equivalence within
Theory and Practice of Logic Programming, 7(4), 1-48, 2007.
- T. Janhunen, E. Oikarinen, H. Tompits, and S. Woltran:
Modularity aspects of disjunctive stable models.
In Proc. of LPMNR'07, 175-187, 2007.
- E. Oikarinen and T. Janhunen:
Modular Equivalence for Normal Logic Programs.
In Proc. of ECAI 2006, 412-416, 2006.
An extended version appeared in Proc. of NMR 2006
(big file), 12-20, 2006.
- T. Janhunen:
Some (in)translatability results for Normal Logic
Programs and Propositional Theories
Journal of Applied Non-Classical Logics, 16(1-2), 35-86, 2006.
verifying the equivalence of logic programs
translating logic programs into sets of clauses
Latest update: 06 February 2013.