Solving non-linear Horn clauses using a linear solver

TL;DR

This paper introduces an incremental method for solving non-linear Horn clauses by transforming them into linear forms based on tree dimension and using a linear solver iteratively, improving efficiency in verification tasks.

Contribution

The paper presents a novel approach combining program transformation and linear solving to efficiently handle non-linear Horn clauses.

Findings

The approach successfully solves some non-linear Horn clauses with small tree dimension.

Transforming non-linear clauses into linear approximations accelerates the solving process.

Experimental results show promise for verification benchmarks.

Abstract

Developing an efficient non-linear Horn clause solver is a challenging task since the solver has to reason about the tree structures rather than the linear ones as in a linear solver. In this paper we propose an incremental approach to solving a set of non-linear Horn clauses using a linear Horn clause solver. We achieve this by interleaving a program transformation and a linear solver. The program transformation is based on the notion of tree dimension, which we apply to trees corresponding to Horn clause derivations. The dimension of a tree is a measure of its non-linearity -- for example a linear tree (whose nodes have at most one child) has dimension zero while a complete binary tree has dimension equal to its height. A given set of Horn clauses $P$ can be transformed into a new set of clauses $P^k$ (whose derivation trees are the subset of $P$'s derivation trees with dimension at most $k$). We start by generating $P^k$ with $k=0$, which is linear by definition, then pass it to a linear solver. If $P^k$ has a solution $M$, and is a solution to $P$ then $P$ has a solution $M$. If $M$ is not a solution of $P$, we plugged $M$ to $P^{(k+1)}$ which again becomes linear and pass it to the solver and continue successively for increasing value of $k$ until we find a solution to $P$ or resources are exhausted. Experiment on some Horn clause verification benchmarks indicates that this is a promising approach for solving a set of non-linear Horn clauses using a linear solver. It indicates that many times a solution obtained for some under-approximation $P^k$ of $P$ becomes a solution for $P$ for a fairly small value of $k$.