Efficient Generation of Unsatisfiability Proofs and Cores in SAT

DOI10.1007/978-3-540-89439-1_2MaRDI QIDQ5505540zbMATH OpenOpenAlexFDO

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

Publication date 27 January 2009

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-89439-1_2

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Practical algorithms for unsatisfiability proof and core generation in SAT solvers
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Cores in core based MaxSat algorithms: an analysis

Cited in

(9)

• A framework for certified Boolean branch-and-bound optimization
• Accelerating logic-based benders decomposition for railway rescheduling by exploiting similarities in delays
• Guiding high-performance SAT solvers with unsat-core predictions
• Branch and Bound for Boolean Optimization and the Generation of Optimality Certificates
• Accelerated deletion-based extraction of minimal unsatisfiable cores
• Practical algorithms for unsatisfiability proof and core generation in SAT solvers
• A logic-based Benders decomposition for microscopic railway timetable planning
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API

Describes a project that uses

Uses Software

• BerkMin
• Chaff

This page was built for publication: Efficient Generation of Unsatisfiability Proofs and Cores in SAT

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