SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs

Michael Codish, Jürgen Giesl, Peter Schneider-Kamp, René Thiemann

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

Resumé

This paper introduces a propositional encoding for recursive path orders (RPO), in connection with dependency pairs. Hence, we capture in a uniform setting all common instances of RPO, i.e., lexicographic path orders (LPO), multiset path orders (MPO), and lexicographic path orders with status (LPOS). This facilitates the application of SAT solvers for termination analysis of term rewrite systems (TRSs). We address four main inter-related issues and show how to encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (A) the lexicographic comparison w.r.t. a permutation of the arguments; (B) the multiset extension of a base order; (C) the combined search for a path order together with an argument filter to orient a set of inequalities; and (D) how the choice of the argument filter influences the set of inequalities that have to be oriented (so-called usable rules). We have implemented our contributions in the termination prover AProVE. Extensive experiments show that by our encoding and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.
OriginalsprogEngelsk
TidsskriftJournal of Automated Reasoning
Vol/bind49
Udgave nummer1
Sider (fra-til)53-93
ISSN0168-7433
DOI
StatusUdgivet - 2012

Fingeraftryk

Experiments

Citer dette

Codish, Michael ; Giesl, Jürgen ; Schneider-Kamp, Peter ; Thiemann, René. / SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. I: Journal of Automated Reasoning. 2012 ; Bind 49, Nr. 1. s. 53-93.
@article{ae732c2a9fc64ba9a9a4f019622e20cc,
title = "SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs",
abstract = "This paper introduces a propositional encoding for recursive path orders (RPO), in connection with dependency pairs. Hence, we capture in a uniform setting all common instances of RPO, i.e., lexicographic path orders (LPO), multiset path orders (MPO), and lexicographic path orders with status (LPOS). This facilitates the application of SAT solvers for termination analysis of term rewrite systems (TRSs). We address four main inter-related issues and show how to encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (A) the lexicographic comparison w.r.t. a permutation of the arguments; (B) the multiset extension of a base order; (C) the combined search for a path order together with an argument filter to orient a set of inequalities; and (D) how the choice of the argument filter influences the set of inequalities that have to be oriented (so-called usable rules). We have implemented our contributions in the termination prover AProVE. Extensive experiments show that by our encoding and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.",
author = "Michael Codish and J{\"u}rgen Giesl and Peter Schneider-Kamp and Ren{\'e} Thiemann",
year = "2012",
doi = "10.1007/s10817-010-9211-0",
language = "English",
volume = "49",
pages = "53--93",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer",
number = "1",

}

SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs. / Codish, Michael; Giesl, Jürgen; Schneider-Kamp, Peter; Thiemann, René.

I: Journal of Automated Reasoning, Bind 49, Nr. 1, 2012, s. 53-93.

Publikation: Bidrag til tidsskriftTidsskriftartikelForskningpeer review

TY - JOUR

T1 - SAT Solving for Termination Proofs with Recursive Path Orders and Dependency Pairs

AU - Codish, Michael

AU - Giesl, Jürgen

AU - Schneider-Kamp, Peter

AU - Thiemann, René

PY - 2012

Y1 - 2012

N2 - This paper introduces a propositional encoding for recursive path orders (RPO), in connection with dependency pairs. Hence, we capture in a uniform setting all common instances of RPO, i.e., lexicographic path orders (LPO), multiset path orders (MPO), and lexicographic path orders with status (LPOS). This facilitates the application of SAT solvers for termination analysis of term rewrite systems (TRSs). We address four main inter-related issues and show how to encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (A) the lexicographic comparison w.r.t. a permutation of the arguments; (B) the multiset extension of a base order; (C) the combined search for a path order together with an argument filter to orient a set of inequalities; and (D) how the choice of the argument filter influences the set of inequalities that have to be oriented (so-called usable rules). We have implemented our contributions in the termination prover AProVE. Extensive experiments show that by our encoding and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.

AB - This paper introduces a propositional encoding for recursive path orders (RPO), in connection with dependency pairs. Hence, we capture in a uniform setting all common instances of RPO, i.e., lexicographic path orders (LPO), multiset path orders (MPO), and lexicographic path orders with status (LPOS). This facilitates the application of SAT solvers for termination analysis of term rewrite systems (TRSs). We address four main inter-related issues and show how to encode them as satisfiability problems of propositional formulas that can be efficiently handled by SAT solving: (A) the lexicographic comparison w.r.t. a permutation of the arguments; (B) the multiset extension of a base order; (C) the combined search for a path order together with an argument filter to orient a set of inequalities; and (D) how the choice of the argument filter influences the set of inequalities that have to be oriented (so-called usable rules). We have implemented our contributions in the termination prover AProVE. Extensive experiments show that by our encoding and the application of SAT solvers one obtains speedups in orders of magnitude as well as increased termination proving power.

U2 - 10.1007/s10817-010-9211-0

DO - 10.1007/s10817-010-9211-0

M3 - Journal article

VL - 49

SP - 53

EP - 93

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

IS - 1

ER -