Solving non-linear Horn clauses using a linear Horn clause solver
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...
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Open Publishing Association
2016-07-01
|
| Series: | Electronic Proceedings in Theoretical Computer Science |
| Online Access: | http://arxiv.org/pdf/1607.04459v1 |
| _version_ | 1818862756447649792 |
|---|---|
| author | Bishoksan Kafle John P. Gallagher Pierre Ganty |
| author_facet | Bishoksan Kafle John P. Gallagher Pierre Ganty |
| author_sort | Bishoksan Kafle |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-12-19T10:04:55Z |
| format | Article |
| id | doaj.art-30d2f4d2e6ff45ec893bf9574c936250 |
| institution | Directory Open Access Journal |
| issn | 2075-2180 |
| language | English |
| last_indexed | 2024-12-19T10:04:55Z |
| publishDate | 2016-07-01 |
| publisher | Open Publishing Association |
| record_format | Article |
| series | Electronic Proceedings in Theoretical Computer Science |
| spelling | doaj.art-30d2f4d2e6ff45ec893bf9574c9362502022-12-21T20:26:32ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802016-07-01219Proc. HCVS2016334810.4204/EPTCS.219.4:6Solving non-linear Horn clauses using a linear Horn clause solverBishoksan Kafle0John P. Gallagher1Pierre Ganty2 Roskilde University Roskilde University and IMDEA Software Institute 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.http://arxiv.org/pdf/1607.04459v1 |
| spellingShingle | Bishoksan Kafle John P. Gallagher Pierre Ganty Solving non-linear Horn clauses using a linear Horn clause solver Electronic Proceedings in Theoretical Computer Science |
| title | Solving non-linear Horn clauses using a linear Horn clause solver |
| title_full | Solving non-linear Horn clauses using a linear Horn clause solver |
| title_fullStr | Solving non-linear Horn clauses using a linear Horn clause solver |
| title_full_unstemmed | Solving non-linear Horn clauses using a linear Horn clause solver |
| title_short | Solving non-linear Horn clauses using a linear Horn clause solver |
| title_sort | solving non linear horn clauses using a linear horn clause solver |
| url | http://arxiv.org/pdf/1607.04459v1 |
| work_keys_str_mv | AT bishoksankafle solvingnonlinearhornclausesusingalinearhornclausesolver AT johnpgallagher solvingnonlinearhornclausesusingalinearhornclausesolver AT pierreganty solvingnonlinearhornclausesusingalinearhornclausesolver |