Solving non-linear Horn clauses using a linear Horn clause solver

Bishoksan Kafle
(Roskilde University)
John P. Gallagher
(Roskilde University and IMDEA Software Institute)
Pierre Ganty
(IMDEA Software Institute, Spain)

In this paper we show that checking satisfiability of a set of non-linear Horn clauses (also called a non-linear Horn clause program) can be achieved using a solver for linear Horn clauses. We achieve this by interleaving a program transformation with a satisfiability checker for linear Horn clauses (also called a solver for linear Horn clauses). The program transformation is based on the notion of tree dimension, which we apply to a set of non-linear clauses, yielding a set whose derivation trees have bounded dimension. Such a set of clauses can be linearised. The main algorithm then proceeds by applying the linearisation transformation and solver for linear Horn clauses to a sequence of sets of clauses with successively increasing dimension bound. The approach is then further developed by using a solution of clauses of lower dimension to (partially) linearise clauses of higher dimension. We constructed a prototype implementation of this approach and performed some experiments on a set of verification problems, which shows some promise.

In John P. Gallagher and Philipp Rümmer: Proceedings 3rd Workshop on Horn Clauses for Verification and Synthesis (HCVS2016), Eindhoven, The Netherlands, 3rd April 2016, Electronic Proceedings in Theoretical Computer Science 219, pp. 33–48.
Published: 14th July 2016.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: