In this project you will study the Boolean SAT(isfiability) problem, and related combinatorial decision problems of interest in Artificial Intelligence and Computer Science.
You will gain some familiarity with search paradigms that have been developped for the SAT problem, including:
- Systematic Lookahead;
- Backtracking Search; AND
- (Stochastic) Local Search.
Over the course of the project you shall gain knowledge and understanding of how these relate, and how they can complement each other in solving problems that are challenging, either because they are very large, or apparently very difficult.
Develop and empirically evaluate new strategies for scheduling search and probing processes, in a parallel computing environment, in order to decompose and solve SAT problems relatively efficiently.
A familiarity with C and C++, or keen willingness to learn, will be useful attributes on this project.
There is an established literature that has developed and characterised SAT problem features for portfolio optimisation (e.g., [A*]), and explored machine learning techniques, and related methods in the operations research literature, for portfolio optimisation. Your work will build on this, and more recent contributions that solve SAT problems by interleaving distinct search strategies/algorithms (e.g., [B*]).
[A*] Lin Xu, Frank Hutter, Holger H. Hoos, Kevin Leyton-Brown: SATzilla: Portfolio-based Algorithm Selection for SAT. J. Artif. Intell. Res. 32: 565-606 (2008)
[B*] Armin Biere, Katalin Fazekas, Mathias Fleury, Maximillian Heisinger. CaDiCaL, Kissat, Paracooba, Plingeling and Treengeling Entering the SAT Competition 2020. In Proc. of SAT Competition 2020 - Solver and Benchmark Descriptions, Tomas Balyo, Nils Froleyks, Marijn Heule, Markus Iser, Matti Järvisalo, Martin Suda (editors), vol. B-2020-1 of Department of Computer Science Report Series B, 2020. pages 50-53, University of Helsinki, 2020.
How to get some Satisfaction?
There are two competing paradigms for solving SAT problems using serial processing: (i) stochastic local search (SLS), such as investigated by Pham, Thornton, Gretton, and Sattar (2008); Pham, Thornton, and Sattar (2007), or otherwise (ii) a backtracking search of conflict-driven clause learning (CDCL), as studied by Audemard and Simon (2009); Biere (2008). Both have their merits, and we note that the latter is recently considered to be best suited, in isolation, to solving transition system problems (Rintanen, 2012), and by employing additional bespoke propagators, transition system problems with non-determinism, as described recently by Pandey and Rintanen (2018). This project will focus on search portfolio optimisation, and especially this topic in case of large SAT probelms that are decomposed.
Why (Boolean) SAT?
One application of interest to us is in system/software verification and in controller synthesis (i.e. Automated Planning). A fundamental process in any state-of-the-art symbolic execution or automated software verification tool is the translation/compilation of queries----e.g., "Does this C program crash?"--to decision problems, and then a call a to satisfiability/decision procedure which is used to resolve the query. The Mayhem toolchain by Cha, Avgerinos, Rebert, and Brumley (2012) and angr by Shoshitaishvili et al. (2016) use the SAT (Modulo Theory) system Z3, described some years ago by de Moura and Bjørner (2008). S2E by Chipounov, Kuznetsov, and Candea (2012) supports a number of solvers, including Z3, that is to our knowledge used most frequently for "industry-strength" solving. We note that the open source (MIT License) Z3 tool itself can be characterized, for the most part in this discussion, as a bespoke implementation of a serial Boolean satisfiability procedure, such as briefly described above.
Notes of Parallel Search
Parallelism can be exploited in the tuning of algorithm configurations (Birattari, Yuan, Balaprakash, & Stützle, 2010), search-space splitting, or portfolio approaches (Hutter, Hoos, Leyton-Brown, & Stützle, 2009; M. Lindauer, Hutter, Hoos, & Schaub, 2017; M. T. Lindauer,Hoos, Hutter, & Schaub, 2015). Identifying and sharing good clauses is key to efficient parallelism (Audemard & Simon, 2009), however, Katsirelos, Sabharwal, Samulowitz, and Simon (2013) identify bottlenecks in the structure of resolution refutations which place hard limits on parallelism in search-space splitting for CDCL solvers.
Boolean Satisfiability, Artificial Intelligence, Search, Machine Learning