Proving Termination Using Recursive Path Orders and SAT Solving.

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

Published in: FroCoS (2007)

Keyphrases

sat solving
sat solvers
term rewrite systems
boolean satisfiability
max sat
boolean optimization
sat problem
lower bound
orders of magnitude
search tree
sat encodings
computational complexity
information retrieval systems
constraint satisfaction