Logo des Repositoriums
 

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

Kurzanzeige
dc.contributor.authorYoung, Jeffrey M.
dc.contributor.authorBittner, Paul Maximilian
dc.contributor.authorWalkingshaw, Eric
dc.contributor.authorThüm, Thomas
dc.contributor.editorEngels, Gregor
dc.contributor.editorHebig, Regina
dc.contributor.editorTichy, Matthias
dc.date.accessioned2023-01-18T13:38:53Z
dc.date.available2023-01-18T13:38:53Z
dc.date.issued2023
dc.description.abstractWe 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.en
dc.identifier.isbn978-3-88579-726-5
dc.identifier.pissn1617-5468
dc.identifier.urihttps://dl.gi.de/handle/20.500.12116/40119
dc.language.isoen
dc.publisherGesellschaft für Informatik e.V.
dc.relation.ispartofSoftware Engineering 2023
dc.relation.ispartofseriesLecture Notes in Informatics (LNI) - Proceedings, Volume P-332
dc.subjectsatisfiability solving
dc.subjectvariation
dc.subjectchoice calculus
dc.subjectsoftware product lines
dc.titleVariational Satisfiability Solving: Efficiently Solving Lots of Related SAT Problems - Summaryen
dc.typeText/Conference Paper
gi.citation.endPage130
gi.citation.publisherPlaceBonn
gi.citation.startPage129
gi.conference.date20.–24. Februar 2023
gi.conference.locationPaderborn
gi.conference.sessiontitleWissenschaftliches Hauptprogramm

Dateien

Originalbündel
1 - 1 von 1
Vorschaubild
Name:
paper51.pdf
Größe:
227.88 KB
Format:
Adobe Portable Document Format
Herunterladen

Sammlungen

P332 - Software Engineering 2023