Input Restricted Branching for Kodkod

Kodkod is an efficient SAT-based constraint solver for first order logic with relations, transitive closure, bit-vector arithmetic, and partial models. Kodkod translates a constraint satisfaction problem given in relational first-order logic into an equisatisfiable formula in propositional logic, in turn using an off-the-shelf SAT solver to check their satisfiability. Have a look at the Kodkod Website for further information about Kodkod.

SAT solvers performance highly depends on the chosen variable ordering heuristic. We conducted several experiments exploiting information available at the Kodkod level to influence SAT solver's variable ordering. Among these, variants of Input Restricted Branching lead to performance improvements by high orders of magnitude on satisfiable problems.

We provide here a patch for Kodkod 1.5.2 and MiniSAT 2.2.0 incorporating the possibility to choose a variable ordering method at the Kodkod-side. Among these you can choose between two variants of Input Restricted Branching and the default behavior. All of this is configurable via one additional option in the Kodkod Options-object. We provide an API documentation for the new source-files and files that we have changed.

Publications

Markus Iser, Mana Taghdiri, Carsten Sinz
Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod (Poster Presentation)

Markus Iser
Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod

People

Mana Taghdiri
Carsten Sinz
Markus Iser

Download

• Source Code
  The archive contains the modified source code of Kodkod 1.5.2 as well as two patch files that document the changes applied to the original version.
  Kodkod 1.5.2 (Source)
• Patch Files
  If you have already embedded Kodkod 1.5.2 in your program you can as well apply the two patches to your source-code. Be careful if you do not use the exact same version, you might need to copy some lines of code by hand.
  Kokod 1.5.2 (Patch)
  MiniSAT 2.2.0 (Patch)