SAT Based Local Improvement (Research Project)

Funding organization: Austrian Science Fund (FWF)

Project Team

Topic

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.

Publications

44 results

2023
[44]	The Silent (R)evolution of SAT Johannes K. Fichte, Daniel Le Berre, Markus Hecher, Stefan Szeider Communications of the ACM, volume 66, number 6, pages 64–72, June 2023. [bibtex] [doi]
[43]	SAT-Boosted Tabu Search for Coloring Massive Graphs Andre Schidler, Stefan Szeider J. Exp. Algorithmics, 2023. Note: to appear [bibtex]
[42]	Are Hitting Formulas Hard for Resolution? Tomáš Peitl, Stefan Szeider Discr. Appl. Math., volume 337, pages 173–184, 2023. [bibtex] [doi]
[41]	On the parameterized complexity of clustering problems for incomplete data Eduard Eiben, Robert Ganian, Iyad Kanj, Sebastian Ordyniak, Stefan Szeider Journal of Computer and System Sciences, volume 134, pages 1–19, 2023. [bibtex] [doi]
[40]	Computing twin-width with SAT and branch & bound Andre Schidler, Stefan Szeider The 32nd International Joint Conference on Artificial Intelligence (IJCAI-23), August 19–25, 2023, Macao, S.A.R. (Edith Elkind, ed.), 2023, International Joint Conferences on Artificial Intelligence Organization. Note: Main Track, to appear [bibtex]
[39]	A Dynamic MaxSAT-based Approach to Directed Feedback Vertex Sets Rafael Kiesel, André Schidler Proceedings of the Symposium on Algorithm Engineering and Experiments, ALENEX 2023, Florence, Italy, January 22-23, 2023 (Gonzalo Navarro, Julian Shun, eds.), pages 39–52, 2023, SIAM. [bibtex] [doi]
[38]	Circuit Minimization with QBF-Based Exact Synthesis Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, 2023, AAAI Press. Note: to appear [bibtex]
[37]	The Parameterized Complexity of Finding Concise Local Explanations Sebastian Ordyniak, Giacomo Paesani, Stefan Szeider The 32nd International Joint Conference on Artificial Intelligence (IJCAI-23), August 19–25, 2023, Macao, S.A.R. (Edith Elkind, ed.), 2023, International Joint Conferences on Artificial Intelligence Organization. Note: Main Track, to appear [bibtex]
[36]	SAT-Based Generation of Planar Graphs Markus Kirchweger, Manfred Scheucher, Stefan Szeider The 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), July 04-08, 2023, Alghero, Italy (Meena Mahajan, Friedrich Slivovsky, eds.), 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Note: to appear [bibtex]
[35]	A SAT Solver's Opinion on the Erdős-Faber-Lovász Conjecture Markus Kirchweger, Tomáš Peitl, Stefan Szeider The 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), July 04-08, 2023, Alghero, Italy (Meena Mahajan, Friedrich Slivovsky, eds.), 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Note: to appear [bibtex]
[34]	Co-Certificate Learning with SAT Modulo Symmetries Markus Kirchweger, Tomas Peitl, Stefan Szeider The 32nd International Joint Conference on Artificial Intelligence (IJCAI-23), August 19–25, 2023, Macao, S.A.R. (Edith Elkind, ed.), 2023, International Joint Conferences on Artificial Intelligence Organization. Note: Main Track, to appear [bibtex]
[33]	IPASIR-UP: User Propagators for CDCL Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere The 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), July 04-08, 2023, Alghero, Italy (Meena Mahajan, Friedrich Slivovsky, eds.), 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Note: to appear [bibtex]
[32]	Learning Small Decision Trees with Large Domain Eduard Eiben, Sebastian Ordyniak, Giacomo Paesani, Stefan Szeider The 32nd International Joint Conference on Artificial Intelligence (IJCAI-23), August 19–25, 2023, Macao, S.A.R. (Edith Elkind, ed.), 2023, International Joint Conferences on Artificial Intelligence Organization. Note: Main Track, to appear [bibtex]
2022
[31]	Learning Large Bayesian Networks with Expert Constraints Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider 38th Conference on Uncertainty in Artificial Intelligence (UAI 2022), Eindhoven, Netherlands, August 1–5, 2022 (James Cussens, Kun Zhang, eds.), pages 180:1592–1601, 2022. [bibtex] [pdf]
[30]	A SAT Approach to Twin-Width André Schidler, Stefan Szeider Proceedings of ALENEX 2022, the 24nd SIAM Symposium on Algorithm Engineering and Experiments (Cynthia A. Phillips, Bettina Speckmann, eds.), pages 67–77, 2022, Society for Industrial and Applied Mathematics (SIAM). [bibtex] [pdf] [doi]
[29]	PACE Solver Description: DAGer - Cutting out Cycles with MaxSAT Rafael Kiesel, André Schidler 17th International Symposium on Parameterized and Exact Computation, IPEC 2022, September 7-9, 2022, Potsdam, Germany (Holger Dell, Jesper Nederlof, eds.), volume 249 of LIPIcs, pages 32:1–32:4, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. [bibtex] [pdf] [doi]
[28]	SAT-Based Local Search for Plane Subgraph Partitions (CG Challenge) André Schidler 38th International Symposium on Computational Geometry, SoCG 2022, June 7-10, 2022, Berlin, Germany (Xavier Goaoc, Michael Kerber, eds.), volume 224 of LIPIcs, pages 74:1–74:8, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. [bibtex] [pdf] [doi]
[27]	A SAT Attack on Rota’s Basis Conjecture Markus Kirchweger, Manferd Scheucher, Stefan Szeider 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel (Kuldeep S. Meel, Ofer Strichman, eds.), volume 236 of LIPIcs, pages 4:1–4:18, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. [bibtex] [pdf] [doi]
[26]	Weighted Model Counting with Twin-Width Robert Ganian, Filip Pokrývka, Andre Schidler, Kirill Simonov, Stefan Szeider 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel (Kuldeep S. Meel, Ofer Strichman, eds.), volume 236 of LIPIcs, pages 15:1–15:17, 2022, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. [bibtex] [pdf] [doi]
[25]	Finding a Cluster in Incomplete Data Eduard Eiben, Robert Ganian, Iyad Kanj, Sebastian Ordyniak, Stefan Szeider 30th Annual European Symposium on Algorithms (ESA 2022) (Shiri Chechik, Gonzalo Navarro, Eva Rotenberg, Grzegorz Herman, eds.), volume 244 of Leibniz International Proceedings in Informatics (LIPIcs), pages 47:1–47:14, 2022, Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [bibtex] [pdf] [doi]
[24]	Tractable Abstract Argumentation via Backdoor-Treewidth Wolfgang Dvorak, Markus Hecher, Matthias König, Andre Schidler, Stefan Szeider, Stefan Woltran Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, Thirty-Fourth Conference on Innovative Applications of Artificial Intelligence, IAAI 2022, The Twelveth Symposium on Educational Advances in Artificial Intelligence, EAAI 2022 Virtual Event, February 22 - March 1, 2022, pages 5608–5615, 2022, AAAI Press. [bibtex] [pdf]
[23]	SAT Backdoors: Depth Beats Size Jan Dreier, Sebastian Ordyniak, Stefan Szeider 30th Annual European Symposium on Algorithms (ESA 2022) (Shiri Chechik, Gonzalo Navarro, Eva Rotenberg, Grzegorz Herman, eds.), volume 244 of Leibniz International Proceedings in Informatics (LIPIcs), pages 46:1–46:18, 2022, Schloss Dagstuhl – Leibniz-Zentrum für Informatik. [bibtex] [pdf] [doi]
2021
[22]	Finding the Hardest Formulas for Resolution Tomáš Peitl, Stefan Szeider Journal of Artificial Intelligence Research, volume 72, pages 69–97, 2021. Note: Conference Award Track, best paper CP 2020 [bibtex] [doi]
[21]	Learning fast-inference Bayesian networks Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider Proceedings of NeurIPS 2021, the Thirty-fifth Conference on Neural Information Processing Systems (M. Ranzato, A. Beygelzimer, K. Nguyen, P.S. Liang, J.W. Vaughan, Y. Dauphin, eds.), pages 17852–17863, 2021. [bibtex] [pdf]
[20]	Turbocharging Treewidth-Bounded Bayesian Network Structure Learning Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider Proceeding of AAAI-21, the Thirty-Fifth AAAI Conference on Artificial Intelligence, pages 3895–3903, 2021, AAAI Press. [bibtex] [pdf]
[19]	Computing Optimal Hypertree Decompositions with SAT Andre Schidler, Stefan Szeider Proceeding of IJCAI-21, the 30th International Joint Conference on Artificial Intelligence (Zhi-Hua Zhou, ed.), 2021. [bibtex] [doi]
[18]	SAT-based Decision Tree Learning for Large Data Sets André Schidler, Stefan Szeider Proceeding of AAAI-21, the Thirty-Fifth AAAI Conference on Artificial Intelligence, pages 3904–3912, 2021, AAAI Press. [bibtex] [pdf]
[17]	Finding the Hardest Formulas for Resolution (Extended Abstract) Tomáš Peitl, Stefan Szeider Proceeding of IJCAI-21, the 30th International Joint Conference on Artificial Intelligence (Zhi-Hua Zhou, ed.), pages 4814–4818, 2021. Note: Sister Conferences Best Papers [bibtex] [doi]
[16]	Parameterized Complexity of Small Decision Tree Learning Sebastian Ordyniak, Stefan Szeider Proceeding of AAAI-21, the Thirty-Fifth AAAI Conference on Artificial Intelligence, pages 6454–6462, 2021, AAAI Press. [bibtex] [pdf]
[15]	Backdoor DNFs Sebastian Ordyniak, Andre Schidler, Stefan Szeider Proceeding of IJCAI-2021, the 30th International Joint Conference on Artificial Intelligence (Zhi-Hua Zhou, ed.), pages 1403–1409, 2021. [bibtex] [doi]
[14]	SAT Modulo Symmetries for Graph Generation Markus Kirchweger, Stefan Szeider Proceeings of CP 2021, the 27th International Conference on Principles and Practice of Constraint Programming (Laurent D. Michel, ed.), pages 39:1–-39:17, 2021, Dagstuhl Publishing. [bibtex] [pdf] [doi]
[13]	The Parameterized Complexity of Clustering Incomplete Data Eduard Eiben, Robert Ganian, Iyad Kanj, Sebastian Ordyniak, Stefan Szeider Proceeding of AAAI-21, the Thirty-Fifth AAAI Conference on Artificial Intelligence, pages 7296–7304, 2021, AAAI Press. [bibtex] [pdf]
2020
[12]	On Existential MSO and Its Relation to ETH Robert Ganian, Ronald de Haan, Iyad Kanj, Stefan Szeider ACM Trans. Comput. Theory, volume 12, number 4, pages 22:1–22:32, 2020. [bibtex] [pdf] [doi]
[11]	MaxSAT-Based Postprocessing for Treedepth Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider Proceedings of CP 2020, the 26th International Conference on Principles and Practice of Constraint Programming (Helmut Simonis, ed.), volume 12333 of Lecture Notes in Computer Science, pages 478–495, 2020, Springer Verlag. [bibtex] [pdf] [doi]
[10]	A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth Friedrich Slivovsky, Stefan Szeider Proceedings of SAT 2020, The 23rd International Conference on Theory and Applications of Satisfiability Testing (Luca Pulina, Martina Seidl, eds.), volume 12178 of Lecture Notes in Computer Science, pages 267–276, 2020, Springer Verlag. [bibtex] [pdf]
[9]	Short Q-Resolution Proofs with Homomorphisms Ankit Shukla, Friedrich Slivovsky, Stefan Szeider Proceedings of SAT 2020, The 23rd International Conference on Theory and Applications of Satisfiability Testing (Luca Pulina, Martina Seidl, eds.), volume 12178 of Lecture Notes in Computer Science, pages 412–428, 2020, Springer Verlag. [bibtex] [pdf]
[8]	Computing Optimal Hypertree Decompositions André Schidler, Stefan Szeider Proceedings of ALENEX 2020, the 22nd SIAM Symposium on Algorithm Engineering and Experiments (Guy Blelloch, Irene Finocchi, eds.), pages 1–11, 2020, Society for Industrial and Applied Mathematics (SIAM). [bibtex] [pdf]
[7]	Finding the Hardest Formulas for Resolution Tomáš Peitl, Stefan Szeider Proceedings of CP 2020, the 26th International Conference on Principles and Practice of Constraint Programming (Helmut Simonis, ed.), volume 12333 of Lecture Notes in Computer Science, pages 514–530, 2020, Springer Verlag. Note: Best Paper Award [bibtex] [pdf]
[6]	Formalizing Graph Trail Properties in Isabelle/HOL Laura Kovács, Hanna Lachnitt, Stefan Szeider Intelligent Computer Mathematics - 13th International Conference, CICM 2020, Bertinoro, Italy, July 26-31, 2020, Proceedings (Christoph Benzmüller, Bruce R. Miller, eds.), volume 12236 of Lecture Notes in Computer Science, pages 190–205, 2020, Springer Verlag. [bibtex] [pdf]
[5]	Threshold Treewidth and Hypertree Width Robert Ganian, Andre Schidler, Manuel Sorge, Stefan Szeider Proceeding of IJCAI-PRICAI2020, the 29th International Joint Conference on Artificial Intelligence and the 17th Pacific Rim International Conference on Artificial Intelligence, pages 1898–1904, 2020. [bibtex] [pdf] [doi]
[4]	Fixed-Parameter Tractability of Dependency QBF with Structural Parameters Robert Ganian, Tomáš Peitl, Friedrich Slivovsky, Stefan Szeider Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020 (Diego Calvanese, Esra Erdem, Michael Thielscher, eds.), pages 392–402, 2020. [bibtex] [pdf]
[3]	On the Parameterized Complexity of Clustering Incomplete Data into Subspaces of Small Rank Robert Ganian, Iyad Kanj, Sebastian Ordyniak, Stefan Szeider Proceeding of AAAI-20, the Thirty-Fourth AAAI Conference on Artificial Intelligence, February 7–12, 2020, New York, pages 3906–3913, 2020, AAAI Press. [bibtex] [pdf]
[2]	Breaking Symmetries with RootClique and LexTopsort Johannes K. Fichte, Markus Hecher, Stefan Szeider Proceedings of CP 2020, the 26th International Conference on Principles and Practice of Constraint Programming (Helmut Simonis, ed.), volume 12333 of Lecture Notes in Computer Science, pages 286–303, 2020, Springer Verlag. [bibtex] [pdf]
[1]	A Time Leap Challenge for SAT-Solving Johannes K. Fichte, Markus Hecher, Stefan Szeider Proceedings of CP 2020, the 26th International Conference on Principles and Practice of Constraint Programming (Helmut Simonis, ed.), volume 12333 of Lecture Notes in Computer Science, pages 267–285, 2020, Springer Verlag. [bibtex] [pdf]