Local Search for Checking Satisfiability of Formulas with Trigonometric Functions
摘要
Inspired by the local search framework for SMT over the theory of Non-linear Real Arithmetic (NRA) in [25], we propose in this paper a local search algorithm for SMT over an extended theory of NRA, denoted as \(\textrm{NTA}^{-}\) , which admits the sine function. To establish a key operation, called cell-jump, for updating variable assignments in local search, we design an algorithm for isolating real roots of mixed trigonometric-polynomials with real coefficients. The new local search algorithm is implemented as a tool, called LS( \(\textrm{NTA}^{-}\) ). Experiments are carried out to evaluate LS( \(\textrm{NTA}^{-}\) ) on four classes of benchmarks. The results show that LS( \(\textrm{NTA}^{-}\) ) performs better than state-of-the-art SMT solvers on these benchmarks. It possesses the capability to handle simple transcendental equation constraints, and is good at solving \(\textrm{NTA}^{-}\) formulas with inequality constraints of high degrees.