82 citations · 369 across the 63 of their papers we have counts for
77 papers
SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
Jialiang Sun, Kuldeep Meel
Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem diff…
Provably Tractable NFA-Constrained Language Generation via HMMs
Jialiang Sun, Kuldeep Meel
Constrained generation aims to sample from language models (LMs) conditioned on hard constraints. Existing constrained-generation techniques for nondeterministic finite automaton (…
Scaling Zero Knowledge UNSAT Verification via Normalized Chaining
Ashwin Karthikeyan, Ethan Kharitonov, Kuldeep S. Meel +1
Proofs of UNSAT are a standard primitive in formal verification and software assurance. In many real-world settings, the proof itself encodes proprietary or security-sensitive info…
Quantifying Sensitivity for Tree Ensembles: A symbolic and compositional approach
Ajinkya Naik, Chaitanya Garg, S. Akshay +2
Decision tree ensembles (DTE) are a popular model for a wide range of AI classification tasks, used in multiple safety critical domains, and hence verifying properties on these mod…
The Limitations and Power of NP-Oracle-Based Functional Synthesis Techniques
Brendan Juba, Kuldeep S. Meel
Given a Boolean relational specification between inputs and outputs, the problem of functional synthesis is to construct a function that maps each assignment of the input to an ass…
Towards Practical Zero-Knowledge Proof for PSPACE
Ashwin Karthikeyan, Hengyu Liu, Kuldeep S. Meel +1
Efficient zero-knowledge proofs (ZKPs) have been restricted to NP statements so far, whereas they exist for all statements in PSPACE. This work presents the first practical zero-kn…
Counting Answer Sets of Disjunctive Answer Set Programs
Mohimenul Kabir, Supratik Chakraborty, Kuldeep S Meel
Answer Set Programming (ASP) provides a powerful declarative paradigm for knowledge representation and reasoning. Recently, counting answer sets has emerged as an important computa…
A Simple and Effective ASP-Based Tool for Enumerating Minimal Hitting Sets
Mohimenul Kabir, Kuldeep S Meel
The hitting set problem is a fundamental problem in computer science and mathematics. Given a family of sets over a universe of elements, a minimal hitting set is a subset-minimal…
An ASP-Based Framework for MUSes
Mohimenul Kabir, Kuldeep S Meel
Given an unsatisfiable formula, understanding the core reason for unsatisfiability is crucial in several applications. One effective way to capture this is through the minimal unsa…
Efficient Certified Reasoning for Binarized Neural Networks
Jiong Yang, Yong Kiam Tan, Mate Soos +2
Neural networks have emerged as essential components in safety-critical applications -- these use cases demand complex, yet trustworthy computations. Binarized Neural Networks (BNN…
Scalable Counting of Minimal Trap Spaces and Fixed Points in Boolean Networks
Mohimenul Kabir, Van-Giang Trinh, Samuel Pastva +1
Boolean Networks (BNs) serve as a fundamental modeling framework for capturing complex dynamical systems across various domains, including systems biology, computational logic, and…
CNFs and DNFs with Exactly Solutions
L. Sunil Chandran, Rishikesh Gajjala, Kuldeep S. Meel
Model counting is a fundamental problem that consists of determining the number of satisfying assignments for a given Boolean formula. The weighted variant, which computes the weig…
On Top-Down Pseudo-Boolean Model Counting
Suwei Yang, Yong Lai, Kuldeep S. Meel
Pseudo-Boolean model counting involves computing the number of satisfying assignments of a given pseudo-Boolean (PB) formula. In recent years, PB model counting has seen increased…
Formally Solving Answer-Construction Problems in Lean
Jialiang Sun, Yuzhi Tang, Ao Li +2
Large language models (LLMs) have achieved remarkable progress in formal mathematical reasoning. Mathematical competition problems fall into two broad types: theorem-proving proble…
Towards Practical First-Order Model Counting
Ananth K. Kidambi, Guramrit Singh, Paulius Dilkas +1
First-order model counting (FOMC) is the problem of counting the number of models of a sentence in first-order logic. Since lifted inference techniques rely on reductions to varian…
Probabilistic Explanations for Linear Models
Bernardo Subercaseaux, Marcelo Arenas, Kuldeep S Meel
Formal XAI is an emerging field that focuses on providing explanations with mathematical guarantees for the decisions made by machine learning models. A significant amount of work…
Towards Projected and Incremental Pseudo-Boolean Model Counting
Suwei Yang, Kuldeep S. Meel
Model counting is a fundamental task that involves determining the number of satisfying assignments to a logical formula, typically in conjunctive normal form (CNF). While CNF mode…
Engineering an Efficient Approximate DNF-Counter
Mate Soos, Uddalok Sarkar, Divesh Aggarwal +3
Model counting is a fundamental problem in many practical applications, including query evaluation in probabilistic databases and failure-probability estimation of networks. In thi…
The Cardinality of Identifying Code Sets for Soccer Ball Graph with Application to Remote Sensing
Anna L. D. Latour, Arunabha Sen, Kaustav Basu +2
In the context of satellite monitoring of the earth, we can assume that the surface of the earth is divided into a set of regions. We assume that the impact of a big social/environ…
On Lower Bounding Minimal Model Count
Mohimenul Kabir, Kuldeep S Meel
Minimal models of a Boolean formula play a pivotal role in various reasoning tasks. While previous research has primarily focused on qualitative analysis over minimal models; our s…
#CFG and #DNNF admit FPRAS
Kuldeep S. Meel, Alexis de Colnet
We provide the first fully polynomial-time randomized approximation scheme for the following two counting problems: 1. Given a Context Free Grammar over alphabet , count the…
An FPRAS for Model Counting for Non-Deterministic Read-Once Branching Programs
Kuldeep S. Meel, Alexis de Colnet
Non-deterministic read-once branching programs, also known as non-deterministic free binary decision diagrams (nFBDD), are a fundamental data structure in computer science for repr…
Auditable Algorithms for Approximate Model Counting
Kuldeep S. Meel, Supratik Chakraborty, S. Akshay
Model counting, or counting the satisfying assignments of a Boolean formula, is a fundamental problem with diverse applications. Given #P-hardness of the problem, developing algori…
Exact ASP Counting with Compact Encodings
Mohimenul Kabir, Supratik Chakraborty, Kuldeep S Meel
Answer Set Programming (ASP) has emerged as a promising paradigm in knowledge representation and automated reasoning owing to its ability to model hard combinatorial problems from…