# Forward LTLf Synthesis: DPLL At Work

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

## Key facts

- Cited by 4 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 67 references that are in the map.
- First posted on arXiv 27 Feb 2023.

## Builds on (most cited first, 4 of 4)

- [Symbolic LTLf Synthesis](https://mlsanity.com/paper/1705.08426/) (2017)
- [Hybrid Compositional Reasoning for Reactive Synthesis from Finite-Horizon Specifications](https://mlsanity.com/paper/1911.08145/) (2019)
- [SAT-based Explicit LTLf Satisfiability Checking](https://mlsanity.com/paper/1811.03176/) (2018)
- [A Symbolic Approach to Safety LTL Synthesis](https://mlsanity.com/paper/1709.07495/) (2017)

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

- [Model Checking Strategies from Synthesis Over Finite Traces](https://mlsanity.com/paper/2305.08319/) (2023)
- [On-the-fly Synthesis for LTL over Finite Traces: An Efficient Approach that Counts](https://mlsanity.com/paper/2408.07324/) (2024)
- [Efficient Dynamic Shielding for Parametric Safety Specifications](https://mlsanity.com/paper/2505.22104/) (2025)
- [A Compositional Framework for On-the-Fly LTLf Synthesis](https://mlsanity.com/paper/2508.04116/) (2025)

## Abstract (arXiv)

This paper proposes a new AND-OR graph search framework for synthesis of Linear Temporal Logic on finite traces (LTLf), that overcomes some limitations of previous approaches. Within such framework, we devise a procedure inspired by the Davis-Putnam-Logemann-Loveland (DPLL) algorithm to generate the next available agent-environment moves in a truly depth-first fashion, possibly avoiding exhaustive enumeration or costly compilations. We also propose a novel equivalence check for search nodes based on syntactic equivalence of state formulas. Since the resulting procedure is not guaranteed to terminate, we identify a stopping condition to abort execution and restart the search with state-equivalence checking based on Binary Decision Diagrams (BDD), which we show to be correct. The experimental results show that in many cases the proposed techniques outperform other state-of-the-art approaches. Our implementation Nike competed in the LTLf Realizability Track in the 2023 edition of SYNTCOMP, and won the competition.