Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
type: Item
instance of: scholarly article
title: Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
author: Jo Devriendt
author: Ambros M. Gleixner
author: Jakob Nordstrom
published in: Constraints
publication date: 2022-02-10T00:00:00Z
Mathematics Subject Classification ID: 68T20
Mathematics Subject Classification ID: 90C27
Mathematics Subject Classification ID: 03F20
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 90C11
zbMATH DE Number: 7471952
zbMATH Keywords: pseudo-Boolean
zbMATH Keywords: conflict-driven search
zbMATH Keywords: cutting plane proofs
zbMATH Keywords: integer programming
zbMATH Keywords: linear programming
zbMATH Keywords: cut generation
zbMATH Keywords: RoundingSat
describes a project that uses: OPBDP
describes a project that uses: Sat4j
describes a project that uses: Open-WBO
describes a project that uses: Chaff
describes a project that uses: SCIP
describes a project that uses: MIPLIB
describes a project that uses: Gurobi
describes a project that uses: Pueblo
describes a project that uses: CPLEX
MaRDI profile type: Publication
full work available at URL: s10601-020-09318-x
OpenAlex ID: W3126051750
cites work: Conflict analysis in mixed integer programming
cites work: Constraint Integer Programming: A New Approach to Integrate CP and MIP
cites work: Mixed Integer Programming: Analyzing 12 Years of Progress
cites work: Logic-based 0-1 constraint programming
cites work: Modelling discrete optimisation problems in constraint logic programming
cites work: Q5715680
cites work: Near optimal seperation of tree-like and general resolution
cites work: Short proofs are narrow—resolution made simple
cites work: Progress in computational mixed integer programming -- a look back from the other side of the tipping point
cites work: Q5769706
cites work: The Complexity of Satisfiability of Small Depth Circuits
cites work: The complexity of theorem-proving procedures
cites work: On the complexity of cutting-plane proofs
cites work: Numerically safe Gomory mixed-integer cuts
cites work: Q3844775
cites work: A machine program for theorem-proving
cites work: A Computing Procedure for Quantification Theory
cites work: Q3429154
cites work: Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers
cites work: An effective dynamic programming algorithm for the minimum-cost maximal knapsack packing problem
cites work: Conflict-driven answer set solving: from theory to practice
cites work: The intractability of resolution
cites work: Generalized resolution for 0--1 linear inequalities
cites work: On the complexity of \(k\)-SAT
cites work: Q4071737
cites work: Aggregation and Mixed Integer Rounding to Solve MIPs
cites work: GRASP: a search algorithm for propositional satisfiability
cites work: Open-WBO: A Modular MaxSAT Solver,
cites work: Pebble games, proof complexity, and time-space trade-offs
cites work: Where are the hard knapsack problems?
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Q3429161
cites work: Linear programming: foundations and extensions
cites work: In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving
DOI: 10.1007/S10601-020-09318-X
description: scientific article; zbMATH DE number 7471952