Meel Group

Computer Science Department
School of Computing
National University of Singapore

Welcome to the Meel Group’s web page. We are situated at National University of Singapore.

Meelgroup flipside

Interests

  • Artificial Intelligence
  • Constrained Sampling and Counting
  • Knowledge Representation and Reasoning
  • Formal Methods
  • Interpretable Models

Research

Overview

Enabling Beyond NP Revolution

Our research program’s long-term vision is to advance automated reasoning techniques to enable computing to deal with increasingly uncertain real-world environments. From the core technical perspective, our research program is motivated by the unprecedented advances in the combinatorial solving techniques over the past three decades, often called as NP revolution, owing to the focus on the fundamental problem in Nondeterministic Polynomial (NP) time complexity: satisfiability (SAT). The NP revolution offers us the opportunity to develop scalable techniques for problems that lie Beyond NP. In particular, we focus on four fundamental problems that lie beyond NP: constrained counting, constrained sampling, functional synthesis, and maximum satisfiability. Our research program is focused on enabling Beyond NP Revolution via making progress on the following critical enabling ingredients:

Theme 1: Beyond Worst-Case Algorithmic Design

While theoreticians have studied the aforementioned problems for over thirty years, such studies employed the narrow lens of SAT oracles, which did not broadly allow a more nuanced characterization of the SAT queries’ complexity. In contrast, we focus on designing algorithms with SAT queries that can be efficiently solved by the underlying SAT solvers. In the context of approximate counting, we have developed a hashing-based framework, ApproxMC, that relies on sparse XORs to circumvent the practical hardness of queries based on dense XORs [MSV19a, MSV19b, ABM20, MA20, BM20]. The LICS20 paper [MA20](co-authored with S. Akshay) resolved the longstanding open problem of designing a sparse XOR-based algorithmic framework that can achieve runtime improvement without losing theoretical guarantees. As a high degree of symmetry in the underlying constraints amplifies the practical hardness, we rely on domainlevel symmetry breaking for performance improvement [WUA+20]. In the context of sampling, our framework, Waps, employs the progress in knowledge compilation to achieve scalability without losing theoretical guarantees [SGRM18, GSRM19]. In follow-up work, we improved the underlying algorithmic framework for knowledge compilation via probabilistic caching enabled via universal hashing [SRSM19]. Building on the success of constrained sampling and machine learning techniques, we proposed a novel algorithmic framework, called Manthan, for functional synthesis that achieved significant breakthrough in the number of instances solved [GRM20a].

Theme 2: Applications

A key ingredient in the NP revolution was focus on the instances arising from the real-world, allowing the design of techniques tuned to practical instances. In a similar vein, we focus on discovering new applications for the aforementioned problems and the design of efficient modeling schemes. In an interdisciplinary collaboration, we reduced the problem of reliability of power transmission grids to constrained counting [PDOMV19]. Furthermore, we reduce the quantitative verification of neural networks [NSM+19, BSS+19], and quantification of information flow [BEH+18] to constrained counting. Building on our algorithmic progress in constrained sampling, we design efficient technique for higher t-wise coverage in the context of highly configurable software systems [BLM20]. In regards to maximum satisfiability, we showed that the problem of decoding in group testing reduces to maximum satisfiability [CGSM20]. In another line of work, we design efficient provable techniques for learning interpretable classifiers via reduction to MaxSAT [MM18, GM19, GMM20].

Theme 3: Query-Driven Design of Solvers

SAT solvers’ usage inside broader algorithmic frameworks gives rise to the rich structure of the SAT queries. We have taken a twofold approach: On one hand, our recent work on uncovering the structure of solution spaces through the lens of phase transition behavior [PJM19, GRM20b]. As a next step, we focus on engineering the underlying architecture of the SAT solvers. Given the crucial importance of CNF-XOR solving for counting and sampling, we have proposed a novel architecture, BIRD, relying on the tight integration of CDCL and Gauss-Jordan Elimination to achieve significant improvements for CNF-XOR solving [SM19, SGM20]. Motivated by applications in cryptography and collaboration with the Defense Service Organization (DSO), we developed a new architecture, Bosphorus, for CNF-ANF formulas [CSCM19], and further improved performance with phase saving [SM20]. Our most ambitious project, CrystalBall [SKM19], focuses on the data-driven synthesis of SAT Solvers by combining the advances in proof systems with supervised learning.

Theme 4: Testing Framework

Similar to the pivotal role played by testing frameworks in the NP revolution, the realization of the Beyond NP revolution would need scalable testing and verification methodologies. As a first step, we have focused on testing of constrained samplers. In contrast to conventional programs, one trace/sample is typically inadequate to prove the non-conformity of the underlying samplers. We are developing an algorithmic framework, Barbarik, that sits at the intersection of property testing and symbolic reasoning [CM19]. Barbarik [CM19, MPC20] can handle product distributions and is the first tester to require a constant number of samples, in contrast to prior work requiring exponentially many samples.

Open-Source Tools

Our research has led to the release of 10 actively maintained open source tools. Our SAT solver entry won 3rd place in the Main Track of the highly prestigious and competitive SAT competition 2020 (the first instance of a top-3 finish by an entry from Singapore) while our model counting entry won 1st place in two of three tracks.

Publications

Quickly discover relevant content by filtering publications.
(2021). Program Synthesis as Dependency Quantified Formula Modulo Theory. In Proceedings International Joint Conference on Artificial Intelligence (IJCAI).

PDF Code

(2021). Scalable Quantitative Verification For Deep Neural Networks. In IEEE/ACM 43rd International Conference on Software Engineering (ICSE).

PDF Code Slides

(2021). The Power of Literal Equivalence in Model Counting. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).

PDF

(2021). Counting Maximal Satisfiable Subsets. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).

PDF

(2021). Justicia A Stochastic SAT Approach to Formally Verify Fairness. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).

PDF

News

Our paper on Program Synthesis as Dependency Quantified Formula Modulo Theory has been accepted to IJCAI 2021.
We show that theory-constrained synthesis can be reduced DQF(T), i.e., to the problem of finding a witness of a dependency quantified formula modulo theory.
Authors: Priyanka Golia, Subhajit Roy, Kuldeep S. Meel
Our paper on scalable quantitative verification for deep neural networks has been accepted to ICSE 2021.
We give a sampling-based approach for quantifying properties for deep neural networks and an attack-agnostic metric called adversarial hardness to capture a model's robustness.
Authors: Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel and Prateek Saxena
We will be presenting three papers at NeurIPS-20.
1. The first paper focuses on efficient distance approximation in high dimension distributions. We propose an amazingly simple method that can compute L1 distance with rigorous guarantees. Come Poster Session 5 on Thursday.
    Joint work with A. Bhattacharya, S. Gayen, and N.V. Vinodchandran
2. The second paper provides the first scalable method to test samplers in practice. Barbarik can now test samplers that sample from log-linear models. If you propose a sampling technique but can't prove its correctness, you can now use Barbarik to check its quality. Just the way we use testing for our software. (Poster)
    Joint work with S. Chakraborty and Y. Pote
3. The third paper seeks to tame discrete integration with the boon of dimensionality (Yes, the boon not the curse). We extended our IJCAI-15's work of weighted to unweighted counting (thereby increasing the dimensionality) to handle rational weights. (Poster)
    Joint work with J.M. Dudek and D. Fried
All the five papers from our group were accepted to AAAI 2021.
1. Justicia: A Stochastic SAT Approach to Formally Verify Fairness
    Authors: Bishwamittra Ghosh, Debabrota Basu, and Kuldeep S Meel
2. Predicting Forest Fire Using Remote Sensing Data And Machine Learning
    Authors: Suwei Yang, Massimo Lupascu, and Kuldeep S Meel
3. Symmetric Component Caching for Model Counting on Structured Instances
    Authors: Timothy van Bremen, Vincent Derkinderen, Shubham Sharma, Subhajit Roy, and Kuldeep S Meel
4. Counting Maximal Satisfiable Subsets
    Authors: Jaroslav Bendik and Kuldeep S. Meel
5. The Power of Literal Equivalence in Model Counting
    Authors: Yong Lai, Kuldeep S Meel, and Roland Yap

Software


Manthan

Manthan: A Data-Driven Approach for Boolean Function Synthesis

NPAQ

NPAQ: Neural Property Approximate Quantifier

ApproxMC

A hashing-based algorithm for discrete integration over finite domains.

CrystalBall

A framework to provide white-box access to the execution of SAT solver.

GANAK

GANAK: A Scalable Probabilistic Exact Model Counter

UniGen

An algorithm to generate uniform samples subject to given set of constraints.

Barbarik

On Testing of Uniform Samplers

WAPS

WAPS: Weighted and Projected Sampling

Bosphorus

An ANF and CNF simplifier and converter.

KUS

Knowledge Compilation meets Uniform Sampling

MIS

An algorithm to compute minimal independent support for a given CNF formula.

SMTApproxMC

An approximate model counter for Bitvector theory.

WeightGen

A hashing-based approximate sampler for weighted CNF formulas.

WeightMC

A weighted model counter over Boolean domains.

1-CARD-XOR

Phase Transition Behavior of Cardinality and XOR Constraints

Meet the Team

Faculty

Postdoctoral Researchers

Avatar

Jaroslav Bendík

Avatar

Lawqueen Kanesh

Avatar

Vignesh Sivaraman

PhD Students

Avatar

Mohimenul Kabir

Research Interns

Avatar

Biswadeep

Alumni

Avatar

Yong Lai

Avatar

Alexis de Colnet

Avatar

Rémi Delannoy

Past Visitors

2019

Pavan Aduri

Iowa State

Roland Jie-Hong

National Taiwan University

2018

Vijay Ganesh

Waterloo

Openings

We are always looking for highly motivated Ph.D. students, research assistants and summer internship for exceptional undergraduate interns in our group. We work at the intersection of algorithmic design and systems; therefore, an ideal candidate should have deeper expertise in one area and willingness to learn the other. A strong background in statistics, algorithms/formal methods and prior experience in coding is crucial to make a significant contribution to our research.

Application Procedure:

  • If you are a student at NUS, feel free to drop by Kuldeep's office or schedule a meeting with him. (See his calendar).
  • Post-doc position: We have multiple post-doc positions available. Read advertisement for more details about the positions and application procedure.
  • Internship (>=6 months): We strongly prefer candidates who want to use their internship as a way to apply for PhD programs (@NUS or elsewhere; of course, if you are good, we would like you to remain at NUS). Email meel+interns@comp.nus.edu.sg with a PDF of your CV. 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.
  • Short term internship (=3 months): We may offer short term internship to exceptional undergraduates. Same process as above.
  • PhD positions: Admissions to School of Computing@NUS are handled via a central admission procedure: You can either apply via Department of Computer Science or the Institute of Data Science.
  • NUS and Singapore

    NUS is a world-class university that provides an outstanding and supportive research environment. Its School of Computing is highly ranked (within the top 15) among the computer science departments in the world. Singapore is a vibrant, well-connected city with low taxes and research hub in Asia.

    Contact