Classified by Research TopicSorted by DateClassified by Publication Type

Counting, Sampling, and Synthesis: The Quest for Scalability

Counting, Sampling, and Synthesis: The Quest for Scalability.
Kuldeep S. Meel.
In Proceedings of International Joint Conference on Artificial Intelligence (IJCAI), July 2022.

Download

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

BibTeX

@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 Sun Apr 14, 2024 11:15:51