Markus Iser 

Karlsruhe Institute of Technology, Diplomarbeit, 2012

Kodkod is a constraint solver for bounded relational first-order logic which translates problems into equisatisfiable propositional formulas, in turn using an off-the-shelf SAT solver to check their satisfiability. This work is motivated by the observation that permuting top-level propositions in Kodkod can lead to great runtime variations in the SAT solver. The reason for this phenomenon are different initial variable orderings, as Kodkod processes and translates the constraints in the given order. 

We extended the interface between Kodkod and MiniSAT to accept priorities for variables and used them in two distinct ways. One approach involves a partial override of MiniSAT’s native variable ordering score, whereas the other is based on score ini-tialization, leaving MiniSAT a great liberty during the curse of evaluation. We device a method of extracting variable priorities by structural analysis of Kodkod’s Abstract Syntax Tree (AST).

In a simple initial approach, we restricted the search to Kodkod’s primary variables and explain the correspondence to similar experiments regarding input restricted branching found in literature. While that first naive approach leads to considerable performance boosts on satisfiable problems, a general performance deterioration is encountered on unsatisfiable instances. This phenomenon empirically confirms important proof-theoretic results.

In a second approach, we uniformly initialized the MiniSAT score related to Kodkod’s primary variables, hereby strongly dampening the performance deterioration on unsatisfiable problems while still yielding the performance improvement on satisfiable problems expectable due to the initial experiment.

By structural analysis of Kodkod’s AST we calculated a more fine-grained set of priorities to modify the inner ordering of Kodkod’s primary variables. The objective is to prioritize the most constraint variables for early discovery of dead ends in the search tree and to maximize boolean constraint propagation. This third and last approach leads to runtime improvements on both satisfiable and unsatisfiable instances. In order to be able to analyze Kodkod’s abstract syntax tree, we developed methods which may yet remain interesting for future approaches.