Abstract
We present a new method for solving nonlinear integer arithmetic constraints. The method relies on the MCSat approach to solving nonlinear constraints, while using branch and bound in a conflict-directed manner. We report encouraging experimental results where the new procedure outperforms state-of-the-art SMT solvers based on bit-blasting.
Cite
CITATION STYLE
APA
Jovanović, D. (2017). Solving nonlinear integer arithmetic with MCSAT. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10145 LNCS, pp. 330–346). Springer Verlag. https://doi.org/10.1007/978-3-319-52234-0_18
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Already have an account? Sign in
Sign up for free