# Solving Constrained Horn Clauses Using Dependence-Disjoint Expansions

## TL;DR

This paper introduces Clause-Dependence Disjoint (CDD), a new class of recursion-free CHC systems that are smaller and more efficient to solve, and presents a solver named Shara that leverages this class.

## Contribution

The paper defines CDD, a novel class of recursion-free CHC systems, and develops Shara, a solver that reduces arbitrary CHCs to CDDs for improved efficiency.

## Key findings

- Shara outperforms existing solvers in many practical scenarios.
- CDD systems are generally smaller than equivalent systems in other classes.
- The approach improves efficiency in solving recursion-free CHCs.

## Abstract

Recursion-free Constrained Horn Clauses (CHCs) are logic-programming problems that can model safety properties of programs with bounded iteration and recursion. In addition, many CHC solvers reduce recursive systems to a series of recursion-free CHC systems that can each be solved efficiently. In this paper, we define a novel class of recursion-free systems, named Clause-Dependence Disjoint (CDD), that generalizes classes defined in previous work. The advantage of this class is that many CDD systems are smaller than systems which express the same constraints but are part of a different class. This advantage in size allows CDD systems to be solved more efficiently than their counterparts in other classes. We implemented a CHC solver named Shara. Shara solves arbitrary CHC systems by reducing the input to a series of CDD systems. Our evaluation indicates that Shara outperforms state-of-the-art implementations in many practical cases.