Meel Group

Department of Computer Science
University of Toronto

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

Meelgroup flipside

Interests

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

Research

Our primary research interest is in automated reasoning. The long term vision of our research program is to advance automated reasoning techniques to enable computing to deal with increasingly uncertain real-world environments. The core theme of our research program is the quest for scalability. Accordingly, our work straddles theory and practice, and draws upon ideas from randomized algorithms, statistical inference, formal methods, distribution testing, and software engineering.

Given the broad nature of the field of automated reasoning, our research group's work spans multiple traditional subfields of computer science, reflected by publication record as well as recognition in artificial intelligence (AAAI: 17×, IJCAI: 13×, NeurIPS: 6×), formal methods (CAV: 7×, CP: 8×, SAT: 6×, TACAS: 3×), design automation (ICCAD: 2×, DATE: 2×, DAC: 1×), and logic/databases (PODS: 4×, ICALP: 1×, LPAR: 4×, LICS: 2×). In short, a research group that is not bound by (traditional) borders.

Publications

Quickly discover relevant content by filtering publications.
Yacine Izza, Kuldeep S. Meel, and Joao Marques-Silva (2024). Locally-Minimal Probabilistic Explanations. In Proceedings of ECAI - European Conference on Artificial Intelligence.

PDF

Kuldeep S. Meel, Supratik Chakraborty, and S. Akshay (2024). Auditable Algorithms for Approximate Model Counting. In Proceedings of the AAAI Conference on Artificial Intelligenc (AAAI).

PDF

Suwei Yang, and Kuldeep S. Meel (2024). Engineering an Exact Pseudo-Boolean Model Counter. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).

PDF

Mohimenul Kabir,, Supratik Chakraborty,, and Kuldeep S. Meel (2024). Exact ASP Counting with Compact Encodings. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).

PDF

Rishiraj Bhattacharya, Sourav Chakraborty, Yash Pote, Uddalok Sarkar, and Sayantan Sen (2024). Testing Self-Reducible Samplers. In Proceedings of the AAAI Conference on Artificial Intelligenc (AAAI).

PDF

See all publications

Blog Posts

CrystalBall: SAT solving, Data Gathering, and Machine Learning
Knowledge Compilation meets Uniform Sampling
WAPS: Weighted and Projected Sampling
GANAK: A Scalable Probabilistic Exact Model Counter
Bosphorus: An ANF and CNF simplifier and converter
See all posts

News

Our work on lower bounding minimal model count has been accepted to ICLP 2024.
We present two techniques for lower bounding the number of minimal models of a propositional formula. The work has been selected for TPLP journal
Authors: Mohimenul Kabir and Kuldeep S. Meel
Sep 5, 2024 12:00 AM
Our work on Quantum Circuit Mapping Based on Incremental and Parallel SAT Solving has been accepted to SAT 2024.
We introduce a novel circuit mapping method by combining incremental and parallel solving for Boolean Satisfiability (SAT). We present an innovative SAT encoding for circuit mapping problems, which significantly improves solver-based mapping methods and provides a smooth trade-off between compilation quality and compilation time.
Authors: Jiong Yang, Yaroslav A. Kharkov, Yunong Shi, Marijn Heule, and Bruno Dutertre
May 23, 2024 12:00 AM
Our work on Formally Certified Approximate Model Counting has been accepted to CAV 2024.
We present the first certification framework for approximate model counting with formally verified guarantees on the quality of its output approximation. Our approach combines: (i) a static, once-off, formal proof of the algorithm's PAC guarantee in the Isabelle/HOL proof assistant; and (ii) dynamic, per-run, verification of ApproxMC's calls to an external CNF-XOR solver using proof certificates.
Authors: Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen, and Kuldeep S. Meel
Mar 26, 2024 12:00 AM
Five Papers accepted to AAAI 2024.
1. The first paper is Auditable Algorithms for Approximate Model Counting
    Authors: S. Akshay, Supratik Chakraborty and Kuldeep S. Meel
2. The second paper is An Approximate Skolem Function Counter
    Authors: Arijit Shaw, Brendan Juba and Kuldeep S. Meel
3. The third paper is Exact ASP Counting with Compact Encodings
    Authors: Mohimenul Kabir, Supratik Chakraborty and Kuldeep S. Meel
4. The fourth paper is Testing Self-Reducible Samplers
    Authors: Rishiraj Bhattacharyya, Sourav Chakraborty, Yash Pote, Uddalok Sarkar and Sayantan Sen
5. The fifth paper is Engineering an Exact Pseudo-Boolean Model Counter
    Authors: Suwei Yang and Kuldeep S. Meel
Dec 14, 2023 12:00 AM
See all news

Software


Name Input Type Project Webpage Note
Arjun CNF Preprocessor Source Minimal independent set calculator and CNF minimizer
ApproxMC CNF Approximate Counter Source Supports projected model counting
ExactMC CNF Exact Counter Source Supports weighted model counting
GANAK CNF Exact Counter Source Supports projected model counting
PBCount Pseudo-Boolean Formula Exact Counter Source Supports weighted model counting
ApproxMC-PB Pseudo-Boolean Formula Approximate Counter Source Supports projected model counting
sharpASP Answer set program Exact Counter Source Exact count of the number of answer sets
ApproxASP Answer set program Approximate counter Source approximately counts the number of answer sets
pepin DNF Approximate Counter Source Supports weighted model counting
Crane First Order Formula Exact Counter Source Supports weighted model counting
CSB SMT (bit vector) Approximate Counter and Sampler Source Approximate counting, almost uniform and uniform-like smapling
SkolemFC QBF Approximate Counter Source Counts number of Skolem functions
AMUSIC CNF Approximate MUS Counter Source Counts minimal unsatisfiable subsets of CNF
Weighted-to-unweighted Weighted CNF Utility Source Converts weighted CNF to unweighted CNF
UniGen CNF Almost Uniform sampler Source Supports Projected Sampling
CMSGen CNF Uniform-like sampler Source Supports Projected Sampling
WAPS CNF Exact Uniform sampler Source Supports weighted and Projected Sampling
INC CNF Incremental uniform sampler Source Supports weighted Sampling
Manthan QBF Skolem Function Synthesizer Source Synthesize Skolem function given a specification
Barbarik CNF Sampler Sampler Tester Source Supports weighted sampler testing
Teq NNF Probabilistic Circuit Closeness Tester Source Tests whether two Probabilistic Circuits (in NNF) are close
Cubeprobe CNF Sampler Sampler Tester Source Self reducible sampler tester

Meet the Team

Faculty

Avatar

Kuldeep S. Meel

Postdoctoral Researchers

Avatar

Paulius Dilkas

PhD Students

Avatar

Arijit Shaw

Avatar

Suwei Yang

Avatar

Uddalok Sarkar

Avatar

Yash Pote

Avatar

Jiong Yang

Avatar

Jack Sun

Avatar

Mohimenul Kabir

Avatar

Yifan Ruan

Research Interns

Avatar

Ashwin Karthikeyan

Alumni - Postdoc graduates

Avatar

Yacine Izza

Avatar

Gunjan Kumar

Avatar

Tim van Bremen

Avatar

Anna Latour

Avatar

Yong Lai

Avatar

Jaroslav Bendík

Avatar

Lawqueen Kanesh

Avatar

Vignesh Sivaraman

Alumni - PhD graduates

Avatar

Priyanka Golia

Avatar

Bishwamittra Ghosh

Avatar

Teodora Baluta

Alumni - Research Interns

Avatar

Durgesh Agrawal

Avatar

Bhavishya

Avatar

Aaryan Gupta

Avatar

Alexandru Dinu

Avatar

Ananth Krishna Kidambi

Avatar

Biswadeep

Avatar

Guramrit Singh

Avatar

Mihir J Vahanwala

Avatar

Souptik Halder

Avatar

Zhanzhong Pang

Alumni - Masters Graduates

Avatar

Rémi Delannoy

Avatar

Shubham Sharma

Avatar

Rahul Gupta

Avatar

Alexis de Colnet

Past Visitors

2023

Dror Fried

Open University of Israel

Friedrich Slivovsky

TU Wien

S Akshay

IIT Bombay

2019

Sourav Chakraborty

CMI

Jan Elferrs

KTH

Pavan Aduri

Iowa State

Roland Jie-Hong

National Taiwan University

Stephan Gocht

KTH

2018

Sourav Chakraborty

CMI

Aditya Shrotri

Rice

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 the University of Toronto, 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. Interested candidates should email meel+postdoc@cs.toronto.edu with a PDF of CV, which must contain information of at least two references. Furthermore, a short write up indicating your interest in a particular theme is required. The initial term of appointment will be one year extensible for another year, upon review of satisfactory performance. The selected candidates will be offered competitive salaries and benefits including generous travel funding to top-tier conferences.
  • Internship (>=6 months): We strongly prefer candidates who want to use their internship as a way to apply for PhD programs (at UofT or elsewhere; of course, if you are good, we would like you to remain at UofT). Email meel+interns@cs.toronto.edu 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 the Department of Computer Science at UofT are handled via a central admission procedure.

    • UofT and Toronto

    UofT is a world-class university that provides an outstanding and supportive research environment. Its Department of Computer Science is highly ranked (within the top 15) among the computer science departments in the world. Toronto is a vibrant, well-connected city and a research hub in North America.

    Contact