DROPS

Document

Automated Synthesis: Functional, Reactive and Beyond (Dagstuhl Seminar 24171)

Authors: S. Akshay, Bernd Finkbeiner, Kuldeep S. Meel, Ruzica Piskac, and Arijit Shaw

Published in: Dagstuhl Reports, Volume 14, Issue 4 (2024)

Abstract

This report summarizes the program of Dagstuhl Seminar 24171 on "Automated Synthesis: Functional, Reactive and Beyond". The seminar brought together researchers working on different aspects of functional synthesis and investigated its relationship with reactive synthesis. Through multiple expository tutorials, diverse technical talks, and multiple open discussion sessions, the seminar crystallized the current challenges for theory and tools in this area and opened fresh directions towards new applications.

Cite as

S. Akshay, Bernd Finkbeiner, Kuldeep S. Meel, Ruzica Piskac, and Arijit Shaw. Automated Synthesis: Functional, Reactive and Beyond (Dagstuhl Seminar 24171). In Dagstuhl Reports, Volume 14, Issue 4, pp. 85-107, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{akshay_et_al:DagRep.14.4.85,
  author =	{Akshay, S. and Finkbeiner, Bernd and Meel, Kuldeep S. and Piskac, Ruzica and Shaw, Arijit},
  title =	{{Automated Synthesis: Functional, Reactive and Beyond (Dagstuhl Seminar 24171)}},
  pages =	{85--107},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{14},
  number =	{4},
  editor =	{Akshay, S. and Finkbeiner, Bernd and Meel, Kuldeep S. and Piskac, Ruzica and Shaw, Arijit},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.14.4.85},
  URN =		{urn:nbn:de:0030-drops-213515},
  doi =		{10.4230/DagRep.14.4.85},
  annote =	{Keywords: automated synthesis, boolean functions, knowledge representations, reactive synthesis, SAT/SMT solvers}
}

Document

DOI: 10.4230/LIPIcs.SAT.2023.28

Explaining SAT Solving Using Causal Reasoning

Authors: Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)

Abstract

The past three decades have witnessed notable success in designing efficient SAT solvers, with modern solvers capable of solving industrial benchmarks containing millions of variables in just a few seconds. The success of modern SAT solvers owes to the widely-used CDCL algorithm, which lacks comprehensive theoretical investigation. Furthermore, it has been observed that CDCL solvers still struggle to deal with specific classes of benchmarks comprising only hundreds of variables, which contrasts with their widespread use in real-world applications. Consequently, there is an urgent need to uncover the inner workings of these seemingly weak yet powerful black boxes. In this paper, we present a first step towards this goal by introducing an approach called {CausalSAT}, which employs causal reasoning to gain insights into the functioning of modern SAT solvers. {CausalSAT} initially generates observational data from the execution of SAT solvers and learns a structured graph representing the causal relationships between the components of a SAT solver. Subsequently, given a query such as whether a clause with low literals blocks distance (LBD) has a higher clause utility, {CausalSAT} calculates the causal effect of LBD on clause utility and provides an answer to the question. We use {CausalSAT} to quantitatively verify hypotheses previously regarded as "rules of thumb" or empirical findings, such as the query above or the notion that clauses with high LBD experience a rapid drop in utility over time. Moreover, {CausalSAT} can address previously unexplored questions, like which branching heuristic leads to greater clause utility in order to study the relationship between branching and clause management. Experimental evaluations using practical benchmarks demonstrate that {CausalSAT} effectively fits the data, verifies four "rules of thumb", and provides answers to three questions closely related to implementing modern solvers.

Cite as

Jiong Yang, Arijit Shaw, Teodora Baluta, Mate Soos, and Kuldeep S. Meel. Explaining SAT Solving Using Causal Reasoning. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.SAT.2023.28,
  author =	{Yang, Jiong and Shaw, Arijit and Baluta, Teodora and Soos, Mate and Meel, Kuldeep S.},
  title =	{{Explaining SAT Solving Using Causal Reasoning}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.28},
  URN =		{urn:nbn:de:0030-drops-184909},
  doi =		{10.4230/LIPIcs.SAT.2023.28},
  annote =	{Keywords: Satisfiability, Causality, SAT solver, Clause management}
}

Search Results

Documents authored by Shaw, Arijit

Automated Synthesis: Functional, Reactive and Beyond (Dagstuhl Seminar 24171)

Abstract

Cite as

Explaining SAT Solving Using Causal Reasoning

Abstract

Cite as

Thanks for your feedback!

Could not send message