Structure Identification with SAT (STRIDES)
Structure Identification with SAT (STRIDES)
Disciplines
Computer Sciences (20%); Mathematics (80%)
Keywords
-
SAT-encodings,
Relational structure identification,
Recursive Backdoors,
Pseudo-Boolean Solving,
PySAT,
MaxSAT Solving
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.
- Technische Universität Wien - 100%
- Günther R. Raidl, Technische Universität Wien , national collaboration partner
- Nysret Musliu, Technische Universität Wien , national collaboration partner
- Alexey Ignatiev, Monash University - Australia
- Serge Gaspers, The University of New South Wales - Australia
- Daniel Leberre, Université d Artois - France
- Sebastiani Roberto, Università di Trento - Italy
- Carlos Ansotegui, Universitat de Lleida - Spain
Research Output
- 2 Citations
- 4 Publications
-
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 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 -
2024
Title Backdoor DNFs DOI 10.1016/j.jcss.2024.103547 Type Journal Article Author Ordyniak S Journal Journal of Computer and System Sciences Pages 103547 Link Publication -
2024
Title SAT backdoors: Depth beats size DOI 10.1016/j.jcss.2024.103520 Type Journal Article Author Dreier J Journal Journal of Computer and System Sciences Pages 103520 Link Publication