A framework for certified Boolean branch-and-bound optimization

DOI10.1007/S10817-010-9176-ZzbMATH Open1213.68581OpenAlexW2105888199MaRDI QIDQ2429985FDOQ2429985

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

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

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)

Cites Work

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

Cited In (5)

• 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
• QMaxSATpb: a certified MaxSAT solver
• Reducing chaos in SAT-like search: finding solutions close to a given one

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)