Finding Regular Herbrand Models for CHCs using Answer Set Programming

TL;DR

This paper presents a novel approach to verifying the satisfiability of Constrained Horn Clauses over Algebraic Data Types by encoding the problem into Answer Set Programming and using Clingo to find regular Herbrand models or counterexamples.

Contribution

It introduces an ASP-based method for constructing tree automata to recognize Herbrand models, offering an alternative to existing automaton derivation techniques.

Findings

Successfully encodes CHCs with ADTs into ASP

Provides a semi-complete satisfiability checker using Clingo

Can find regular Herbrand models or counterexamples

Abstract

We are interested in proving satisfiability of Constrained Horn Clauses (CHCs) over Algebraic Data Types (ADTs). We propose to prove satisfiability by building a tree automaton recognizing the Herbrand model of the CHCs. If such an automaton exists then the model is said to be regular, i.e., the Herbrand model is a regular set of atoms. Kostyukov et al. have shown how to derive an automaton when CVC4 finds a finite model of the CHCs. We propose an alternative way to build the automaton using an encoding into a SAT problem using Clingo, an Answer Set Programming (ASP) tool. We implemented a translation of CHCs with ADTs into an ASP problem. Combined with Clingo, we obtain a semi-complete satisfiability checker: it finds a tree automaton if a regular Herbrand model exists or finds a counter-example if the problem is unsatisfiable.