In this project you will study the Boolean SAT(isfiability) problem, and related combinatorial decision problems of interest in Artificial Intelligence and Computer Science.
The aim of the project is to develop and evaluate novel heuristics for guiding a conflict-driven clause learning procedure -- I.e., variable and value selection heuristics. In particular, assuming a parallel computing environment there are opportunities to probe subproblems to find succinct families of strong resolvants, autarchies, etc., and to use machine learning to acquire problem-specific search guidance.
Speedup search exercises in large structured problems that appear in recent international SAT competitions/challenges, and in particular Boolean SAT queries of interest to automated software engineering and planning.
A familiarity with C and C++, or keen willingness to learn, will be useful attributes on this project.
Knot Pipatsrisawat, Adnan Darwiche: On the power of clause-learning SAT solvers as resolution engines. Artif. Intell. 175(2): 512-525 (2011)
Jia Hui Liang, Hari Govind V K, Pascal Poupart, Krzysztof Czarnecki, Vijay Ganesh. An Empirical Study of Branching Heuristics Through the Lens of Global Learning Rate. 20th International Conference on Theory and Applications of Satisfiability Testing (SAT 2017) August 29, 2017.
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 CDCL, related limited resolution procedures, and search concepts (e.g. lookahead, probing, etc.).
Why (Boolean) SAT?
Boolean SAT(isfiability),Artificial Intelligence, Machine Learning, Search