Solving Nonlinear Integer Arithmetic with MCSAT

被引：24
|
作者：
Jovanovic, Dejan [1 ]
机构：
[1] SRI Int, 333 Ravenswood Ave, Menlo Pk, CA 94025 USA
来源：
VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, VMCAI 2017 | 2017年 / 10145卷
基金：
美国国家科学基金会;
关键词：
SAT-SOLVER;
D O I：
10.1007/978-3-319-52234-0_18
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：330 / 346
页数：17
相关论文
共 50 条
  • [1] Experimenting on Solving Nonlinear Integer Arithmetic with Incremental Linearization
    Cimatti, Alessandro
    Griggio, Alberto
    Irfan, Ahmed
    Roveri, Marco
    Sebastiani, Roberto
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2018, 2018, 10929 : 383 - 398
  • [2] Cutting to the Chase Solving Linear Integer Arithmetic
    Jovanovic, Dejan
    de Moura, Leonardo
    AUTOMATED DEDUCTION - CADA-23, 2011, 6803 : 338 - +
  • [3] Towards Verifying Nonlinear Integer Arithmetic
    Beame, Paul
    Liew, Vincent
    COMPUTER AIDED VERIFICATION (CAV 2017), PT II, 2017, 10427 : 238 - 258
  • [4] Toward Verifying Nonlinear Integer Arithmetic
    Beame, Paul
    Liew, Vincent
    JOURNAL OF THE ACM, 2019, 66 (03)
  • [5] A scalable method for solving satisfiability of integer linear arithmetic logic
    Sheini, HM
    Sakallah, KA
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 : 241 - 256
  • [6] Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
    Habermehl, Peter
    Havlena, Vojtech
    Hecko, Michal
    Holik, Lukas
    Lengal, Ondrej
    COMPUTER AIDED VERIFICATION, PT I, CAV 2024, 2024, 14681 : 42 - 67
  • [7] Solving Bitvectors with MCSAT: Explanations from Bits and Pieces
    Graham-Lengrand, Stephane
    Jovanovic, Dejan
    Dutertre, Bruno
    AUTOMATED REASONING, PT I, 2020, 12166 : 103 - 121
  • [8] Solving a nonlinear integer program for allocating resources
    Liu, Y. H.
    Chuang, J. M.
    Hwang, Ming-Hu
    MATHEMATICAL AND COMPUTER MODELLING, 2006, 44 (3-4) : 377 - 381
  • [9] Solving nonlinear systems by constraint inversion and interval arithmetic
    Ceberio, M
    Granvilliers, L
    ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION, 2001, 1930 : 127 - 141
  • [10] Widening integer arithmetic
    Redwine, K
    Ramsey, N
    COMPILER CONSTRUCTION, PROCEEDINGS, 2004, 2985 : 232 - 249
12345