Variable and clause elimination for LTL satisfiability checking

TL;DR

This paper introduces variable and clause elimination techniques for LTL satisfiability checking, adapting SAT preprocessing methods to reduce formula size and improve solver efficiency.

Contribution

It extends SAT preprocessing techniques to LTL, enabling more effective simplification and faster satisfiability checking through label-based clause reinterpretation.

Findings

Significant reduction in formula size achieved

Decreased solver runtime observed

Effective adaptation of SAT techniques to LTL

Abstract

We study preprocessing techniques for clause normal forms of LTL formulas. Applying the mechanism of labelled clauses enables us to reinterpret LTL satisfiability as a set of purely propositional problems and thus to transfer simplification ideas from SAT to LTL. We demonstrate this by adapting variable and clause elimination, a very effective preprocessing technique used by modern SAT solvers. Our experiments confirm that even in the temporal setting substantial reductions in formula size and subsequent decrease of solver runtime can be achieved.