<div class="csl-bib-body">
<div class="csl-entry">Kirchweger, M. (2023). <i>Dynamic symmetry breaking for SAT-encodings of combinatorial problems</i> [Diploma Thesis, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2023.98841</div>
</div>
-
dc.identifier.uri
https://doi.org/10.34726/hss.2023.98841
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/177268
-
dc.description.abstract
We propose a novel SAT-based approach to graph generation. Our approach utilizes the interaction between a CDCL SAT solver and a special symmetry propagator where the SAT solver runs on an encoding of the desired graph property. The symmetry propagator checks partially generated graphs for minimality with respect to a lexicographic ordering during the solving process. This approach has several advantages over a static symmetry breaking: (i) symmetries are detected early in the generation process, (ii) symmetry breaking is seamlessly integrated into the CDCL procedure, and (iii) the propagator can perform a complete symmetry breaking without causing a prohibitively largeinitial encoding. We instantiate our approach by generating extremal graphs with certain restrictions in terms of forbidden subgraphs and diameter. With our approach, we could confirm the Murty-Simon Conjecture (1979) on diameter-2-critical graphs for graphs up to 19 vertices and prove the completeness of sets of Ramsey graphs with certain parameters.
en
dc.language
English
-
dc.language.iso
en
-
dc.rights.uri
http://rightsstatements.org/vocab/InC/1.0/
-
dc.subject
SAT
de
dc.subject
Symmetriebrechen
de
dc.subject
kombinatorische Probleme
de
dc.subject
SAT
en
dc.subject
symmetry breaking
en
dc.subject
combinatorial problems
en
dc.title
Dynamic symmetry breaking for SAT-encodings of combinatorial problems
en
dc.title.alternative
Dynamisches Brechen von Symmetrien bei SAT-Enkodierungen kombinatorischer Probleme
de
dc.type
Thesis
en
dc.type
Hochschulschrift
de
dc.rights.license
In Copyright
en
dc.rights.license
Urheberrechtsschutz
de
dc.identifier.doi
10.34726/hss.2023.98841
-
dc.contributor.affiliation
TU Wien, Österreich
-
dc.rights.holder
Markus Kirchweger
-
dc.publisher.place
Wien
-
tuw.version
vor
-
tuw.thesisinformation
Technische Universität Wien
-
tuw.publication.orgunit
E192 - Institut für Logic and Computation
-
dc.type.qualificationlevel
Diploma
-
dc.identifier.libraryid
AC16856042
-
dc.description.numberOfPages
70
-
dc.thesistype
Diplomarbeit
de
dc.thesistype
Diploma Thesis
en
dc.rights.identifier
In Copyright
en
dc.rights.identifier
Urheberrechtsschutz
de
tuw.advisor.staffStatus
staff
-
tuw.advisor.orcid
0000-0001-8994-1656
-
item.languageiso639-1
en
-
item.mimetype
application/pdf
-
item.openairecristype
http://purl.org/coar/resource_type/c_bdcc
-
item.fulltext
with Fulltext
-
item.openairetype
master thesis
-
item.grantfulltext
open
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
crisitem.author.dept
E192-01 - Forschungsbereich Algorithms and Complexity