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

Structure Identification with SAT (Research Project)

Project Acronym: STRIDES (Structure Identification with SAT)

Funding organization: Austrian Science Fund (FWF)

Project number: P 36420

Grant DOI: 10.55776/P36420

Project Team

 

  • Stefan Szeider (PI)
  • André Schidler
  • P.R. Vaidyanathan
  • Florentina Voboril

Topic

SAT is the famous propositional satisfiability problem. It asks to assign the variables of a propositional formula with truth values 0 and 1 such that the entire formula becomes true. SAT is generally considered intractable, but over the last twenty years, computer programs (SAT solvers) have been engineered that can solve the problem surprisingly fast. Numerous other hard problems can be translated to SAT and solved via SAT solvers. However, the translation to SAT often causes a significant increase in size, which limits the application of SAT solvers to small problem inputs.

The project aims at scaling the use of SAT solvers to large problem inputs by utilizing the recently introduced SAT-based Local Improvement Method (SLIM). It starts with an initial heuristic solution and repeatedly applies a SAT solver to small local parts of the input, overcoming the size limitation. The project will investigate using SLIM for problems that ask to find a specific hard-to-find structure in given data. Such structure identification problems arise in text data, large graphs and networks, and logical circuits. It will focus on methods for making the SLIM approach more efficient and finding general insights into its workings. The research is expected to lead to new theoretical and practical results.

Publications

16 results
2025
[16]Extracting Problem Structure with LLMs for Optimized SAT Local Search
André Schidler, Stefan Szeider
SOCS 2025, The 18th International Symposium on Combinatorial Search. August 12-15, 2025. University of Glasgow, Scotland, United Kingdom, 2025.
Note: to appear
[bibtex]
[15]StreamLLM: Enhancing Constraint Programming with Large Language Model-Generated Streamliners
Florentina Voboril, Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider
2025, IEEE Computer Soc..
Note: To appear
[bibtex]
2024
[14]SAT-based Decision Tree Learning for Large Data Sets
André Schidler, Stefan Szeider
Journal of Artificial Intelligence Research, volume 80, pages 875–918, 2024.
[bibtex]
[13]Backdoor DNFs
Sebastian Ordyniak, Andre Schidler, Stefan Szeider
Journal of Computer and System Sciences, volume 144, pages 103547, 2024.
[bibtex] [doi]
[12]SAT backdoors: Depth beats size
Jan Dreier, Sebastian Ordyniak, Stefan Szeider
Journal of Computer and System Sciences, volume 142, pages 103520, 2024.
[bibtex] [doi]
[11]Revisiting Causal Discovery from a Complexity-Theoretic Perspective
Robert Ganian, Viktoriia Korchemna, Stefan Szeider
Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24 (Kate Larson, ed.), pages 3377–3385, 8 2024, International Joint Conferences on Artificial Intelligence Organization.
Note: Main Track
[bibtex] [doi]
[10]Compilation and Fast Model Counting beyond CNF
Alexis de Colnet, Stefan Szeider, Tianwei Zhang
Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence, IJCAI-24 (Kate Larson, ed.), pages 3315–3323, 8 2024, International Joint Conferences on Artificial Intelligence Organization.
Note: Main Track
[bibtex] [doi]
[9]Small unsatisfiable k-CNFs with bounded literal occurrence
Tianwei Zhang, Tomáš Peitl, Stefan Szeider
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) (Supratik Chakraborty, Jie-Hong Roland Jiang, eds.), volume 305 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1–31:22, 2024, Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]
[8]SAT-Based Tree Decomposition with Iterative Cascading Policy Selection
Hai Xia, Stefan Szeider
AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy, Sriraam Natarajan, eds.), pages 8191–8199, 2024, AAAI Press.
[bibtex] [pdf] [doi]
[7]Structure-guided Local Improvement for Maximum Satisfiability
André Schidler, Stefan Szeider
The 30th International Conference on Principles and Practice of Constraint Programming, CP 2024 (Paul Shaw, ed.), 2024, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex]
[6]eSLIM: Circuit Minimization with SAT Based Local Improvement
Franz-Xaver Reichl, Friedrich Slivovsky, Stefan Szeider
27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024) (Supratik Chakraborty, Jie-Hong Roland Jiang, eds.), volume 305 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1–23:14, 2024, Schloss Dagstuhl – Leibniz-Zentrum für Informatik.
[bibtex] [doi]
[5]A General Theoretical Framework for Learning Smallest Interpretable Models
Sebastian Ordyniak, Giacomo Paesani, Mateusz Rychlicki, Stefan Szeider
AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy, Sriraam Natarajan, eds.), pages 10662–10669, 2024, AAAI Press.
[bibtex] [pdf] [doi]
[4]Learning Small Decision Trees for Data of Low Rank-Width
Konrad Dabrowski, Eduard Eiben, Sebastian Ordyniak, Giacomo Paesani, Stefan Szeider
AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy, Sriraam Natarajan, eds.), pages 10476–10483, 2024, AAAI Press.
[bibtex] [pdf] [doi]
[3]Hardness of Random Reordered Encodings of Parity for Resolution and CDCL
Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider
AAAI'24, the Thirty-Eighth AAAI Conference on Artificial Intelligence, February 20-27, Vancouver, Canada (Jennifer Dy, Sriraam Natarajan, eds.), pages 7978–7986, 2024, AAAI Press.
[bibtex] [pdf] [doi]
2023
[2]Proven optimally-balanced Latin rectangles with SAT
Vaidyanathan Peruvemba Ramaswamy, Stefan Szeider
Proceedings of CP 2023, the 29th International Conference on Principles and Practice of Constraint Programming (Roland Yap, ed.), volume 280 of LIPIcs, pages 48:1–48:10, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]
[1]From Data Completion to Problems on Hypercubes: A Parameterized Analysis of the Independent Set Problem
Eduard Eiben, Robert Ganian, Iyad Kanj, Sebastian Ordyniak, Stefan Szeider
18th International Symposium on Parameterized and Exact Computation, IPEC 2023, September 6-8, 2023, Amsterdam, The Netherlands (Neeldhara Misra, Magnus Wahlström, eds.), volume 285 of LIPIcs, pages 16:1–16:14, 2023, Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
[bibtex] [pdf] [doi]

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.