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


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


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.


Quickly discover relevant content by filtering publications.
(2023). Functional Synthesis via Formal Methods and Machine Learning. PhD Thesis, National University of Singapore and Indian Institute of Technology Kanpur.


(2023). A Fast and Accurate ASP Counting Based Network Reliability Estimator. In Proceedings of International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR).


(2023). Approximate Model Counting: Is SAT Oracle More Powerful than NP Oracle?. In Proceedings of International Colloquium on Automata, Languages and Programming (ICALP).


(2023). Support Size Estimation: The Power of Conditioning. In International Symposium on Mathematical Foundations of Computer Science (MFCS).



We have presented a tutorial on auditing bias in machine learning in IJCAI 2023. Presenters: Bishwamittra Ghosh and Debabrota Basu.
In this tutorial, we address three questions on bias in machine learning: (i) Choosing a compatible fairness metric based on application context, (ii) Formally quantifying fairness with respect to the compatible metric, and (iii) Explaining the sources of unfairness corresponding to the metric.
We will present our paper Solving the Identifying Code Set Problem with Grouped Independent Support this month at IJCAI 2023.
We show how reducing an NP-hard problem to a problem in the second order of the polynomial hierarchy helps us to exponentially decrease the encoding size. By leveraging modern solvers that solve problems beyond NP, we can solve much larger problem instances than the former state of the art.
If you are attending IJCAI in Macau, please come to our talk on Wednesday 23rd August, at 11:45am in the CSO: Constraint Programming session, or join us for the poster session afterwards, from 5pm until 6:30pm. You can also check out our preprint or watch this short video, which summarises our contribution.
Authors: Anna L.D. Latour, Arunabha Sen, Kuldeep S. Meel
Our work on Rounding Meets Approximate Model Counting has been accepted to CAV 2023 and received Distinguished Paper Award.
We round the approximate count of ApproxMC, which allows us to achieve 4$\times$ speedup over the state of the art.
Authors: Jiong Yang and Kuldeep S. Meel
Our paper Synthesising Recursive Functions for First-Order Model Counting: Challenges, Progress, and Conjectures has been accepted to KR 2023.
We extend the first-order model counting algorithm ForcLift with new compilation rules, enabling it to discover recursive solutions to previously-unsolved instances.
Authors: Paulius Dilkas, Vaishak Belle



A weighted model counter for first-order logic


Manthan: A Data-Driven Approach for Boolean Function Synthesis


NPAQ: Neural Property Approximate Quantifier


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


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


GANAK: A Scalable Probabilistic Exact Model Counter


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


On Testing of Uniform Samplers


WAPS: Weighted and Projected Sampling


An ANF and CNF simplifier and converter.


Knowledge Compilation meets Uniform Sampling


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


An approximate model counter for Bitvector theory.


A hashing-based approximate sampler for weighted CNF formulas.


A weighted model counter over Boolean domains.


Phase Transition Behavior of Cardinality and XOR Constraints

Meet the Team


Postdoctoral Researchers

PhD Students

Research Interns



Yong Lai


Rémi Delannoy


Alexis de Colnet

Ananth Krishna Kidambi



Guramrit Singh


Lawqueen Kanesh

Past Visitors


Dror Fried

Open University of Israel

S Akshay

IIT Bombay


Pavan Aduri

Iowa State

Roland Jie-Hong

National Taiwan University


Vijay Ganesh



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