Improving IntSat by expressing disjunctions of bounds as linear constraints

DOI10.3233/AIC-150684MaRDI QIDQ4589125zbMATH OpenOpenAlexFDO

Authors Roberto Asín, Marc Bezem, Robert Nieuwenhuis

Publication date 7 November 2017

Published in AI Communications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/aic-150684

zbMATH Keywords

conflict-driven clause learningconstraint programminginteger linear programmingSAT

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Integer programming (90C10)

Recommendations

• Linearity Constraints as Bounded Intervals in Linear Logic Programming
• Improving linear constraint propagation by changing constraint representation
• scientific article; zbMATH DE number 7378350
• Integer programs for logic constraint satisfaction
• Theory and Applications of Satisfiability Testing
• Enhancing set constraint solvers with lexicographic bounds
• A practical approach to satisfiability modulo linear integer arithmetic
• Building tractable disjunctive constraints

Cited in

(3)

• Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search
• Conflict analysis in mixed integer programming
• IntSat: integer linear programming by conflict-driven constraint learning

This page was built for publication: Improving IntSat by expressing disjunctions of bounds as linear constraints

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