Learn to relax: integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search

DOI10.1007/S10601-020-09318-XMaRDI QIDQ2074664zbMATH OpenOpenAlexFDO

Authors Jo Devriendt, Ambros M. Gleixner, Jakob Nordstrom

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

zbMATH Keywords

conflict-driven searchcut generationcutting plane proofsinteger programminglinear programmingpseudo-BooleanRoundingSat

Mathematics Subject Classification ID

Complexity of proofs (03F20) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mixed integer programming (90C11) Combinatorial optimization (90C27)

Recommendations

• IntSat: integer linear programming by conflict-driven constraint learning
• scientific article; zbMATH DE number 5139167
• On using cutting planes in pseudo-Boolean optimization
• Conflict analysis in mixed integer programming
• Improving IntSat by expressing disjunctions of bounds as linear constraints

Cites work

• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• A Machine-Oriented Logic Based on the Resolution Principle
• Aggregation and Mixed Integer Rounding to Solve MIPs
• An effective dynamic programming algorithm for the minimum-cost maximal knapsack packing problem
• Conflict analysis in mixed integer programming
• Conflict-driven answer set solving: from theory to practice
• Constraint Integer Programming: A New Approach to Integrate CP and MIP
• Generalized resolution for 0--1 linear inequalities
• GRASP: a search algorithm for propositional satisfiability
• scientific article; zbMATH DE number 5139161 (Why is no real title available?)
• scientific article; zbMATH DE number 5139167 (Why is no real title available?)
• scientific article; zbMATH DE number 3177183 (Why is no real title available?)
• scientific article; zbMATH DE number 3489106 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• scientific article; zbMATH DE number 3029852 (Why is no real title available?)
• In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving
• Linear programming: foundations and extensions
• Logic-based 0-1 constraint programming
• Mixed integer programming: analyzing 12 years of progress
• Modelling discrete optimisation problems in constraint logic programming
• Near optimal seperation of tree-like and general resolution
• Numerically safe Gomory mixed-integer cuts
• On the complexity of k-SAT
• On the complexity of cutting-plane proofs
• Open-WBO: a modular MaxSAT solver
• Pebble games, proof complexity, and time-space trade-offs
• Progress in computational mixed integer programming -- a look back from the other side of the tipping point
• Short proofs are narrow—resolution made simple
• The complexity of satisfiability of small depth circuits
• The complexity of theorem-proving procedures
• The intractability of resolution
• Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers
• Where are the hard knapsack problems?

Cited in

(6)

• Multiple-choice knapsack constraint in graphical models
• IntSat: integer linear programming by conflict-driven constraint learning
• Using execution logs for improving pseudo-Boolean propagation
• Speeding up pseudo-Boolean propagation
• Engineering and evaluating multi-objective pseudo-Boolean optimizers
• Improving local search algorithm for pseudo Boolean optimization

Describes a project that uses

Uses Software

• OPBDP
• Sat4j
• Open-WBO
• Chaff
• SCIP
• MIPLIB
• Gurobi
• Pueblo
• CPLEX

This page was built for publication: Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2074664)