SAT-Based Explicit LTLf Satisfiability Checking
Abstract
We present 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 speed-up compared to the second-best solver.
Cite
Text
Li et al. "SAT-Based Explicit LTLf Satisfiability Checking." AAAI Conference on Artificial Intelligence, 2019. doi:10.1609/AAAI.V33I01.33012946Markdown
[Li et al. "SAT-Based Explicit LTLf Satisfiability Checking." AAAI Conference on Artificial Intelligence, 2019.](https://mlanthology.org/aaai/2019/li2019aaai-sat/) doi:10.1609/AAAI.V33I01.33012946BibTeX
@inproceedings{li2019aaai-sat,
title = {{SAT-Based Explicit LTLf Satisfiability Checking}},
author = {Li, Jianwen and Rozier, Kristin Y. and Pu, Geguang and Zhang, Yueling and Vardi, Moshe Y.},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {2019},
pages = {2946-2953},
doi = {10.1609/AAAI.V33I01.33012946},
url = {https://mlanthology.org/aaai/2019/li2019aaai-sat/}
}