A CDCL-style calculus for solving non-linear constraints

DOI10.1007/978-3-030-29007-8_8zbMath1435.68300arXiv1905.09227OpenAlexW2970220778MaRDI QIDQ2180222

Konstantin Korovin, Norbert Th. Müller, Franz Brauße, Margarita Korovina

Publication date: 13 May 2020

Full work available at URL: https://arxiv.org/abs/1905.09227

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items (4)

Optimization modulo non-linear arithmetic via incremental linearization ⋮ Conflict-driven satisfiability for theory combination: lemmas, modules, and proofs ⋮ The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints ⋮ The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints

This page was built for publication: A CDCL-style calculus for solving non-linear constraints