DPvis is a Java tool to visualize the structure of SAT instances and runs of the DPLL (Davis-Putnam-Logemann-Loveland) procedure. It uses advanced graph layout algorithms to display the problem's internal structure arising from its variable dependency (interaction) graph. DPvis is also able to generate animations showing the dynamic change of a problem's structure during a typical DPLL run. Besides implementing a simple variant of the DPLL algorithm on its own, DPvis also features an interface to MiniSAT, a state-of-the-art DPLL implementation. Using this interface, runs of MiniSAT can be visualized—including the generated search tree and the effects of clause learning. DPvis is supposed to help in teaching the DPLL algorithm and in gaining new insights in the structure (and hardness) of SAT instances.
Propositional Encoding of Cardinality Constraints[link][download]
Cardinality constraints—expressing numerical bounds on discrete quantities—arise frequently from the encoding of real-world problems (e.g. product configuration, radio frequency assignment, discrete tomography). Boolean cardinality constraints put numerical restrictions on the number of Boolean variables that are allowed to be true at the same time. A typical construct like ≤(x1,...,xn) expresses that not more than k out of n variables x1,...,xn are allowed to be true. Encoding cardinality constraints to conjunctive normal form (CNF) is important, as typical SAT-Solvers expect input in this form. We have implemented two CNF encodings for Boolean cardinality constraints, LTSEQ and LTPAR, based on different counter circuits. Whereas LTPAR needs only 7n clauses and 2n variables, LTSEQ requires O(nĚk) clauses and O(nĚk) additional encoding variables, but allows for an immediate decision by unit-propagation (i.e. without search), whether the constraint is fulfilled or not. Details can be found in a CP-2005 paper and in an extended technical report.[publication][talk]
PaSAT is a parallel implementation of the DPLL (Davis-Putnam-Logemann-Loveland) algorithm. PaSAT implements dynamic search space partitioning, lemma generation, intelligent backjumping, and—as a novelty—lemma exchange. PaSAT is built upon the threading middleware DOTS (Distributed Object-Oriented Threads System), a parallel programming toolkit for C++ that integrates a wide range of different computing platforms into a single system environment for high performance computing. It makes the threads programming paradigm available in a distributed memory environment. Thus with DOTS, a hierarchical multiprocessor, consisting of a (heterogeneous) cluster of shared-memory multiprocessor systems can be efficiently programmed using a single paradigm (fork/join).[link][download][publication]
ARA is an automatic theorem prover for various kinds of relation algebras. It is based on Gordeev's Reduction Predicate Calculi for n-variable logic (RPCn) which allow first-order finite variable proofs. Using results from Tarski/Givant and Maddux we can prove validity in the theories of simple semi-associative relation algebras, relation algebras and representable relation algebras using the calculi RPC3, RPC4 and RPCω. ARA is a Haskell-implementation that offers various reduction strategies for RPCn, and a set of simplifications preserving n-variable provability.[link][publication][press article (in German)]
Complex products like motor vehicles can be ordered by the customer in a great number of variations. It may turn out, however, that an ordered configuration is not actually manufacturable. Geometrical, functional, country specific, and sales restrictions have to be considered. Therefore, electronic configuration systems are employed, allowing an automatized management of both product variants and constraints. In our work we examine how to apply formal methods to check consistency of such configuration systems. We formulate different consistency properties and encode them—together with the whole order management process—in propositional dynamic logic (PDL). Thus, we enable the use of automatic theorem proving methods. Instead of generating proofs in PDL directly, we translae PDL proof obligations to purely propositional logic assertions. That way, we can make use of advanced SAT-Solving methods. Our approach allows to formulate assertions about the totality of all valid product instances. Errors in the product data base—and ultimately in the order management process—may thus be reduced.[link][publication]
Large-scale medical systems—like magnetic resonance tomographs—are manufactured with a steadily growing number of product options. Different model lines can be equipped with large numbers of supplementary equipment options like (gradient) coils, amplifiers, magnets or imaging devices. The diversity in service and maintenance procedures, which may be different for each of the many product instances, grows accordingly. Therefore, instead of having one common on-line service handbook for all medical devices, Siemens parcels out the on-line documentation into small (help) packages, out of which a suitable subset is selected for each individual product instance. Selection of packages is controlled by XML terms. To check whether the existing set of help packages is sufficient for all possible devices and service cases, we developed the Help-Checker-Tool (HCT). HCT translates XML input into Boolean logic formulae and employs both SAT- and BDD-based methods to check consistency and completeness of the on-line documentation. To explain its reasoning and to facilitate error correction, it generates small (counter-)examples for cases where verification conditions are violated.