TCS / Software / sateq
Helsinki University of Technology, 
     Laboratory for Theoretical Computer Science


Verifying the Equivalence of Propositional Theories

[Background] [Usage] [Download] [Benchmarks] [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:

  • -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.


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.


  • 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.


  • 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