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). Gaussian Elimination Meets Maximum Satisfiability. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR).

PDF Code Poster

(2021). Testing Probabilistic Circuits. In Advances in Neural Information Processing Systems (NeurIPS).

PDF

(2021). Engineering an Efficient PB-XOR Solver. In Proceedings of International Conference on Constraint Programming (CP).

PDF Code Dataset

(2021). Engineering an Efficient Boolean Functional Synthesis Engine. In Proceedings of International Conference On Computer Aided Design (ICCAD).

PDF Code Slides Video

(2021). Designing Samplers is Easy: The Boon of Testers. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD).

PDF Code Slides Video

News

Our paper on Testing of Probabilistic Cirucits is accepted to NeurIPS 2021.
Authors: Yash Pote and Kuldeep S. Meel
Our paper on Engineering an Efficient PB-XOR Solver is accepted to CP 2021.
Authors: Jiong Yang and Kuldeep S. Meel
Our paper Engineering an Efficient Boolean Functional Synthesis Engine has been accepted to ICCAD 2021.
The work addresses scalability barriers faced by the current state-of-the-art synthesis techniques. We propose four algorithmic improvements for a data-driven framework for functional synthesis.
Authors: Priyanka Golia, Friedrich Slivovsky, Subhajit Roy, Kuldeep S. Meel
Our paper Designing Samplers is Easy: The Boon of Testers has been accepted to FMCAD 2021.
Our Sampler not only passes the tests of Barbarik but also leads to significant performance improvements for real-world instances.
Authors: Priyanka Golia, Mate Soos, Sourav Chakraborty, Kuldeep S. Meel

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

Gunjan Kumar

Avatar

Lawqueen Kanesh

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