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
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
31 results| 2026 | |
| [31] | A General Theoretical Framework for Learning Smallest Interpretable Models Artificial Intelligence, volume 350, pages 104441, 2026. |
| [30] | From Data Completion to Problems on Hypercubes: A Parameterized Analysis of the Independent Set Problem Algorithmica, volume 88, number 1, pages 8, 2026. |
| [29] | OBDDs, SDDs, and Circuits of Bounded Width: Completeness Matters Artificial Intelligence, volume 351, pages 104458, 2026. |
| [28] | Streamliners for Answer Set Programming Proceedings of the 42nd International Conference on Logic Programming (ICLP 2026), 2026. Note: To appear |
| [27] | MaxSAT-Based Compression for Tsetlin Machines Proceedings of the 43rd International Conference on Machine Learning, ICML 2026, July 6–11, 2026, Seoul, South Korea, 2026. Note: To appear |
| [26] | VIPR Certificate Construction from Black-Box ILP Solvers 32nd International Conference on Principles and Practice of Constraint Programming, CP 2026, July 20–23, 2026, Lisbon, Portugal, 2026, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Note: To appear |
| [25] | CP-Agent: Agentic Constraint Programming Proceedings of the 3rd International Workshop on Large Language Models for Code (LLM4Code '26), 2026, Assoc. Comput. Mach., New York. Note: To appear; preprint: CoRR abs/2508.07468, https://arxiv.org/abs/2508.07468 |
| [24] | Computing Probabilistic Explanations for ML Models: Fixed-Parameter Algorithms The 40th Annual AAAI Conference on Artificial Intelligence, AAAI-2026, pages 24622–24629, 2026. |
| [23] | Smart Cubing for Graph Search: A Comparative Study 32nd International Conference on Principles and Practice of Constraint Programming, CP 2026, July 20–23, 2026, Lisbon, Portugal, 2026, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Note: To appear; preprint: CoRR abs/2501.17201, https://arxiv.org/abs/2501.17201 |
| 2025 | |
| [22] | Generating Streamlining Constraints with Large Language Models Journal of Artificial Intelligence Research, volume 84, pages 16:1–16:19, 2025. Note: Abstract reprint in AAAI 2026, page 39900 |
| [21] | StreamLLM: Enhancing Constraint Programming with Large Language Model-Generated Streamliners 2025 IEEE/ACM 1st International Workshop on Neuro-Symbolic Software Engineering (NSE), pages 17-22, 5 2025, IEEE Computer Soc.. |
| [20] | Balancing Latin Rectangles with LLM-Generated Streamliners 31st International Conference on Principles and Practice of Constraint Programming, CP 2025, August 10-15, 2025, Glasgow, Scotland (Maria Garcia de la Banda, ed.), volume 340 of LIPIcs, pages 36:1–36:17, 2025, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
| [19] | Bridging Language Models and Symbolic Solvers via the Model Context Protocol 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, August 12-15, 2025, Glasgow, Scotland (Jeremias Berg, Jakob Nordström, eds.), volume 341 of LIPIcs, pages 30:1–30:12, 2025, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
| [18] | Extracting Problem Structure with LLMs for Optimized SAT Local Search SOCS 2025, The 18th International Symposium on Combinatorial Search. August 12-15, 2025. University of Glasgow, Scotland, United Kingdom, 2025. |
| [17] | Analyzing Reformulation Performance in Core-Guided MaxSAT Solving 28th International Conference on Theory and Applications of Satisfiability Testing, SAT 2025, August 12-15, 2025, Glasgow, Scotland (Jeremias Berg, Jakob Nordström, eds.), volume 341 of LIPIcs, pages 26:1–26:18, 2025, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
| [16] | Optimal Decision Tree Pruning Revisited: Algorithms and Complexity Forty-second International Conference on Machine Learning, ICML 2025, Vancouver, BC, Canada, July 13-19, 2025, 2025, OpenReview.net. |
| [15] | Uncovering and Verifying Optimal Community Structure in Complex Networks: A MaxSAT Approach Computational Science - ICCS 2025 - 25th International Conference, Singapore, July 7-9, 2025, Proceedings, Part II (Michael H. Lees, Wentong Cai, Siew Ann Cheong, Yi Su, David Abramson, Jack J. Dongarra, Peter M. A. Sloot, eds.), volume 15904 of Lecture Notes in Computer Science, pages 35–49, 2025, Springer Verlag. |
| 2024 | |
| [14] | SAT-based Decision Tree Learning for Large Data Sets Journal of Artificial Intelligence Research, volume 80, pages 875–918, 2024. |
| [13] | Backdoor DNFs Journal of Computer and System Sciences, volume 144, pages 103547, 2024. |
| [12] | SAT backdoors: Depth beats size Journal of Computer and System Sciences, volume 142, pages 103520, 2024. |
| [11] | Revisiting Causal Discovery from a Complexity-Theoretic Perspective 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 |
| [10] | Compilation and Fast Model Counting beyond CNF 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 |
| [9] | Small unsatisfiable k-CNFs with bounded literal occurrence 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. |
| [8] | SAT-Based Tree Decomposition with Iterative Cascading Policy Selection 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. |
| [7] | Structure-guided Local Improvement for Maximum Satisfiability The 30th International Conference on Principles and Practice of Constraint Programming, CP 2024 (Paul Shaw, ed.), 2024, Schloss Dagstuhl - Leibniz-Zentrum für Informatik. |
| [6] | eSLIM: Circuit Minimization with SAT Based Local Improvement 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. |
| [5] | A General Theoretical Framework for Learning Smallest Interpretable Models 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. |
| [4] | Learning Small Decision Trees for Data of Low Rank-Width 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. |
| [3] | Hardness of Random Reordered Encodings of Parity for Resolution and CDCL 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. |
| 2023 | |
| [2] | Proven optimally-balanced Latin rectangles with SAT 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. |
| [1] | From Data Completion to Problems on Hypercubes: A Parameterized Analysis of the Independent Set Problem 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. |
