Variational Satisfiability Solving: Efficiently Solving Lots of Related SAT Problems - Summary

Vorschaubild nicht verfügbar
Volltext URI
Text/Conference Paper
ISSN der Zeitschrift
Software Engineering 2023
Wissenschaftliches Hauptprogramm
Gesellschaft für Informatik e.V.
We report about recent research on satisfiability solving for variational domains, originally published in 2022 in the Empirical Software Engineering Journal (EMSE) within the special issue on configurable systems[ Yo22]. Incremental SAT solving is an extension of classic SAT solving that enables solving a set of related SAT problems by identifying and exploiting shared terms. However, using incremental solvers effectively is hard since performance is sensitive to the input order of subterms and results must be tracked manually. This paper translates the ordering problem to an encoding problem and automates the use of incremental solving. We introduce variational SAT solving, which differs from incremental solving by accepting all related problems as a single variational input and returning all results as a single variational output. Variational SAT solving automates the interaction with the incremental solver and enables a method to automatically optimize sharing in the input. We formalize a variational SAT algorithm, construct a prototype variational solver, and perform an empirical analysis on two real-world datasets that applied incremental solvers to software evolution scenarios. We show that the prototype solver scales better for these problems than four off-the-shelf incremental solvers while also automatically tracking individual results.
Young, Jeffrey M.; Bittner, Paul Maximilian; Walkingshaw, Eric; Thüm, Thomas (2023): Variational Satisfiability Solving: Efficiently Solving Lots of Related SAT Problems - Summary. Software Engineering 2023. Bonn: Gesellschaft für Informatik e.V.. PISSN: 1617-5468. ISBN: 978-3-88579-726-5. pp. 129-130. Wissenschaftliches Hauptprogramm. Paderborn. 20.–24. Februar 2023