Splitting on Demand in SAT Modulo Theories

By Clark W. Barrett, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. 2006

125 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks (2017, background): “In practice, splitting can be managed by a SAT engine with splitting-on-demand [1].”
Lazy proofs for DPLL(T)-based SMT solvers (2016, methodology): “Rule Learni models theory solvers following the splitting-on-demand paradigm [5].”
A Unified View of Piecewise Linear Neural Network Verification (2017, methodology): “[11] present a procedure named Reluplex to verify properties of Neural Network containing linear functions and ReLU activation unit, functioning as an SMT solver using the splitting-on-demand framework [1].”
Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure (2006, methodology): “From the extensive literature on SMT techniques, the approach coming closest to ours is the splitting-on-demand technique in SMT of Barett, Nieuwenhuis, Oliv-eras, and Tinelli [1].”
Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic (2014, background): “Range 0 1 [2, 10] [11, 100] [101, 1000] [1000, 2238] total D(n) 32832k 645k 896k 174k 2362 7 34551k ∑ D(n) 0 645k 3677k 3628k 479k 10k 8440k V(n) 30475k 924k 1008k 130k 655 0 32539k ∑ V(n) 0 924k 3900k 2366k 126k 0 7317k”
Handbook of Satisfiability (2021, background): “The approach can be refined to work with several theory solvers when the background theory T is a combination of the solver’s theories [15, 14].”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “At full eﬀort, the theory solver must either produce a lemma (following the splitting-on-demand approach [23]) or determine whether L is sat-isﬁable or not and, in the latter case, produce a conﬂict clause , a clause that is valid in the theory T but is inconsistent with L .”