Propositional Encoding of Constraints over Tree-Shaped Data

TL;DR

This paper introduces a functional programming language with algebraic data types for specifying constraints over tree-shaped data, translating these constraints into propositional logic for automated analysis tasks.

Contribution

It presents a novel language and compiler that convert constraints over tree data into SAT problems, enabling automated termination analysis.

Findings

Successfully translated tree constraints into SAT problems.

Applied to automated termination analysis of rewrite systems.

Demonstrated the language's expressiveness and practical utility.

Abstract

We present a functional programming language for specifying constraints over tree-shaped data. The language allows for Haskell-like algebraic data types and pattern matching. Our constraint compiler CO4 translates these programs into satisfiability problems in propositional logic. We present an application from the area of automated analysis of (non-)termination of rewrite systems.