An approach for extracting a small unsatisfiable core

DOI10.1007/s10703-008-0051-zzbMath1165.68487OpenAlexW2126900870MaRDI QIDQ1028724

Roman Gershman, Ofer Strichman, Maya Koifman

Publication date: 6 July 2009

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-008-0051-z

zbMATH Keywords

resolutionSATunsatisfiable core

Mathematics Subject Classification ID

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

Related Items (3)

Accelerating predicate abstraction by minimum unsatisfiable cores extraction ⋮ Faster Extraction of High-Level Minimal Unsatisfiable Cores ⋮ Accelerated Deletion-based Extraction of Minimal Unsatisfiable Cores

Uses Software

• SATIRE
• CVC
• MUP
• AMUSE

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• The complexity of facets resolved
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• Local-search extraction of mUSes
• A fast algorithm for finding dominators in a flowgraph
• Proof-guided underapproximation-widening for multi-process systems
• Computer Aided Verification
• Algorithms – ESA 2004
• A Machine-Oriented Logic Based on the Resolution Principle
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

This page was built for publication: An approach for extracting a small unsatisfiable core