News

2024

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

2023

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
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.
Aug 19, 2023 12:00 AM
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
Aug 3, 2023 12:00 PM Macau
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
Jul 19, 2023 1:15 PM
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
Jun 9, 2023 12:00 PM
Our paper on explaining the sources of bias in machine learning via influence functions has been accepted in FAccT 2023. Authors: Bishwamittra Ghosh, Debabrota Basu and Kuldeep S. Meel.
We combine explainability with fairness in machine learning, where we compute the influence of individual features and the intersectional effect of multiple features on the resulting bias of a classifier on a dataset. This allows us to have a higher granular depiction of sources of bias than earlier methods.
Apr 8, 2023 12:00 AM
Our paper Generating Random Instances of Weighted Model Counting: An Empirical Analysis with Varying Primal Treewidth has been accepted to CPAIOR 2023.
We introduce a random model and use it to discover some critical differences among weighted model counting algorithms.
Authors: Paulius Dilkas
Feb 25, 2023 12:00 PM

2022

Our paper on Synthesis with Explicit Dependencies has been accepted to DATE 2023. Moreover, it has also received the best paper award nomination.
We present an approach that combines advances in machine learning with automated reasoning for efficiently synthesizing functions with explicit dependencies.
Authors: Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel
Nov 16, 2022 2:15 PM
Our paper On Scalable Testing of Samplers is accepted to NeurIPS 2022.
Authors: Yash Pote and Kuldeep S. Meel
Nov 6, 2022 12:00 AM
Our work on Projected Model Counting: Beyond Independent Support has been accepted to ATVA 2022.
We show that we can identify a set of variables, called upper bound support (UBS) , that is not necessarily a subset of sampling set, and yet counting models projected on UBS guarantees an upper bound of the projected model count.
Authors: Jiong Yang, Supratik Chakraborty, and Kuldeep S. Meel
Jul 4, 2022 1:15 PM
Our work on A Scalable Shannon Entropy Estimator is accepted to CAV-22.
We propose the first efficient algorithmic technique to estimate the Shannon entropy of a specification with PAC-style guarantees, i.e., the computed estimate is guaranteed to lie within a (1 ± ε)-factor of the ground truth with confidence at least 1−δ.
Authors: Priyanka Golia, Brendan Juba, Kuldeep S. Meel
May 9, 2022 1:15 PM
Our work On Quantitative Testing of Samplers has been accepted to CP-22.
We design a computational hardness-based tester, called ScalBarbarik that provides a qunatitative way to analysis the quality of a sampler.
Authors: Mate Soos, Priyanka Golia, Sourav Chakraborty, Kuldeep S. Meel
May 8, 2022 1:15 PM

2021

Our paper on “Efficient Learning of Interpretable Classification Rules” is accepted to JAIR journal.
Authors: Bishwamittra Ghosh, Dmitry Malioutov and Kuldeep S. Meel
Dec 21, 2021 12:00 AM
Our paper “A Scalable t-wise Coverage Estimator” is accepted to. ICSE 2022.
Authors: Eduard Baranov, Sourav Chakraborty, Axel Legay, Kuldeep S. Meel, and N.V. Vinodchandran
Dec 3, 2021 12:00 AM
Three Papers accepted to AAAI 2022.
1. The first paper is on Algorithmic Fairness Verification with Graphical Models.
    Authors: Bishwamittra Ghosh, Debabrota Basu and Kuldeep S. Meel
2. The second paper is ApproxASP - A Scalable Approximate Answer Set Counter.
    Authors: Mohimenul Kabir , Flavio Everardo, Ankit Shukla, Johannes K. Fichte, Markus Hecher and Kuldeep Meel
3. The third paper is on Constraint-Driven Explanations for Black Box ML Models.
    Authors: Aditya Shrotri, Nina Narodytska, Alexey Ignatiev, Joao Marques-Silva, Kuldeep S. Meel and Moshe Vardi
Dec 2, 2021 12:00 AM
Our paper on Testing of Probabilistic Cirucits is accepted to NeurIPS 2021.
Authors: Yash Pote and Kuldeep S. Meel
Nov 7, 2021 12:00 AM
Congratulations to Teodora Baluta for winning the Google PhD Fellowship.
Oct 30, 2021 2:15 PM
Our paper on Engineering an Efficient PB-XOR Solver is accepted to CP 2021.
Authors: Jiong Yang and Kuldeep S. Meel
Jul 28, 2021 12:00 AM
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
Jul 14, 2021 2:15 PM
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
Jul 9, 2021 2:15 PM
Our work on MaxSAT augmented with Gauss Jordan Elimination is accepted to KR2021.
Authors: Mate Soos and Kuldeep S. Meel
Jun 15, 2021 2:15 PM
Our work on GPU-based Parallel SAT solving is accepted to SAT 2021.
Authors: Nicolas Prevot, Mate Soos, and Kuldeep S. Meel
May 4, 2021 2:15 PM
Our paper on Program Synthesis as Dependency Quantified Formula Modulo Theory has been accepted to IJCAI 2021.
We show that theory-constrained synthesis can be reduced DQF(T), i.e., to the problem of finding a witness of a dependency quantified formula modulo theory.
Authors: Priyanka Golia, Subhajit Roy, Kuldeep S. Meel
Apr 30, 2021 2:15 PM
Our work on Counting Minimal Unsatisfiable Subsets is accepted to CAV 2021.
Authors: Jaroslav Bendik and Kuldeep S. Meel
Apr 21, 2021 2:15 PM
Kuldeep presented a talk on the rise of model counting at the Data and Knowledge Seminar at Oxford.
Apr 20, 2021 2:15 PM
Our paper Partition Function Estimation: A Quantitative Study has been accepted to IJCAI 2021 Survey Track.
This paper presents a survey of 17 partition function estimation techniques and a rigorous empirical study of their behavior across an extensive set of benchmarks.
Authors: Durgesh Agrawal, Yash Pote, and Kuldeep S. Meel
Apr 19, 2021 2:15 PM
Kuldeep gave a talk on Formal Methods+Machine Learning at CCI MHI Seminars at USC.
Apr 15, 2021 2:15 PM
Our work on computation of union of sets in streaming model is accepted to PODS-21.
Authors: Kuldeep S. Meel, N.V.Vinodchandran, and Sourav Chakraborty
Apr 2, 2021 2:15 PM
Kuldeep gave a talk on Formal Methods+Machine Learning at the PL Seminar at University of Wisconsin.
Mar 24, 2021 2:15 PM
Kuldeep gave a talk on Formal Methods+Machine Learning at Waterloo's ML+Logic Seminar.
Mar 15, 2021 2:15 PM
Our work on Linear Modular Arithmetic in CP is accepted to CPAIOR-21.
Authors: Gilles Pesant, Kuldeep S. Meel, and Mahshid Mohammadalitajrishi
Mar 13, 2021 2:15 PM
Kuldeep will present a talk on synthesis at the CITRIS People and Robotics seminar.
Mar 1, 2021 2:15 PM
Kuldeep will be giving an in-depth talk on the rise of approximate model counting at Simons Workshop on Beyond Satisfiability. Recorded video .
Feb 9, 2021 2:15 PM
Kuldeep will be giving an introductory talk on Approximate Counting and Sampling at Simons Bootcamp for Program on Satisfiability.
Feb 5, 2021 2:15 PM
Join, from the comfort of your home, our tutorial on Logic-Enabled Verification and Explanation of ML Models at IJCAI-21.
Jan 8, 2021 2:15 PM

2020

Our paper on scalable quantitative verification for deep neural networks has been accepted to ICSE 2021.
We give a sampling-based approach for quantifying properties for deep neural networks and an attack-agnostic metric called adversarial hardness to capture a model's robustness.
Authors: Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel and Prateek Saxena
Dec 17, 2020 2:15 PM
We will be presenting three papers at NeurIPS-20.
1. The first paper focuses on efficient distance approximation in high dimension distributions. We propose an amazingly simple method that can compute L1 distance with rigorous guarantees. Come Poster Session 5 on Thursday.
    Joint work with A. Bhattacharya, S. Gayen, and N.V. Vinodchandran
2. The second paper provides the first scalable method to test samplers in practice. Barbarik can now test samplers that sample from log-linear models. If you propose a sampling technique but can't prove its correctness, you can now use Barbarik to check its quality. Just the way we use testing for our software. (Poster)
    Joint work with S. Chakraborty and Y. Pote
3. The third paper seeks to tame discrete integration with the boon of dimensionality (Yes, the boon not the curse). We extended our IJCAI-15's work of weighted to unweighted counting (thereby increasing the dimensionality) to handle rational weights. (Poster)
    Joint work with J.M. Dudek and D. Fried
Dec 5, 2020 2:15 PM
All the five papers from our group were accepted to AAAI 2021.
1. Justicia: A Stochastic SAT Approach to Formally Verify Fairness
    Authors: Bishwamittra Ghosh, Debabrota Basu, and Kuldeep S Meel
2. Predicting Forest Fire Using Remote Sensing Data And Machine Learning
    Authors: Suwei Yang, Massimo Lupascu, and Kuldeep S Meel
3. Symmetric Component Caching for Model Counting on Structured Instances
    Authors: Timothy van Bremen, Vincent Derkinderen, Shubham Sharma, Subhajit Roy, and Kuldeep S Meel
4. Counting Maximal Satisfiable Subsets
    Authors: Jaroslav Bendik and Kuldeep S. Meel
5. The Power of Literal Equivalence in Model Counting
    Authors: Yong Lai, Kuldeep S Meel, and Roland Yap
Dec 2, 2020 12:00 AM
Three Papers accepted to NeurIPS 2020.
1. The first paper on On Testing of Samplers.
    Authors: Kuldeep S Meel, Yash Pralhad Pote and Sourav Chakraborty
2. The second paper on Taming Discrete Integration via the Boon of Dimensionality.
    Authors: Jeffrey M. Dudek, Dror Fried and Kuldeep S. Meel
3. The third paper on Efficient Distance Approximation for Structured High-Dimensional Distributions via Learning.
    Authors: Arnab Bhattacharyya, Sutanu Gayen, Kuldeep S. Meel and N. V. Vinodchandran
Sep 25, 2020 12:00 AM
Our Paper on Model Counting meets F0 Estimation (public version forthcoming!) is accepted to PODS 2021.
Authors: Arnab Bhattacharyya, Kuldeep Meel, A. Pavan and N.V. Vinodchandran
Sep 18, 2020 12:00 AM
We presented our work on Phase Transition Behaviour in Knowledge Compilation at CP 2020.
Sep 10, 2020 12:00 AM
We presented three papers at CAV 2020.
1. The first paper builds on our CNF-XOR solving paradigm (BIRD) and as a result, the new versions of ApproxMC and UniGen are faster than ever.
2. The second paper proposes the first algorithm for approximate MUS counting.
3. The third one proposes a data-driven approach for Boolean functional synthesis, which works at the intersection of constrained sampling, machine learning and automated reasoning.
Jul 22, 2020 12:00 AM
We have released the source code of Manthan.
Jul 13, 2020 12:00 AM
Our Paper on Phase Transition Behaviour in Knowledge Compilation is accepted to CP 2020.
Authors: Rahul Gupta, Subhajit Roy and Kuldeep S. Meel
Jul 8, 2020 12:00 AM
We have released ApproxMC 4.
Jul 7, 2020 12:00 AM
Two Papers accepted to SAT 2020.
1. The first paper shows that the currently known bounds for sparse hashing are too weak to be used for algorithms such as ApproxMC. Authors: Durgesh Agarwal, Bhavishya and Kuldeep S. Meel
2. The second paper proposes a new phase selection strategy for SAT solvers. Improving SAT solvers is just a very very hard job and we are excited about the improvements that our proposal brings to the world of SAT solving. Authors: Arijit Shaw and Kuldeep S. Meel
Apr 25, 2020 12:00 AM
Paper on Sparse Hashing for Approximate Model counting accepted to LICS 2020. Authors: S. Akshay and Kuldeep S. Meel
One of the reviews: “Rarely it is that there is a paper that proves a beautiful new theoretical result, explaining and simplifying previous work, and on top of that shows how it can be used to improve state-of-the-art practical algorithms. The paper “Sparse hashing for scalable approximate model counting: theory and practice” achieves exactly that.”
Apr 10, 2020 12:00 AM
Paper accepted to LPAR-23.
The paper formalizes Induction Models on N extending the classical work of Henkin. Authors: A Dileep, Kuldeep S. Meel and Ammar F. Sabili
Apr 8, 2020 12:00 AM
Three Papers accepted at Computer Aided Verification (CAV) 2020 conference.
1. The first paper proposes a new approach that combines sampling+machine learning+MaxSAT to achieve a significant progress in solving Boolean Functional Synthesis. Authors: Priyanka Golia, Subhajit Roy, and Kuldeep S. Meel
2. The second paper builds on our CNF-XOR solving paradigm (BIRD) and as a result, the new versions of ApproxMC and UniGen are faster than ever. Stay tuned for our releases. Authors: Mate Soos, Stephan Gocht, and Kuldeep S. Meel
3. The third paper proposes the first algorithm for approximate MUS counting. Authors: Jaroslav Bendik and Kuldeep S. Meel
Apr 6, 2020 12:00 AM
Sampling-based approach for quantittive quantitative verification of Deep Neural Nets.
We propose a new attack agnostic metric adversarial hardness to capture the model's robustness: https://arxiv.org/pdf/2002.06864.pdf Authors: Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel and Prateek Saxena.
Feb 18, 2020 12:00 AM
Alexey Ignatiev, Joao Marques-Silva, Kuldeep S. Meel and Nina Narodytska give a tutorial at the Tutorial Forum in AAAI'20: Rigorous Verification and Explanation of ML Models.
Feb 8, 2020 12:00 AM
Our paper on classification rules in relaxed logical form is accepted in ECAI-2020. Authors: Bishwamittra Ghosh, Dmitry Malioutov, and Kuldeep S. Meel
Jan 15, 2020 12:00 AM

2019

Our paper on Symmetry breaking and model counting is accepted to TACAS 2020. Authors: Wenxi Wang, Muhammad Usman, Alyas Almaawi, Kaiyuan Wang, Kuldeep S. Meel, and Sarfraz Khurshid
Dec 23, 2019 12:00 AM
Two of our group's papers are accepted to accepted as poster presentations with a spotlight talk at StarAI 2020 workshop in AAAI 2020: Our AIES-19 paper on incremental classification rule learning and our CCS-19 paper on quantiatative verification for binarized neural networks.
Dec 7, 2019 12:00 AM
Our paper on MaxSAT-based formulation for group testing is accepted in AAAI 2020. Authors: Lorenzo Ciampiconi, Bishwamittra Ghosh, Jonathan Scarlett and Kuldeep S. Meel
Sep 30, 2019 12:00 AM
Alexis will be presenting our work on unifying hashing-based approaches for discrete integration, and Bishwa will present on learning interpretable classifiers at CP2019.
Sep 30, 2019 12:00 AM
Our Paper on embedding symbolic knowledge into Neural Networks is accepted to NeurIPS 2019. Authors: Yaqi Xie, Ziwei Xu, Mohan S. Kankanhalli, Kuldeep S. Meel, Harold Soh
Sep 1, 2019 12:00 AM
We presented three papers at IJCAI-19. 1) The first paper explores the phase transition behavior of conjunction of cardinality and XOR constraints. 2) The second paper describes a radically new approach to exact counting wherein we compute estimates that are probabilistically exact! 3) The third one is our invited paper on #DNF.
Aug 13, 2019 12:00 AM
We have released the source code of GANAK.
Aug 12, 2019 12:00 AM
Our NPAQ framework focused on providing PAC guarantees for verification of Neural Networks is accepted to CCS-19 Quoting reviewer: “This work is pioneering a new technique to solve an incredibly challenging problem, and it shows that smaller problem can be solved. I can live with that, future work can improve computational efficiency.” Authors: Teodora Baluta, Shiqi Shen, Shweta Shinde, Kuldeep S. Meel, Prateek Saxena
Jul 30, 2019 12:00 AM
Our paper on interpretable rules expressed as relaxed-CNF is accepted at IJCAI workshop on XAI (Explainable Artificial Intelligence) and DSO (Data Science meets Optimization), 2019. Authors: Bishwamittra Ghosh, Dmitry Malioutov, Kuldeep S. Meel.
Jun 23, 2019 12:00 AM
Kuldeep recieved notification of the award of NRF Fellowship for AI for the project: Provably Verified and Explainable Probabilistic Reasoning.
May 15, 2019 12:00 AM
Two papers accepted to IJCAI. The first paper explores the phase transition behavior of conjunction of cardinality and XOR constraints. Authors: Yash Pote, Saurabh Joshi, Kuldeep Meel.
The second paper describes a radically new approach to exact counting wherein we compute estimates that are probabilistically exact! Authors: Shubham Sharma, Kuldeep Meel. Combined with our invited paper on #DNF, this makes 3 papers that we will be presenting at IJCAI.
May 9, 2019 12:00 AM
Two papers accepted to SAT 2019. The first paper introduces the first version of CrystalBall, a framework intended to allow gazing into the black box of SAT solving. Authors: Kuldeep, Mate Soos, Raghav Kulkarni.
The second paper discusses how model counting can be used to analyze explanations provided by tools such as ANCHOR. Authors: Kuldeep, Nina Narodytska, Aditya Shrotri, Alexey Ignatiev, and Joao Marques Silva.
Apr 22, 2019 12:00 AM
Kuldeep is appointed Visiting Assistant Professor in the Department of Computer Science and Engineering at IIT Bombay.
Feb 11, 2019 12:00 AM
Paper on network reliability is accepted to The 13th International Conference on Applications of Statistics and Probability in Civil Engineering Authors: Roger Paredes, Leonardo Duenas-Osorio, Kuldeep S. Meel, and Moshe Y. Vardi.
Feb 2, 2019 12:00 AM
Our paper on weighted and projected sampling is accepted at TACAS 2019. Authors: Shubham Sharma, Rahul Gupta, Subhajit Roy and Kuldeep S. Meel.
Jan 26, 2019 12:00 AM