Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions

DOI10.1007/978-3-642-31365-3_38zbMath1358.68264arXiv1202.1409OpenAlexW1824587283MaRDI QIDQ2908520

Silvia Tomasi, Roberto Sebastiani

Publication date: 5 September 2012

Published in: Automated Reasoning (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Related Items (16)

Optimization modulo non-linear arithmetic via incremental linearization ⋮ Algebraic program analysis ⋮ Search-Space Partitioning for Parallelizing SMT Solvers ⋮ Solving linear optimization over arithmetic constraint formula ⋮ Optimization Modulo Theories with Linear Rational Costs ⋮ An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty ⋮ Unnamed Item ⋮ Local search with a SAT oracle for combinatorial optimization ⋮ Structured learning modulo theories ⋮ Learning discrete decomposable graphical models via constraint optimization ⋮ An interleaved depth-first search method for the linear optimization problem with disjunctive constraints ⋮ Delegatable Functional Signatures ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ \textsc{OptiMathSAT}: a tool for optimization modulo theories ⋮ A Survey of Satisfiability Modulo Theory ⋮ Iterative and core-guided maxsat solving: a survey and assessment

This page was built for publication: Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions