Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API

DOI10.1007/978-3-319-24318-4_14zbMath1471.68252arXiv1502.02484OpenAlexW746264266MaRDI QIDQ3453224

Uwe Egly, Florian Lonsing

Publication date: 20 November 2015

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

Full work available at URL: https://arxiv.org/abs/1502.02484

Mathematics Subject Classification ID

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

Related Items (2)

Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API ⋮ Computing smallest MUSes of quantified Boolean formulas

Uses Software

• MiniSat
• Chaff
• Glucose
• Bloqqer
• DepQBF
• semprop

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Algorithms for computing minimal unsatisfiable subsets of constraints
• Compressing BMC Encodings with QBF
• Incremental QBF Solving by DepQBF
• On Improving MUS Extraction Algorithms
• Towards efficient MUS extraction
• Ultimately Incremental SAT
• Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
• A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories
• Verification of partial designs using incremental QBF
• Blocked Clause Elimination for QBF
• Theory and Applications of Satisfiability Testing
• Quantified Maximum Satisfiability:
• Factoring Out Assumptions to Speed Up MUS Extraction
• Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction
• Efficient Generation of Unsatisfiability Proofs and Cores in SAT
• Minimal False Quantified Boolean Formulas
• A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

This page was built for publication: Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API