“Kuldeep

Kuldeep S. Meel

Sung Kah Kay Assistant Professor
Affiliate, Institute of Data Science
Computer Science Department, School of Computing
National University of Singapore
Office: COM2-03-41
Phone (O): +65-651 61422
Email: meel@comp.nus.edu.sg
Please consult my calendar before suggesting a meeting time.
Research Group Website

Short Bio

Kuldeep Meel is an Assistant Professor in the Computer Science Department of School of Computing at National University of Singapore, where he holds Sung Kah Kay Assistant Professorship. The broader goal of his research is to advance artificial intelligence techniques, which utilize ubiquity of data and formal methods, to enable computing to deal with increasingly uncertain real-world environments.

Open Positions

  • Looking for candidates with strong background in CS/Mathematics/Physics for post-doc for the project: Beyond NP Revolution. Read advertisement for more details.
  • Two post-doc positions available in the broad area of applying machine learning to SAT solvers, approximate counting techniques, and CP. Read advertisement for more details.
  • We are always looking for highly motivated Ph.D. students, research assistants with time commitment of at least 6 months and summer internship for exceptional undergraduate interns in our group. Read this before sending me an email.

[top]

Research Interests

  • Constrained Sampling and Counting         
  • Artificial Intelligence
  • Formal Methods for Verification of AI Systems
  • Interpretable and Explainable Models

[top]

Students & Postdocs

Research Group Website
I am proud of my highly motivated students and postdocs:
  • Teodora Baluta, PhD Student, co-advised with Prateek Saxena
  • Bishwamittra Ghosh, PhD Student
  • Priyanka Golia, Joint NUS-IITK PhD Student, co-advised with Subhajit Roy (IITK)
  • Yash Pote, PhD Student

  • Lorenzo Ciampiconi, MS@Politecnico di Milano (expected: May 2019)
  • Rahul Gupta, BTech+MTech@IITK (expected: May 2019) , co-advised with Subhajit Roy (IITK)
  • Shubham Sharma, BTech+MTech@IITK (expected: May 2019), co-advised with Subhajit Roy (IITK)

  • Mohimenul Kabir, Research Assistant (since: September 2018)
  • Himanshu Arora, Research Assistant (since: Feb 2019)

  • Do Andre Khoi Nguyen, Undergraduate Researcher (since: May 2018)
  • Yang Suwei, Undergraduate Researcher (since: July 2018)

Alumni

  • Alexis de Colnet, MComp@NUS (Graduated: Dec 2018)
  • Dr. Mate Soos, Research Fellow (March 2018 -- June 2018)
  • Bhavishya, Summer Intern (May 2018 - July 2018)

[top]

Teaching

[top]

Awards and Honors

[top]

Selected Recent Publications

Google Scholar
Except for [1], the names of authors are sorted alphabetically and the order does not reflect contribution.
1
BIRD: Engineering an Efficient CNF-XOR SAT Solver and its Applications to Approximate Model Counting
Mate Soos and Kuldeep S. Meel
Proceedings of AAAI Conference on Artificial Intelligence (AAAI), 2019.
Given a Boolean formula F, the problem of model counting, also referred to as #SAT is to compute the number of solutions of F. Model counting is a fundamental problem in artificial intelligence with a wide range of applications including probabilistic reasoning, decision making under uncertainty, quantified information flow, and the like. Motivated by the success of SAT solvers, there has been surge of interest in the design of hashing-based techniques for approximate model counting for the past decade. We profiled the state of the art approximate model counter ApproxMC3 and observed that over 99.99% of time is consumed by the underlying SAT solver, CryptoMinisat. This observation motivated us to ask: Can we design an efficient underlying CNF-XOR SAT solver that can take advantage of the structure of hashing-based algorithms and would this lead to an efficient approximate model counter? The primary contribution of this paper is an affirmative answer to the above question. We present a novel architecture, called BIRD, to handle CNF-XOR formulas arising from hashing-based techniques. The resulting hashing-based approximate model counter, called ApproxMC3, employs the BIRD framework in its underlying SAT solver, CryptoMinisat. To the best of our knowledge, we conducted the most comprehensive study of evaluation performance of counting algorithms involving 1896 benchmarks with computational effort totaling 86400 computational hours. Our experimental evaluation demonstrates significant runtime performance improvement for ApproxMC3 over ApproMC2. In particular, we solve 648 benchmarks more than ApproMC2, the state of the art approximate model counter and for all the formulas where both ApproMC2 and ApproxMC3 did not timeout and took more than 1 seconds, the mean speedup is 284.40 -- more than two orders of magnitude.
2
On testing of Uniform Samplers
Sourav Chakraborty and Kuldeep S. Meel
Proceedings of AAAI Conference on Artificial Intelligence (AAAI), 2019.
Recent years have seen an unprecedented adoption of artificial intelligence in wide variety of applications ranging from medical diagnosis, automobile, security to aircraft collision avoidance. Probabilistic reasoning is a key component of such modern artificial intelligence systems. Sampling techniques form the core of the state of the art probabilistic reasoning systems. In contrast to testing for deterministic programs, where one trace is sufficient to prove the existence of a bug; such is not the case for samplers as one sample is typically not sufficient to prove non-conformity of the sampler to the desired distribution. This makes one wonder: whether it is possible to design testing methodology to test whether a sampler under test generates samples close to a given distribution. The primary contribution of this paper is a positive answer to the above question: We design, to the best of our knowledge, the first algorithmic framework, Barbarik, to test whether the distribution generated by $\varepsilon-$close or $\eta-$far from the uniform distribution. In contrast to the sampling techniques that require an exponential or sub-exponential number of samples for sampler whose support can be represented by $n$ bits, Barbarik requires only $\mathcal{O}(1/(\eta-\varepsilon)^2)$ samples. We present a prototype implementation of Barbarik and use it to test three state of the art uniform samplers over the support defined by combinatorial constraints. Barbarik is able to provide a certificate of uniformity to one sampler and demonstrate non-uniformity for the other two samplers.
3
Not All FPRASs are Equal: Demystifying FPRASs for DNF-Counting
Kuldeep S. Meel, Aditya A. Shrotri, and Moshe Y. Vardi
Proceedings of International Conference on Constraint Programming (CP), 2018.
Invited to Constraints journal and Invited to IJCAI 2019 Sister Conference Best Paper Track
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 probabilistic databases. Owing to the intractability of the exact variant, efforts have focused on the design of approximate techniques for #DNF. Consequently, several Fully Polynomial Randomized Approximation Schemes (FPRASs) based on Monte Carlo techniques have been proposed. Recently, it was discovered that hashing-based techniques too lend themselves to FPRASs for #DNF. Despite significant improvements, the complexity of the hashing-based FPRAS is still worse than that of the best Monte Carlo FPRAS by polylog factors. Two questions were left unanswered in previous works: Can the complexity of the hashing-based techniques be improved? How do the various approaches stack up against each other empirically? In this paper, we first propose a new search procedure for the hashing-based FPRAS that removes the polylog factors from its time complexity. We then present the first empirical study of runtime behavior of different FPRASs for #DNF. The result of our study produces a nuanced picture. First of all, we observe that there is no single best algorithm that outperforms all others for all classes of formulas and input parameters. Second, we observe that the algorithm with the worst time complexity, solves the largest number of benchmarks.
4
Algorithmic Improvements in Approximate Counting for Probabilistic Inference: From Linear to Logarithmic SAT Calls
Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi
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 hashing-based approximate counting. State-of-the-art hashing-based 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 hashing-based 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 state-of-the-art techniques for approximate counting by 1-2 orders of magnitude in running time.
5
On Computing Minimal Independent Support and Its Applications to Sampling and Counting
Alexander Ivrii, Sharad Malik, Kuldeep S. Meel, and Moshe Y. Vardi
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 state-of-the-art constrained sampling and counting tools, while still retaining theoretical guarantees.

Full list of publications is available here

[top]

Service

[top]

News

All news…

Recent Profile: Kuldeep Meel: The New CS Professor
Old Profile: Kuldeep Meel: High-Risk, High-Reward Research

[top]

Recruitment

I am looking for highly motivated Ph.D. students and interns (with time commitment of at least 6 months) in our group.

  • If you are a student at NUS, feel free to drop by my office or schedule a meeting with me. (See my calendar).
  • Otherwise, please send me an email with your CV if you are interested. Make sure your subject contains the word "olleh" and you should include reviews of two of the papers published in the previous 3 years at AAAI/IJCAI/CP/SAT/CAV conferences. The reviews should be in the body of the email (and not as pdf). Furthermore, the body of your email should contain the phrase: "Here are two papers that I have reviewed". You should also provide reason for your choice of the papers. A strong background in statistics, algorithms/formal methods and prior experience in coding is crucial to make a significant contribution to our research.

[top]