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.
(2025). Towards Practical First-Order Model Counting. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT).

PDF

(2024). Locally-Minimal Probabilistic Explanations. In Proceedings of ECAI - European Conference on Artificial Intelligence.

PDF

(2024). An Approximate Skolem Function Counter. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).

PDF

(2024). Auditable Algorithms for Approximate Model Counting. In Proceedings of the AAAI Conference on Artificial Intelligenc (AAAI).

PDF

(2024). Engineering an Exact Pseudo-Boolean Model Counter. In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).

PDF

News

Our work Towards Practical First-Order Model Counting has been accepted to SAT 2025.
We extend the first-order model counting algorithm Crane with the ability to find the base cases of recursive functions and compile (recursive) function definitions into C++ programs.
Authors: Ananth K. Kidambi, Guramrit Singh, Paulius Dilkas, and Kuldeep S. Meel
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
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
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

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

Postdoctoral Researchers

PhD Students

Research Interns

Alumni - Postdoc graduates

Avatar

Yong Lai

Avatar

Lawqueen Kanesh

Alumni - PhD graduates

Alumni - Research Interns

Avatar

Ananth Krishna Kidambi

Avatar

Guramrit Singh

Avatar

Biswadeep

Alumni - Masters Graduates

Avatar

Rémi Delannoy

Avatar

Alexis de Colnet

Past Visitors

2023

Dror Fried

Open University of Israel

S Akshay

IIT Bombay

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 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