| |
SATEQ
Verifying the Equivalence of Propositional Theories
[Background]
[Usage]
[Download]
[Benchmarks]
[Related Publications and Software]
Background
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:
-
-h or --help: print help message
-
--version: print version information
-
-v: verbose mode (human readable)
-
-s: use symbolic names given in the comments
E.g. the instances for checking the equivalence of n-queens encodings
(see below) have to be produced with the -s option
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
direction.
Download
Disclaimer:
The software below is provided on "as is" basis, without
warranties of any kind or fitness for a particular purpose.
Copyright:
The copyright for the binaries is held by Tomi Janhunen. You may
freely use this software for academic and research purposes but not
redistribute it.
Binaries
- 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
an
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
where n is the atom number and name
gives the name of the atom). The translator is designed to be used with
the front-end lparse of the
smodels system.
- 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.
Benchmarks
- Source code for column-wise and
row-wise encodings. We use
the front-end
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
instance (n=4)
- All instances for row-wise
encoding (4<n<32,n=64,n=128); check the smallest
instance (n=4)
- All instances for
n-queens equivalence (4<n<32) produced with
SATEQ;
check the smallest
instance (n=4).
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
the
SMODELS system
(preprint).
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
(preprint).
Journal of Applied Non-Classical Logics, 16(1-2), 35-86, 2006.
-
LPEQ:
verifying the equivalence of logic programs
-
LP2SAT:
translating logic programs into sets of clauses
[TCS main]
[Contact Info]
[Personnel]
[Research]
[Publications]
[Software]
[Studies]
[News Archive]
[Links]
Latest update: 06 February 2013.
Tomi Janhunen
|
