A SAT Encoding for Solving Games with Energy Objectives

Recently, a reduction from the problem of solving parity games to the satisfiability problem in propositional logic (SAT) have been proposed in [5], motivated by the success of SAT solvers in symbolic verification. With analogous motivations, we show how to exploit the notion of energy progress measure to devise a reduction from the problem of energy games to the satisfiability problem for formulas of propositional logic in conjunctive normal form.