A framework for certified Boolean branch-and-bound optimization

DOI10.1007/S10817-010-9176-ZMaRDI QIDQ2429985zbMATH OpenOpenAlexFDO

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

Publication date 5 April 2011

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-010-9176-z

zbMATH Keywords

optimizationSAT

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Polyhedral combinatorics, branch-and-bound, branch-and-cut (90C57)

Recommendations

• Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
• optsat: A Tool for Solving SAT Related Optimization Problems
• Complexity results on DPLL and resolution
• A tight bound for the boolean quadratic optimization problem and its use in a branch and bound algorithm¹
• Search techniques for SAT-based Boolean optimization

Cites work

• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• A logical approach to efficient Max-SAT solving
• A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
• Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
• Efficient Generation of Unsatisfiability Proofs and Cores in SAT
• scientific article; zbMATH DE number 4089320 (Why is no real title available?)
• MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
• On SAT Modulo Theories and Optimization Problems
• Pseudo-Boolean optimization
• Radio link frequency assignment
• Rocket-Fast Proof Checking for SMT Solvers
• Roof duality, complementation and persistency in quadratic 0–1 optimization
• Satisfiability-based algorithms for Boolean optimization
• SATLIB: An online resource for research on SAT

Cited in

(7)

• QMaxSATpb: a certified MaxSAT solver
• Reducing chaos in SAT-like search: finding solutions close to a given one
• Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
• Curriculum-based course timetabling with SAT and MaxSAT
• Certified Core-Guided MaxSAT Solving
• A verified SAT solver framework including optimization and partial valuations
• Certified MaxSAT preprocessing

Describes a project that uses

Uses Software

• MaxSolver
• SATLIB
• CPLEX
• GLPK

This page was built for publication: A framework for certified Boolean branch-and-bound optimization

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