## SATEQ## Verifying the Equivalence of Propositional Theories[Background] [Usage] [Download] [Benchmarks] [Related Publications and Software] ## Background
## Using the Software`sateq` is invoked as follows:
```
```
Command line options for -
`-h` or`--help` : print help message -
`--version` : print version information -
`-v` : verbose mode (human readable) -
`-s` : use symbolic names given in the comments
`-s` option
because atom numbers do not coincide:
`sateq -s qx-04.cnf qy-04.cnf > test-04.cnf` ## DownloadDisclaimer:
The software below is provided on "as is" basis, without
warranties of any kind or fitness for a particular purpose.
## 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*(preprint). Theory and Practice of Logic Programming, 7(4), 1-48, 2007.`SMODELS` system - 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 |