• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Counting, Sampling, and Synthesis: The Quest for Scalability.
Kuldeep S. Meel.
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), July 2022.
The current generation of symbolic reasoning techniques excel at the qualitative tasks (i.e., when the answer is Yes or No); such techniques sufficed for traditional systems whose design sought to achieve deterministic behavior. In contrast, modern computing systems crucially rely on the statistical methods to account for the uncertainty in the environment, and to reason about behavior of these systems, there is need to look beyond qualitative symbolic reasoning techniques. We will discuss our work focused on the development of the next generation of automated reasoning techniques that can perform higher-order tasks such as quantitative measurement, sampling of representative behavior, and automated synthesis of systems. From a core technical perspective, our work builds on the SAT revolution, which refers to algorithmic advances in combinatorial solving techniques for the fundamental problem of satisfiability (SAT), i.e., whether it is possible to satisfy a given set of constraints. The SAT revolution offers the opportunity to develop scalable techniques for problems that lie beyond SAT from complexity perspective and, therefore, stand to benefit from the availability of powerful SAT engines. Our work seeks to enable a Beyond SAT revolution via design of scalable techniques for three fundamental problems that lie beyond SAT: constrained counting, constrained sampling, and automated synthesis.
@inproceedings{Meel22,
author={Meel, Kuldeep S.},
title={Counting, Sampling, and Synthesis: The Quest for Scalability},
bib2html_pubtype={Refereed Conference},
year={2022},
month=jul,
bib2html_rescat={Counting,Sampling,Synthesis},
booktitle=IJCAI,
bib2html_dl_pdf={../Papers/ijcai22.pdf},
abstract={
The current generation of symbolic reasoning techniques excel at the
qualitative tasks (i.e., when the answer is Yes or No); such techniques
sufficed for traditional systems whose design sought to achieve
deterministic behavior. In contrast, modern computing systems crucially rely
on the statistical methods to account for the uncertainty in the
environment, and to reason about behavior of these systems, there is need to
look beyond qualitative symbolic reasoning techniques. We will discuss our
work focused on the development of the next generation of automated
reasoning techniques that can perform higher-order tasks such as
quantitative measurement, sampling of representative behavior, and automated
synthesis of systems. From a core technical perspective, our work builds on
the SAT revolution, which refers to algorithmic advances in combinatorial
solving techniques for the fundamental problem of satisfiability (SAT),
i.e., whether it is possible to satisfy a given set of constraints. The SAT
revolution offers the opportunity to develop scalable techniques for
problems that lie beyond SAT from complexity perspective and, therefore,
stand to benefit from the availability of powerful SAT engines. Our work
seeks to enable a Beyond SAT revolution via design of scalable techniques
for three fundamental problems that lie beyond SAT: constrained counting,
constrained sampling, and automated synthesis.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Apr 30, 2026 09:22:03