MUS Extraction Using Clausal Proofs

DOI10.1007/978-3-319-09284-3_5MaRDI QIDQ3192054zbMATH OpenOpenAlexFDO

Authors Anton Belov, Marijn J. H. Heule, Joao Marques-Silva

Publication date 26 September 2014

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-09284-3_5

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• scientific article; zbMATH DE number 1948188
• scientific article; zbMATH DE number 1765709
• Theorem proving using clausal resolution: from past to present
• Clausal presentation of theories in deduction modulo
• scientific article; zbMATH DE number 1008505
• Program extraction from classical proofs
• Practical program extraction from classical proofs
• scientific article; zbMATH DE number 1301852
• Refinement of classical proofs for program extraction

Cited in

(14)

• Counting minimal unsatisfiable subsets
• Backdoor DNFs
• Accelerated deletion-based extraction of minimal unsatisfiable cores
• Rotation based MSS/MCS enumeration
• Does This Set of Clauses Overlap with at Least One MUS?
• Factoring Out Assumptions to Speed Up MUS Extraction
• Hashing-based approximate counting of minimal unsatisfiable subsets
• Trusted scalable SAT solving with on-the-fly LRAT checking
• Speeding up MUS extraction with preprocessing and chunking
• On improving MUS extraction algorithms
• Towards efficient MUS extraction
• SAT-Based Horn Least Upper Bounds
• MUSer2: an efficient MUS extractor
• Accelerating predicate abstraction by minimum unsatisfiable cores extraction

This page was built for publication: MUS Extraction Using Clausal Proofs

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