SAT-Based Local Improvement Methods (SLIM)
SAT-Based Local Improvement Methods (SLIM)
Disciplines
Computer Sciences (40%); Mathematics (60%)
Keywords
-
SAT-encodings,
Hypertree Width,
Graph Width Parameters,
Clique-Width
Structural decomposition is one of the most successful approaches to the solution of hard computational problems, such as for probabilistic reasoning and computational medical diagnosis. Finding a suitable structural decomposition is itself a computationally hard problem. In this project we propose to study a new approach to finding structural decompositions. The idea is to use an exact method (in particular one that is based on satisfiability- solvers) to locally improve a heuristically obtained decomposition. Based on this new idea we will develop new algorithms for the decomposition of graphs and hypergraphs as well as for structural Bayesian Network learning. Our new approach bears the potential of achieving better decompositions for instances that are too large to be handled by exact approaches, and it also provides novel applications for satisfiability solver technology. The research will be a combination of theoretical investigations and the development and testing of prototype implementations.
- Technische Universität Wien - 100%
- Matti Järvisalo, University of Helsinki - Finland
- Mikko Koivisto, University of Helsinki - Finland
- Martin Grohe, RWTH Aachen - Germany
- Marijn J. H. Heule, Carnegie Mellon University - USA
- Sebastian Ordyniak, University of Sheffield - United Kingdom
Research Output
- 18 Citations
- 30 Publications
-
2021
Title Turbocharging Treewidth-Bounded Bayesian Network Structure Learning DOI 10.1609/aaai.v35i5.16508 Type Journal Article Author Peruvemba Ramaswamy V Journal Proceedings of the AAAI Conference on Artificial Intelligence -
2022
Title Tractable Abstract Argumentation via Backdoor-Treewidth DOI 10.1609/aaai.v36i5.20501 Type Journal Article Author Dvořák W Journal Proceedings of the AAAI Conference on Artificial Intelligence -
2023
Title Circuit Minimization with QBF-Based Exact Synthesis DOI 10.1609/aaai.v37i4.25524 Type Journal Article Author Reichl F Journal Proceedings of the AAAI Conference on Artificial Intelligence -
2023
Title Co-Certificate Learning with SAT Modulo Symmetries DOI 10.24963/ijcai.2023/216 Type Conference Proceeding Abstract Author Kirchweger M Pages 1944-1953 -
2022
Title Finding a Cluster in Incomplete Data DOI 10.4230/lipics.esa.2022.47 Type Conference Proceeding Abstract Author Eiben E Conference LIPIcs, Volume 244, ESA 2022 Pages 47:1 - 47:14 -
2022
Title PACE Solver Description: DAGer - Cutting out Cycles with MaxSAT DOI 10.4230/lipics.ipec.2022.32 Type Conference Proceeding Abstract Author Kiesel R Conference LIPIcs, Volume 249, IPEC 2022 Pages 32:1 - 32:4 -
2022
Title Weighted Model Counting with Twin-Width DOI 10.4230/lipics.sat.2022.15 Type Conference Proceeding Abstract Author Ganian R Conference LIPIcs, Volume 236, SAT 2022 Pages 15:1 - 15:17 -
2022
Title A SAT Attack on Rota's Basis Conjecture DOI 10.4230/lipics.sat.2022.4 Type Conference Proceeding Abstract Author Kirchweger M Conference LIPIcs, Volume 236, SAT 2022 Pages 4:1 - 4:18 -
2023
Title A SAT Solver's Opinion on the Erdős-Faber-Lovász Conjecture DOI 10.4230/lipics.sat.2023.13 Type Conference Proceeding Abstract Author Kirchweger M Conference LIPIcs, Volume 271, SAT 2023 Pages 13:1 - 13:17 -
2023
Title SAT-Based Generation of Planar Graphs DOI 10.4230/lipics.sat.2023.14 Type Conference Proceeding Abstract Author Kirchweger M Conference LIPIcs, Volume 271, SAT 2023 Pages 14:1 - 14:18 -
2022
Title SAT-Based Local Search for Plane Subgraph Partitions (CG Challenge) DOI 10.4230/lipics.socg.2022.74 Type Conference Proceeding Abstract Author Schidler A Conference LIPIcs, Volume 224, SoCG 2022 Pages 74:1 - 74:8 -
2022
Title Weighted Model Counting with Twin-Width DOI 10.48550/arxiv.2206.01706 Type Preprint Author Ganian R -
2022
Title A Dynamic MaxSAT-based Approach to Directed Feedback Vertex Sets DOI 10.48550/arxiv.2211.06109 Type Preprint Author Kiesel R -
2023
Title Co-Certificate Learning with SAT Modulo Symmetries DOI 10.48550/arxiv.2306.10427 Type Preprint Author Kirchweger M -
2019
Title The Parameterized Complexity of Clustering Incomplete Data DOI 10.48550/arxiv.1911.01465 Type Preprint Author Eiben E -
2020
Title Turbocharging Treewidth-Bounded Bayesian Network Structure Learning DOI 10.48550/arxiv.2006.13843 Type Preprint Author R. V -
2021
Title Formalizing Graph Trail Properties in Isabelle/HOL DOI 10.48550/arxiv.2103.03607 Type Other Author Kovacs L -
2020
Title On Existential MSO and Its Relation to ETH DOI 10.1145/3417759 Type Journal Article Author Ganian R Journal ACM Transactions on Computation Theory (TOCT) Pages 1-32 Link Publication -
2020
Title Solving the Steiner Tree Problem with few Terminals DOI 10.1109/ictai50040.2020.00054 Type Conference Proceeding Abstract Author Fichte J Pages 293-300 Link Publication -
2021
Title New width parameters for SAT and #SAT DOI 10.1016/j.artint.2021.103460 Type Journal Article Author Ganian R Journal Artificial Intelligence Pages 103460 Link Publication -
2020
Title Threshold Treewidth and Hypertree Width DOI 10.24963/ijcai.2020/263 Type Conference Proceeding Abstract Author Ganian R Pages 1898-1904 Link Publication -
2020
Title Induction with Generalization in Superposition Reasoning DOI 10.1007/978-3-030-53518-6_8 Type Book Chapter Author Hajdú M Publisher Springer Nature Pages 123-137 Link Publication -
2020
Title Formalizing Graph Trail Properties in Isabelle/HOL DOI 10.1007/978-3-030-53518-6_12 Type Book Chapter Author Kovács L Publisher Springer Nature Pages 190-205 Link Publication -
2023
Title On the parameterized complexity of clustering problems for incomplete data DOI 10.1016/j.jcss.2022.12.001 Type Journal Article Author Eiben E Journal Journal of Computer and System Sciences Pages 1-19 -
2023
Title Are hitting formulas hard for resolution? DOI 10.1016/j.dam.2023.05.003 Type Journal Article Author Peitl T Journal Discrete Applied Mathematics Pages 173-184 Link Publication -
2023
Title SAT-boosted Tabu Search for Coloring Massive Graphs DOI 10.1145/3603112 Type Journal Article Author Schidler A Journal ACM Journal of Experimental Algorithmics Pages 1-19 Link Publication -
2023
Title Computing optimal hypertree decompositions with SAT DOI 10.1016/j.artint.2023.104015 Type Journal Article Author Schidler A Journal Artificial Intelligence Pages 104015 Link Publication -
2023
Title CSP beyond tractable constraint languages DOI 10.1007/s10601-023-09362-3 Type Journal Article Author Dreier J Journal Constraints Pages 450-471 Link Publication -
2022
Title Threshold Treewidth and Hypertree Width DOI 10.1613/jair.1.13661 Type Journal Article Author Ganian R Journal Journal of Artificial Intelligence Research -
2021
Title The Parameterized Complexity of Clustering Incomplete Data DOI 10.1609/aaai.v35i8.16896 Type Journal Article Author Eiben E Journal Proceedings of the AAAI Conference on Artificial Intelligence