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 条
  • [31] Arithmetic Problem Solving
    Stone, Mildred B.
    EDUCATION, 1934, 54 (08): : 505 - 506
  • [32] Problem Solving in Arithmetic
    不详
    SCHOOL AND SOCIETY, 1932, 36 (919): : 189 - 190
  • [33] ARITHMETIC PROBLEM SOLVING
    不详
    TEACHERS COLLEGE RECORD, 1931, 32 (08): : 746 - 747
  • [34] ARITHMETIC PROBLEM SOLVING
    PETERSON, MJ
    ALLER, S
    JOURNAL OF EXPERIMENTAL PSYCHOLOGY, 1971, 91 (01): : 93 - &
  • [35] Problem Solving in Arithmetic
    Osburn, W. J.
    EDUCATIONAL RESEARCH BULLETIN, 1932, 11 (01): : 23 - 24
  • [36] Problem Solving in Arithmetic
    Osburn, W. J.
    Drennan, L. J.
    EDUCATIONAL RESEARCH BULLETIN, 1931, 10 (05): : 123 - 128
  • [37] PROBLEM SOLVING IN ARITHMETIC
    Stevens, B. A.
    JOURNAL OF EDUCATIONAL RESEARCH, 1932, 25 (4-5): : 253 - 260
  • [38] Arithmetic Problem Solving
    Osburn, W. J.
    EDUCATIONAL RESEARCH BULLETIN, 1930, 9 (13): : 375 - 376
  • [39] A Nonlinear Integer Programming Approach to Solving the Robust Parameter Design Optimization Problem
    Ozdemir, Akin
    Cho, Byung Rae
    QUALITY AND RELIABILITY ENGINEERING INTERNATIONAL, 2016, 32 (08) : 2859 - 2870
  • [40] Hybridized neural network and genetic algorithms for solving nonlinear integer programming problem
    Gen, M
    Ida, K
    Lee, CY
    SIMULATED EVOLUTION AND LEARNING, 1999, 1585 : 421 - 429
12345