The branch-and-bound framework has already been successfully applied in SAT-modulotheories (SMT) solvers to check the satisfiability of linear integer arithmetic formulas. In this paper we study how it can be used in SMT solvers for non-linear integer arithmetic on top of two real-algebraic decision procedures: the virtual substitution and the cylindrical algebraic decomposition methods. We implemented this approach in our SMT solver SMT-RAT and compared it with the currently best performing SMT solvers for this logic, which are mostly based on bit-blasting. Furthermore, we implemented a combination of our approach with bit-blasting that outperforms the state-of-the-art SMT solvers for most instances.
展开▼
