Delta debugging fault-triggering propositional model counting instances

To facilitate debugging of unweighted model counters using SharpVelvet

Bachelor thesis (2025)

Authors

D.N. COROIAN Electrical Engineering, Mathematics and Computer Science

Contributors

A.L.D. Latour Algorithmics (mentor)
M. Skrodzki Computer Graphics and Visualisation (graduation committee member)
Faculty
Electrical Engineering, Mathematics and Computer Science
More Info
expand_more

Published Date

31-01-2025

Language

English

Reuse Rights

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.

Faculty

Electrical Engineering, Mathematics and Computer Science

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.

Files

Cse3000_deltamc_davidcoroian.p... (pdf)
(pdf | 0.199 Mb)
Unknown license