Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions

DOI10.1007/978-3-662-46681-0_27zbMath1420.68197arXiv1410.5568OpenAlexW1544041853MaRDI QIDQ5194955

Roberto Sebastiani, Patrick Trentin

Publication date: 17 September 2019

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

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

zbMATH Keywords

cost functionunit clausetruth assignmentbound model checkincremental version

Mathematics Subject Classification ID

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

Related Items (7)

Optimization modulo non-linear arithmetic via incremental linearization ⋮ Global optimization of objective functions represented by ReLU networks ⋮ Structured learning modulo theories ⋮ Delegatable Functional Signatures ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ Optimization modulo the theory of floating-point numbers

This page was built for publication: Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions