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 solvers based on bit-blasting.
Tue 17 Jan
|10:30 - 11:00|
|11:00 - 11:30|
Roderick BloemInstitute of Software Technology, Graz University of Technology , Hana Chockler, Masoud EbrahimiInstitute of Applied Information Processing and Communications, Graz University of Technology, Ofer StrichmanTechnionFile Attached
|11:30 - 12:00|
Dejan JovanovićSRI International