Accelerated deletion-based extraction of minimal unsatisfiable cores

DOI10.3233/SAT190100MaRDI QIDQ5015593zbMATH OpenOpenAlexFDO

Authors Alexander Nadel, Vadim Ryvchin, Ofer Strichman

Publication date 9 December 2021

Published in Journal on Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/sat190100

zbMATH Keywords

minimal high-level unsat coreminimal unsat coreresolution

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• MUS Extraction Using Clausal Proofs
• On getting rid of the preprocessing minimization step in MUC-finding algorithms
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• On improving MUS extraction algorithms

Cites work

• A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• Algorithms for computing minimal unsatisfiable subsets of constraints
• An approach for extracting a small unsatisfiable core
• Approximating minimal unsatisfiable subformulae by means of adaptive core search
• Efficient combination of decision procedures for MUS computation
• Efficient Generation of Unsatisfiability Proofs and Cores in SAT
• Factoring Out Assumptions to Speed Up MUS Extraction
• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Finding Guaranteed MUSes Fast
• scientific article; zbMATH DE number 5510691 (Why is no real title available?)
• scientific article; zbMATH DE number 1956569 (Why is no real title available?)
• scientific article; zbMATH DE number 1852147 (Why is no real title available?)
• scientific article; zbMATH DE number 2243370 (Why is no real title available?)
• Interpolation and SAT-based model checking.
• Locating Minimal Infeasible Constraint Sets in Linear Programs
• MUSer2: an efficient MUS extractor
• On improving MUS extraction algorithms
• Temporal induction by incremental SAT solving
• The complexity of facets resolved
• Theory and Applications of Satisfiability Testing
• Towards efficient MUS extraction
• Using heuristics to find minimal unsatisfiable subformulas in satisfiability problems
• Using local search to find MSSes and MUSes

Cited in

(8)

• Faster Extraction of High-Level Minimal Unsatisfiable Cores
• Anytime answer set optimization via unsatisfiable core shrinking
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction
• Hashing-based approximate counting of minimal unsatisfiable subsets
• Rotation based MSS/MCS enumeration
• Cost-minimal parameter correction subsets for unsatisfiable constraint problems
• Counting minimal unsatisfiable subsets
• On getting rid of the preprocessing minimization step in MUC-finding algorithms

This page was built for publication: Accelerated deletion-based extraction of minimal unsatisfiable cores

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