\textsc{OptiMathSAT}: a tool for optimization modulo theories
From MaRDI portal
Publication:2303246
DOI10.1007/s10817-018-09508-6zbMath1468.68206OpenAlexW3021334088WikidataQ128781501 ScholiaQ128781501MaRDI QIDQ2303246
Patrick Trentin, Roberto Sebastiani
Publication date: 3 March 2020
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-018-09508-6
Multi-objective and goal programming (90C29) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)
Related Items (8)
Optimization modulo non-linear arithmetic via incremental linearization ⋮ Global optimization of objective functions represented by ReLU networks ⋮ Computing optimal hypertree decompositions with SAT ⋮ Solving SAT (and MaxSAT) with a quantum annealer: foundations, encodings, and preliminary results ⋮ MILP, Pseudo-Boolean, and OMT Solvers for Optimal Fault-Tolerant Placements of Relay Nodes in Mission Critical Wireless Networks* ⋮ Optimization modulo the theories of signed bit-vectors and floating-point numbers ⋮ Optimization modulo the theory of floating-point numbers ⋮ OptiMathSAT
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Boolean lexicographic optimization: algorithms \& applications
- A hierarchy of relaxations for linear generalized disjunctive programming
- Deciding floating-point logic with abstract conflict driven clause learning
- Solving constraint satisfaction problems with SAT modulo theories
- Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories
- Structured learning modulo theories
- SCIP: solving constraint integer programs
- Disjunctive programming: Properties of the convex hull of feasible points
- Solving SAT and MaxSAT with a quantum annealer: foundations and a preliminary report
- Propagation via lazy clause generation
- Satisfiability modulo transcendental functions via incremental linearization
- Efficient theory combination via Boolean search
- Optimization in SMT with ${\mathcal LA}$ (ℚ) Cost Functions
- An Abstract Interpretation of DPLL(T)
- Efficient generation of craig interpolants in satisfiability modulo theories
- Optimization Modulo Theories with Linear Rational Costs
- Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
- Minimal-Model-Guided Approaches to Solving Polynomial Constraints and Extensions
- Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
- Solving SAT and SAT Modulo Theories
- Propagation = Lazy Clause Generation
- Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
- Approximating the Pareto Front of Multi-criteria Optimization Problems
- Satisfiability Modulo the Theory of Costs: Foundations and Applications
- Mixed Integer Programming Computation
- Technical Note—Recognizing Unbounded Integer Programs
- A System for Solving Constraint Satisfaction Problems with SMT
- Pushing the Envelope of Optimization Modulo Theories with Linear-Arithmetic Cost Functions
- Theory and Applications of Satisfiability Testing
- The MathSAT5 SMT Solver
- A Modular Approach to MaxSAT Modulo Theories
- Constraint Integer Programming: A New Approach to Integrate CP and MIP
- Symbolic optimization with SMT solvers
- A Parametric Approach for Smaller and Better Encodings of Cardinality Constraints
- On SAT Modulo Theories and Optimization Problems
This page was built for publication: \textsc{OptiMathSAT}: a tool for optimization modulo theories
