Kuldeep S. MeelAssistant Professor

I am starting in Jan 2018 as an Assistant Professor in the Computer Science Department of School of Computing at
National University of Singapore.
My research is centered on the design of computational techniques for constrained sampling and counting, probabilistic reasoning, and machine learning with applications to diverse domains such as power grid resilience, hardware and software verification.
1 
CountingBased Reliability Estimation for PowerTransmission Grids
Proceedings of AAAI Conference on Artificial Intelligence (AAAI), 2017.
Modern society is increasingly reliant on the functionality of infrastructure facilities and utility services. Consequently, there has been surge of interest in the problem of quantification of system reliability, which is known to be #Pcomplete. Reliability also contributes to the resilience of systems, so as to effectively make them bounce back after contingencies. Despite diverse progress, most techniques to estimate system reliability and resilience remain computationally expensive. In this paper, we investigate how recent advances in hashingbased approaches to counting can be exploited to improve computational techniques for system reliability. The primary contribution of this paper is a novel framework, RelNet, that provides provably approximately correct (PAC) estimates for arbitrary networks. We then apply RelNet to ten real world power transmission grids across different cities in the U.S. and are able to obtain, to the best of our knowledge, the first theoretically sound a priori estimates of reliability between several pairs of nodes of interest. Such estimates will help managing uncertainty and support rational decision making for community resilience.

2 
Algorithmic Improvements in Approximate Counting for Probabilistic Inference:
From Linear to Logarithmic SAT Calls
Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), 2016.
Probabilistic inference via model counting has emerged as a scalable technique with strong formal guarantees, thanks to recent advances in hashingbased approximate counting. Stateoftheart hashingbased counting algorithms use an {\NP} oracle, such that the number of oracle invocations grows linearly in the number of variables n in the input constraint. We present a new approach to hashingbased approximate model counting in which the number of oracle invocations grows logarithmically in $n$, while still providing strong theoretical guarantees. Our experiments show that the new approach outperforms stateoftheart techniques for approximate counting by 12 orders of magnitude in running time.

3 
On Computing Minimal Independent Support and Its Applications to Sampling and Counting
Proceedings of International Conference on Constraint Programming (CP), 2015. Best Student Paper Award
Constrained sampling and counting are two fundamental problems arising in domains ranging from artificial intelligence and security, to hardware and software testing. Recent approaches to approximate solutions for these problems rely on employing SAT solvers and universal hash functions that are typically encoded as XOR constraints of length n/2 for an input formula with n variables. As the runtime performance of SAT solvers heavily depends on the length of XOR constraints, recent research effort has been focused on reduction of length of XOR constraints. Consequently, a notion of Independent Support was proposed, and it was shown that constructing XORs over independent support (if known) can lead to a significant reduction in the length of XOR constraints without losing the theoretical guarantees of sampling and counting algorithms. In this paper, we present the first algorithmic procedure (and a corresponding tool, called MIS) to determine minimal independent support for a given CNF formula by employing a reduction to group minimal unsatisfiable subsets (GMUS). By utilizing minimal independent supports computed by MIS, we provide new tighter bounds on the length of XOR constraints for constrained counting and sampling. Furthermore, the universal hash functions constructed from independent supports computed by MIS provide two to three orders of magnitude performance improvement in stateoftheart constrained sampling and counting tools, while still retaining theoretical guarantees.

4 
DistributionAware Sampling and Weighted Model Counting for SAT
Proceedings of AAAI Conference on Artificial Intelligence (AAAI), 2014.
Given a CNF formula and a weight for each assignment of values to variables, two natural problems are weighted model counting and distributionaware sampling of satisfying assignments. Both problems have a wide variety of important applications. Due to the inherent complexity of the exact versions of the problems, interest has focused on solving them approximately. Prior work in this area scaled only to small problems in practice, or failed to provide strong theoretical guarantees, or employed a computationallyexpensive maximum a posteriori probability (MAP) oracle that assumes prior knowledge of a factored representation of the weight distribution. We present a novel approach that works with a blackbox oracle for weights of assignments and requires only an {\NP}oracle (in practice, a SATsolver) to solve both the counting and sampling problems. Our approach works under mild assumptions on the distribution of weights of satisfying assignments, provides strong theoretical guarantees, and scales to problems involving several thousand variables. We also show that the assumptions can be significantly relaxed while improving computational efficiency if a factored representation of the weights is known.

S. Akshay and I are organizing workshop on probabilistic reasoning and formal methods at FSTTCS 2017 on Dec 11.
Our Paper on DNF counting is accepted at FSTTCS 2017. Congratulations Aditya for his first paper.
Submitted paper on DNF counting to FSTTCS 2017
Successfully defended PhD thesis!