Award-Winning Research Pushes Beyond Yes-or-No Answers in Automated Reasoning
Three researchers in the School of Computer Science were recently awarded for their research on a fundamental problem in automated reasoning.
Associate Professor Kuldeep Meel and Ph.D. students Arijit Shaw and Uddalok Sarkar won the Marco Cadoli Best Student Paper Award at the 22nd International Conference on Principles of Knowledge Representation and Reasoning (KR 2025) for their paper on volume computation of satisfiability modulo theory (SMT) formulas.
KR is one of the leading forums for research on the theory and practice of knowledge representation and reasoning.
The team's automated reasoning research aims to build algorithms that allow computers to perform logical reasoning. The output of these algorithms is traditionally binary: satisfiable or unsatisfiable. However, many modern applications demand more complicated answers than this.
Their winning paper, Efficient Volume Computation for SMT Formulas, addresses this issue through SMT formulas. The paper introduces an efficient algorithm that enables SMT solvers to compute volume, allowingthem to answer more complex queries. The new algorithm is faster and more scalable than existing methods for these volume problems.
“Arijit’s thesis focuses on this problem, so this award is a very nice culmination of the effort he has been building toward over the past four years.”
“What makes the result especially compelling is that it’s not only a strong empirical advance but also comes with theoretical guarantees, strengthening its contribution to quantitative automated reasoning,” said Meel, both students' advisor.
