Navigation menu menu

Automated Reasoning - ML Search Heuristics - "Where to next?!" Project

People

Supervisor

Description

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.

Goals

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.

Requirements

A familiarity with C and C++, or keen willingness to learn, will be useful attributes on this project. 

Background Literature

Core Literature

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?

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.

 

Gain

Scholarships are available for AU/NZ university students who wish to do an honours research year of study at the Australian National University. 

https://www.anu.edu.au/study/scholarships/find-a-scholarship/co-lab-honours-grant

Keywords

Boolean SAT(isfiability),Artificial Intelligence, Machine Learning, Search

Updated:  10 August 2021/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing