Speculative SAT Modulo SAT

被引:0
|
作者
Govind, V. K. Hari [1 ]
Garcia-Contreras, Isabel [1 ]
Shoham, Sharon [2 ]
Gurfinkel, Arie [1 ]
机构
[1] Univ Waterloo, Waterloo, ON, Canada
[2] Tel Aviv Univ, Tel Aviv, Israel
基金
欧洲研究理事会; 加拿大自然科学与工程研究理事会;
关键词
D O I
10.1007/978-3-031-57246-3_4
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
State-of-the-art model-checking algorithms like IC3/PDR are based on uni-directional modular SAT solving for finding and/or blocking counterexamples. Modular SAT-solvers divide a SAT-query into multiple sub-queries, each solved by a separate SAT-solver (called a module), and propagate information (lemmas, proof obligations, blocked clauses, etc.) between modules. While modular solving is key to IC3/PDR, it is obviously not as effective as monolithic solving, especially when individual sub-queries are harder to solve than the combined query. This is partially addressed in SAT modulo SAT (SMS) by propagating unit literals back and forth between the modules and using information from one module to simplify the sub-query in another module as soon as possible (i.e., before the satisfiability of any sub-query is established). However, bi-directionality of SMS is limited because of the strict order between decisions and propagation only one module is allowed to make decisions, until its sub-query is SAT. In this paper, we propose a generalization of SMS, called sPEcSMS, that speculates decisions between modules. This makes it bi-directional decisions are made in multiple modules, and learned clauses are exchanged in both directions. We further extend DRUP proofs and interpolation, these are useful in model checking, to sPEcSMS. We have implemented sPEcSMS in Z3 and empirically validate it on a series of benchmarks that are provably hard for SMS.
引用
收藏
页码:43 / 60
页数:18
相关论文
共 50 条
  • [1] SAT Modulo ODE: A Direct SAT Approach to Hybrid Systems
    Eggers, Andreas
    Fraenzle, Martin
    Herde, Christian
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2008, 5311 : 171 - 185
  • [2] SAT Modulo Monotonic Theories
    Bayless, Sam
    Bayless, Noah
    Hoos, Holger H.
    Hu, Alan J.
    [J]. PROCEEDINGS OF THE TWENTY-NINTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, 2015, : 3702 - 3709
  • [3] SAT Modulo Intuitionistic Implications
    Claessen, Koen
    Rosen, Dan
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, (LPAR-20 2015), 2015, 9450 : 622 - 637
  • [4] An Experiment with Satisfiability Modulo SAT
    Zhang, Hantao
    [J]. JOURNAL OF AUTOMATED REASONING, 2016, 56 (02) : 143 - 154
  • [5] An Experiment with Satisfiability Modulo SAT
    Hantao Zhang
    [J]. Journal of Automated Reasoning, 2016, 56 : 143 - 154
  • [6] SAT Modulo Graphs: Acyclicity
    Gebser, Martin
    Janhunen, Tomi
    Rintanen, Jussi
    [J]. LOGICS IN ARTIFICIAL INTELLIGENCE, JELIA 2014, 2014, 8761 : 137 - 151
  • [7] Decision procedures for SAT, SAT modulo theories and beyond. The BarcelogicTools
    Nieuwenhuis, R
    Oliveras, A
    [J]. LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2005, 3835 : 23 - 46
  • [8] SAT Modulo Theories: Getting the Best of SAT and Global Constraint Filtering
    Nieuwenhuis, Robert
    [J]. PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING-CP 2010, 2010, 6308 : 1 - 2
  • [9] Splitting on demand in SAT modulo theories
    Barrett, Clark
    Nieuwenhuis, Robert
    Oliveras, Albert
    Tinelli, Cesare
    [J]. Logic for Programming, Artificial Intelligence, and Reasoning, Proceedings, 2006, 4246 : 512 - 526
  • [10] SAT Modulo Differential Equation Simulations
    Kolarik, Tomas
    Ratschan, Stefan
    [J]. TESTS AND PROOFS (TAP 2020), 2020, 12165 : 80 - 99