| CARVIEW |
Select Language
HTTP/2 200
server: GitHub.com
content-type: text/html; charset=utf-8
last-modified: Tue, 10 Jun 2025 18:49:23 GMT
access-control-allow-origin: *
strict-transport-security: max-age=31556952
etag: W/"68487e33-ff41"
expires: Tue, 30 Dec 2025 22:40:41 GMT
cache-control: max-age=600
content-encoding: gzip
x-proxy-cache: MISS
x-github-request-id: 7C38:1387E:A7501D:BC2C36:69545290
accept-ranges: bytes
age: 0
date: Tue, 30 Dec 2025 22:30:41 GMT
via: 1.1 varnish
x-served-by: cache-bom-vanm7210086-BOM
x-cache: MISS
x-cache-hits: 0
x-timer: S1767133841.911496,VS0,VE207
vary: Accept-Encoding
x-fastly-request-id: f1162dc12d6c4fcf7ca1dc781994a47ee5ca8759
content-length: 13257
MeelGroup
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.
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.
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.
Ananth Krishna Kidambi, Guramrit Singh, Paulius Dilkas, and Kuldeep S. Meel
(2025).
Towards Practical First-Order Model Counting.
In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing (SAT).
Yacine Izza, Kuldeep S. Meel, and Joao Marques-Silva
(2024).
Locally-Minimal Probabilistic Explanations.
In Proceedings of ECAI - European Conference on Artificial Intelligence.
Arijit Shaw, Brendan Juba, and Kuldeep S. Meel
(2024).
An Approximate Skolem Function Counter.
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).
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).
Suwei Yang, and Kuldeep S. Meel
(2024).
Engineering an Exact Pseudo-Boolean Model Counter.
In Proceedings of AAAI Conference on Artificial Intelligence (AAAI).
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
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
Jun 10, 2025 12:00 AM
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
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
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
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
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
Yong Lai
Lawqueen Kanesh
Alumni - PhD graduates
Alumni - Research Interns
Ananth Krishna Kidambi
Guramrit Singh
Biswadeep
Alumni - Masters Graduates
Rémi Delannoy
Alexis de Colnet
Past Visitors
2023
Dror Fried
Open University of Israel
Friedrich Slivovsky
TU Wien
S Akshay
IIT Bombay
2019
Jan Elferrs
KTH
Pavan Aduri
Iowa State
Roland Jie-Hong
National Taiwan University
Stephan Gocht
KTH
2018
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:
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
- meel@cs.toronto.edu
- 6 King's College Rd, Toronto, ON M5S 3G8
- 398B, D.L. Pratt Building
- Kuldeep Meel