  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.
