SAT-Based Explicit LTLf Satisfiability Checking

Abstract

We present a SAT-based framework for LTL_f (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTL_f formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTL_f Satisfiability Checking), a novel algorithm that leverages information produced by propositional SAT solvers from both satisfiability and unsatisfiability results. Experimental evaluations show that CDLSC outperforms all other existing approaches for LTL_f satisfiability checking, by demonstrating an approximate four-fold speed-up compared to the second-best solver.