Efficient Generation of Unsatisfiability Proofs and Cores in SAT

DOI10.1007/978-3-540-89439-1_2zbMATH Open1182.68215OpenAlexW1568765955MaRDI QIDQ5505540FDOQ5505540

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

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

Mathematics Subject Classification ID

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

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

Uses Software

• Chaff
• BerkMin

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)