Algorithms and Complexity Group
  • People
  • Research
  • Courses
  • Talks
  • Jobs
  • Contact

SAT Based Local Improvement (Research Project)

Funding organization: Austrian Science Fund (FWF)

Project number: (FWF P 32441)

Project Team

Stefan Szeider (PI)

André Schidler

P.R. Vaidyanathan

Topic

Many problems can be efficiently translated into the propositional satisfiability problem (SAT) and then solved with a powerful SAT solver or variants such as MaxSAT or QBF-SAT. In some cases, the translation causes a significant blow-up in size, so this one-shot translation is not feasible. In this project, we overcome this limitation by repeatedly translating small local parts of the problem instance to SAT, which allows us to scale the SAT solver's power to large instances. We could successfully implement this approach for various critical computational problems, including learning the structure of a Bayesian network, inducing an interpretable decision tree, or minimizing a Boolean circuit.

Publications

44 results
2023
[44]SAT-Boosted Tabu Search for Coloring Massive Graphs
Andre Schidler, Stefan Szeider
J. Exp. Algorithmics, volume 2825, number 1.5, pages 1–19, 2023.
[bibtex] [doi]
[43]Are Hitting Formulas Hard for Resolution?
Tomáš Peitl, Stefan Szeider
Discr. Appl. Math., volume 337, pages 173–184, 2023.
[bibtex] [doi]
[42]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]
[41]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.), pages 2013–2021, 2023, ijcai.org.
Note: Main Track
[bibtex] [pdf] [doi]
[40]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]
[39]Circuit Minimization with QBF-Based Exact Synthesis
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
Thirty-Seventh AAAI Conference on Artificial Intelligence, AAAI 2023, Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence, IAAI 2023, Thirteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2023, Washington, DC, USA, February 7-14, 2023 (Brian Williams, Yiling Chen, Jennifer Neville, eds.), pages 4087–4094, 2023, AAAI Press.
[bibtex] [pdf] [doi]
[38]The Parameterized Complexity of Finding Concise Local Explanations
Sebastian Ordyniak, Giacomo Paesani, Stefan Szeider
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 3312–3320, 2023, ijcai.org.
[bibtex] [pdf] [doi]
[37]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.), volume 271 of LIPIcs, pages 14:1–14:18, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [doi]
[36]Co-Certificate Learning with SAT Modulo Symmetries
Markus Kirchweger, Tomáš Peitl, Stefan Szeider
Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI 2023, 19th-25th August 2023, Macao, SAR, China, pages 1944–1953, 2023, ijcai.org.
Note: Main Track
[bibtex] [pdf] [doi]
[35]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.), volume 271 of LIPIcs, pages 8:1–8:13, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [doi]
[34]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.), pages 3184–3192, 2023, ijcai.org.
Note: Main Track
[bibtex] [pdf] [doi]
[33]The Computational Complexity of Concise Hypersphere Classification
Eduard Eiben, Robert Ganian, Iyad Kanj, Sebastian Ordyniak, Stefan Szeider
Proceedings of the 40th International Conference on Machine Learning, ICML 2023, pages 9060–9070, 2023, PMLR.
[bibtex] [pdf]
2022
[32]Threshold Treewidth and Hypertree Width
Robert Ganian, Andre Schidler, Manuel Sorge, Stefan Szeider
Journal of Artificial Intelligence Research, volume 74, pages 1687–1713, 2022.
[bibtex] [pdf] [doi]
[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]

 

News

  • Best Paper Award at SOFSEM 2025

    Best Paper Award at SOFSEM 2025

    2025-01-23
    Thomas Depian, Simon D. Fink, Alexander Firbas, Robert Ganian, and Martin Nöllenburg received the Best Paper Award for their paper …Read More »
  • Markus Wallinger receives Award of Excellence for his PhD Thesis

    Markus Wallinger receives Award of Excellence for his PhD Thesis

    2024-12-05
    Our former group member Markus Wallinger won the Award of Excellence by the Federal Ministry for Education, Science and Research. …Read More »
  • Thomas Depian receives State Prize for his Master’s Thesis

    Thomas Depian receives State Prize for his Master’s Thesis

    2024-11-21
    Our group member Thomas Depian won the Appreciation Award given by the Federal Ministry for Education, Science and Research. This …Read More »
  • Best Paper Award at GECCO 2024 for M. Bresich, G. Raidl, and S. Limmer

    Best Paper Award at GECCO 2024 for M. Bresich, G. Raidl, and S. Limmer

    2024-07-24
    Maria Bresich, Günther Raidl, and Steffen Limmer received the best paper award at the 2024 Genetic and Evolutionary Computation Conference …Read More »
  • Welcome to our Feodor Lynen Fellow Dr. Frank Sommer

    Welcome to our Feodor Lynen Fellow Dr. Frank Sommer

    2024-06-14
    On June 1, 2024, Dr. Frank Sommer has joined the Algorithms and Complexity group with a prestigious Feodor Lynen postdoc …Read More »

News archive

All news for 2015, 2016, 2017, 2018, 2019, 2020, 2021, 2022, 2023 and 2024.
TU Wien Informatics
Offenlegung (§25 MedienG) Inhaber der Website ist das Institut für Logic and Computation an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. – Disclaimer – Datenschutzerklärung
Log in requires cookies.