# SAT-based Explicit LTLf Satisfiability Checking

arXiv: https://arxiv.org/abs/1811.03176 · HTML: https://mlsanity.com/paper/1811.03176/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Nov 2018.

## Built on by (most cited first, 6 of 6)

- [Decidable Fragments of LTLf Modulo Theories (Extended Version)](https://mlsanity.com/paper/2307.16840/) (2023)
- [Forward LTLf Synthesis: DPLL At Work](https://mlsanity.com/paper/2302.13825/) (2023)
- [Computing unsatisfiable cores for LTLf specifications](https://mlsanity.com/paper/2203.04834/) (2022)
- [LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments](https://mlsanity.com/paper/2410.00726/) (2024)
- [On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts](https://mlsanity.com/paper/2408.07324/) (2024)
- [Enumerating Minimal Unsatisfiable Cores of LTLf formulas](https://mlsanity.com/paper/2409.09485/) (2024)

## Abstract (arXiv)

We present here a SAT-based framework for LTLf (Linear Temporal Logic on Finite Traces) satisfiability checking. We use propositional SAT-solving techniques to construct a transition system for the input LTLf formula; satisfiability checking is then reduced to a path-search problem over this transition system. Furthermore, we introduce CDLSC (Conflict-Driven LTLf 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 LTLf satisfiability checking, by demonstrating an approximate four-fold speedup compared to the second-best solver.