Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
From MaRDI portal
Publication:2074664
DOI10.1007/s10601-020-09318-xOpenAlexW3126051750MaRDI QIDQ2074664
Ambros M. Gleixner, Jakob Nordström, Jo Devriendt
Publication date: 10 February 2022
Published in: Constraints (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10601-020-09318-x
linear programminginteger programmingcut generationpseudo-Booleanconflict-driven searchcutting plane proofsRoundingSat
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (1)
Uses Software
Cites Work
- Progress in computational mixed integer programming -- a look back from the other side of the tipping point
- Near optimal seperation of tree-like and general resolution
- On the complexity of cutting-plane proofs
- The intractability of resolution
- Modelling discrete optimisation problems in constraint logic programming
- Linear programming: foundations and extensions
- Generalized resolution for 0--1 linear inequalities
- Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers
- In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving
- An effective dynamic programming algorithm for the minimum-cost maximal knapsack packing problem
- Conflict-driven answer set solving: from theory to practice
- Where are the hard knapsack problems?
- Logic-based 0-1 constraint programming
- Conflict analysis in mixed integer programming
- Pebble Games, Proof Complexity, and Time-Space Trade-offs
- Numerically Safe Gomory Mixed-Integer Cuts
- Open-WBO: A Modular MaxSAT Solver,
- Aggregation and Mixed Integer Rounding to Solve MIPs
- The Complexity of Satisfiability of Small Depth Circuits
- Short proofs are narrow—resolution made simple
- GRASP: a search algorithm for propositional satisfiability
- Mixed Integer Programming: Analyzing 12 Years of Progress
- Constraint Integer Programming: A New Approach to Integrate CP and MIP
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
- A machine program for theorem-proving
- The complexity of theorem-proving procedures
- On the complexity of \(k\)-SAT
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
This page was built for publication: Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
