-
Article
Hashing-based approximate counting of minimal unsatisfiable subsets
In many areas of computer science, we are given an unsatisfiable Boolean formula F in CNF, i.e. a set of clauses, with the goal to analyse the unsatisfiability. Examination of minimal unsatisfiable subsets (MUSes...
-
Chapter and Conference Paper
Rounding Meets Approximate Model Counting
The problem of model counting, also known as \(\#\textsf{SAT}\) , is to compute the number of models or satisfying assignments o...
-
Chapter and Conference Paper
Projected Model Counting: Beyond Independent Support
Given a system of constraints over a set X of variables, projected model counting asks us to count satisfying assignments of the constraint system projected on a subset
-
Chapter and Conference Paper
A Scalable Shannon Entropy Estimator
Quantified information flow (QIF) has emerged as a rigorous approach to quantitatively measure confidentiality; the information-theoretic underpinning of QIF allows the end-users to link the computed quantitie...
-
Chapter and Conference Paper
On the Usefulness of Linear Modular Arithmetic in Constraint Programming
Linear modular constraints are a powerful class of constraints that arise naturally in cryptanalysis, checksums, hash functions, and the like. Given their importance, the past few years have witnessed the desi...
-
Chapter and Conference Paper
Leveraging GPUs for Effective Clause Sharing in Parallel SAT Solving
The past two decades have witnessed an unprecedented improvement in runtime performance of SAT solvers owing to clever software engineering and creative design of data structures. Yet, most entries in the annu...
-
Chapter and Conference Paper
Counting Minimal Unsatisfiable Subsets
Given an unsatisfiable Boolean formula F in CNF, an unsatisfiable subset of clauses U of F is called Minimal Unsatisfiable Subset (MUS) if every proper subset of U is satisfiable. Since MUSes serve as explanation...
-
Chapter and Conference Paper
Approximate Counting of Minimal Unsatisfiable Subsets
Given an unsatisfiable formula F in CNF, i.e. a set of clauses, the problem of Minimal Unsatisfiable Subset (MUS) seeks to identify a minimal subset of clauses
-
Chapter and Conference Paper
Manthan: A Data-Driven Approach for Boolean Function Synthesis
Boolean functional synthesis is a fundamental problem in computer science with wide-ranging applications and has witnessed a surge of interest resulting in progressively improved techniques over the past decad...
-
Chapter and Conference Paper
On the Sparsity of XORs in Approximate Model Counting
Given a Boolean formula \(\varphi \) , the problem of model counting, also referred to as #SAT, is to compute the number of solutions of \(\varphi \) . The hashing-based techniques for approximate counting have...
-
Chapter and Conference Paper
A Study of Symmetry Breaking Predicates and Model Counting
Propositional model counting is a classic problem that has recently witnessed many technical advances and novel applications. While the basic model counting problem requires computing the number of all solutio...
-
Chapter and Conference Paper
Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling
Given a Boolean formula, the problem of counting seeks to estimate the number of solutions of F while the problem of uniform sampling seeks to sample solutions uniformly at random. Counting and uniform sampling a...
-
Chapter and Conference Paper
Designing New Phase Selection Heuristics
CDCL-based SAT solvers have transformed the field of automated reasoning owing to their demonstrated efficiency at handling problems arising from diverse domains. The success of CDCL solvers is owed to the des...
-
Chapter and Conference Paper
Phase Transition Behavior in Knowledge Compilation
The study of phase transition behaviour in SAT has led to deeper understanding and algorithmic improvements in modern SAT solvers. Motivated by these prior studies of phase transitions in SAT, we seek to study...
-
Article
Not all FPRASs are equal: demystifying FPRASs for DNF-counting
The problem of counting the number of solutions of a DNF formula, also called #DNF, is a fundamental problem in artificial intelligence with applications in diverse domains ranging from network reliability to ...
-
Chapter and Conference Paper
Correction to: Dual Hashing-Based Algorithms for Discrete Integration
In the version of this paper that was originally published, reference was made to an incorrect grant number. This has now been corrected.
-
Chapter and Conference Paper
Correction to: \(\mathsf {WAPS}\) : Weighted and Projected Sampling
In the version of this paper that was originally published, there was an error in the acknowledgement at the bottom of the first page. “AI Singapore Grant [R-252-000-A16-490]” was mentioned instead of “Nationa...
-
Chapter and Conference Paper
Assessing Heuristic Machine Learning Explanations with Model Counting
Machine Learning (ML) models are widely used in decision making procedures in finance, medicine, education, etc. In these areas, ML outcomes can directly affect humans, e.g. by deciding whether a person should...
-
Chapter and Conference Paper
\(\mathsf {CrystalBall}\) : Gazing in the Black Box of SAT Solving
Boolean satisfiability is a fundamental problem in computer science with a wide range of applications including planning, configuration management, design and verification of software/hardware systems
-
Chapter and Conference Paper
Dual Hashing-Based Algorithms for Discrete Integration
Given a boolean formula F and a weight function \(\rho \) , the problem of discrete integration seeks to co...
