Delta debugging fault-triggering propositional model counting instances
To facilitate debugging of unweighted model counters using SharpVelvet
D.N. COROIAN (TU Delft - Electrical Engineering, Mathematics and Computer Science)
A.L.D. Latour – Mentor (TU Delft - Algorithmics)
M. Skrodzki – Graduation committee member (TU Delft - Computer Graphics and Visualisation)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Propositional model counting (#SAT) is the counting variant of the Boolean Satisfiability (SAT) problem. Development of #SAT solvers has seen a boom in recent years. These tools are complex and hard to debug. To address this, we propose a delta debugger that reduces fault-triggering unweighted model counting instances. Our delta debugger shows an improvement compared to state of the art in the related field of SAT solvers.