IntSat: integer linear programming by conflict-driven constraint learning

DOI10.1080/10556788.2023.2246167MaRDI QIDQ6585824zbMATH OpenFDO

Authors Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell

Publication date 12 August 2024

Published in Optimization Methods \& Software (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1080/10556788.2023.2246167

Mathematics Subject Classification ID

Integer programming (90C10)

Recommendations

• Improving IntSat by expressing disjunctions of bounds as linear constraints
• Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
• Conflict analysis in mixed integer programming
• Learning from conflicts in propositional satisfiability
• Conflict-Driven Heuristics for Mixed Integer Programming

Cites work

• A complete and terminating approach to linear integer solving
• A Computing Procedure for Quantification Theory
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• A machine program for theorem-proving
• A reduction from unbounded linear mixed arithmetic problems into bounded problems
• Analysis of mathematical programming problems prior to applying the simplex algorithm
• Comparing integer linear programming to SAT-solving for hard problems in computational and systems biology
• Computational aspects of infeasibility analysis in mixed integer programming
• Conflict analysis in mixed integer programming
• Cutting to the chase.
• Experiments with conflict analysis in mixed integer programming
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Improving IntSat by expressing disjunctions of bounds as linear constraints
• Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
• The complexity of theorem-proving procedures
• The intractability of resolution

Cited in

(4)

• Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
• Local rapid learning for integer programs
• A parallel branch-and-bound-and-check algorithm for nesting
• Resolution meets cutting planes: introducing hypercube linear resolution

This page was built for publication: IntSat: integer linear programming by conflict-driven constraint learning

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