*NEW* High-Performance Computing for Parallel Boolean SAT(isfiability) Solving

Description

 
 - Funding - 
 
Australian citizens who undertake this project may be eligible for a
generous stipend. Please contact us to find out more.
 
 - Context -
 
This project is one stream in a larger effort that seeks to leverage
distributed compute infrastructure to drastically improve the runtime
efficiency and scalability of Boolean SAT(isfiability) solving, an in
particular SAT solving for transition system models.
 
 - Our first objective is to develop and showcase novel parallel
   approaches that are demonstrated, both theoretically and
   empirically, to be convincingly faster (walltime) than
   state-of-the-art serial procedures.
 
 - Our second objective is to develop and showcase novel parallel
   approaches that are able to efficiently solve problems whose {\em
   Conjunctive Normal Form} (CNF) is very large -- e.g., billions of
   clauses.
 
We are guided by bottlenecks in SAT solving for the following application domains:
 
 
 - Program analysis via symbolic execution; e.g. [1]
 
 - The cryptanalysis of hash functions; e.g. [2]
 
 - Analysis of security properties, and in particular privacy properties; e.g. [3]
 
 
 - Project : High-Performance Computing Workstream -
 
 
We seek to advance SAT solving system technology, with the concrete
objectives being to create a SAT system that:
 
1. Is convincingly faster (walltime) compared to existing monolithic
   serial systems – i.e., ideally we show an exponential separation,
   however at the very least a polynomial speedup factor.
 
2. Scales gracefully to problems where the given CNF representation is
   very very large – e.g., billions of clauses.
 
Our application focus shall be domains where the underlying decision
problems are most naturally modelled as state transition systems. We
expect to achieve our objectives through careful scientific
investigation of high-performance computing technologies for the
efficient and targeted discovery and communication of information
between the processing elements in a distributed search. 
 
 - Background - 
 
There are two paradigms for solving Boolean SAT problems using serial
processing: (i) stochastic local search (SLS), or otherwise (ii) a
backtracking search, such as conflict-driven clause learning (CDCL). Both
have their merits, and we note that the latter is recently considered
to be best suited, in isolation, to solving transition system
problems. Although it is somewhat debatable, most sane researchers
would say these techniques have yet to be coupled nicely.
 
Parallel computation has found a number of uses in solving SAT
problems. Parallelism can be exploited in: (i) the tuning of algorithm
configurations, (ii) search-space splitting, and (iii) portfolio
approaches. Identifying and sharing good constraints is key to
efficient parallelism. We note that bottlenecks have been identified
in the structure of resolution refutations which place hard limits on
parallelism in search-space splitting for CDCL solvers. Finally, once
we start solving bounded model checking (BMC) problems--as we expect
to do in this project--parallelisation is raised as a topic when
considering the search horizon at which to pose queries.
 
A fundamental process in any state-of-the-art symbolic execution tool
is the translation/compilation of queries to decision problems, and
then a call to a satisfiability/decision procedure which is used to
resolve the query. Mayhem and angr use the SAT (Modulo Theory) system
Z3. S2E 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 implements a bespoke
serial Boolean satisfiability procedure to solve hard decision
problems. The focus of this project shall be on developing efficient
parallelisation strategies, for variable selection, value selection,
and constraint propagation in the decision engine that underlies an
effective symbolic execution toolchain.
 
 - Bibliography - 
 
[1] Baldoni, R., Coppa, E., D’Elia, D. C., Demetrescu, C., & Finocchi, I. (2018). A survey of symbolic execution techniques. ACM Comput. Surv., 51(3).
 
[2] Mironov, I., & Zhang, L. (2006). Applications of sat solvers to cryptanalysis of hash functions. IACR Cryptology ePrint Archive.
 
[3] Cortier, V., Dallon, A., & Delaune, S. (2017). SAT-equiv: An efficient tool for equivalence properties. In 30th IEEE computer security foundations symposium, CSF 2017, santa barbara, ca, usa, august 21-25, 2017 (pp. 481–494).
 

Goals

We seek to advance SAT solving system technology, with the concrete objectives being to create a SAT system that:

 
1. Is convincingly faster (walltime) compared to existing monolithic serial systems – i.e., ideally we show an exponential separation, however at the very least a polynomial speedup factor.
 
2. Scales gracefully to problems where the given CNF representation is very very large – e.g., billions of clauses.

Background Literature

 

[1] Baldoni, R., Coppa, E., D’Elia, D. C., Demetrescu, C., & Finocchi, I. (2018). A survey of symbolic execution techniques. ACM Comput. Surv., 51(3).
 
[2] Mironov, I., & Zhang, L. (2006). Applications of sat solvers to cryptanalysis of hash functions. IACR Cryptology ePrint Archive.
 
[3] Cortier, V., Dallon, A., & Delaune, S. (2017). SAT-equiv: An efficient tool for equivalence properties. In 30th IEEE computer security foundations symposium, CSF 2017, santa barbara, ca, usa, august 21-25, 2017 (pp. 481–494).
 

Keywords

SAT, BMC, CDCL, SLS, DLS, HPC, Satisfiability

Updated:  1 November 2018/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing