D6.8: State of the art of SAT and PSA solvers in the light of quantum computing
Creators: name: Hibti, Mohamed
name: Zaiou, Ahmed
name: Younès Bennani,
name: Basarab Matei
Publisher: name: Zenodo
Year: 2022
Subjects: SAT solvers
benchmark
quantum SAT
quantum PSA

description: The main objective of this report is to understand the main factors that may help to solve fault tree analysis problems using quantum algorithms. It turns out that fault tree analysis can be considered an extended variant of Boolean Satisfiability Problem (SAT) which has attracted for decades a lot of research e˙orts from people and communities with a strong background on computer science and, particularly, in computational complexity related disciplines. Many solvers exist for SAT and an annual competition is organized every year to push forward the performances of the algorithms to solve SAT instances. In this report, an overview of last SAT competition winners is provided. Main review objectives were getting an idea of the different strategies and heuristics for solving SAT problems, understanding where the complexity of these algorithms is located and how non chronological search algorithms succeed to solve complex and big instances. The ultimate goal is to see to what extent these strategies can be embedded to enhance the design of hybrid quantum algorithms. Indeed, up to now the quantum algorithm that were already designed to solve either SAT or Probabilistic Safety Assessment (PSA) are limited by the hardware limitation regarding the number of available qubits and the decoherence time. After a brief presentation of the main SAT-solvers, a synthesis of the experiments and results of the last SAT-competitions is presented, with an indication of the minimal and maximal sizes of the different instances that were solved. This confirms that these instances, can be generally at least as big as the industrial instances one can find in the reliability problems (or fault tree analysis) for complex industrial systems. Regarding the instances’s complexity, we should note that the nature of the industrial instances has many particularities that one take can consider for simplification. Indeed, aside from redundancies (which may be the most complexity related aspect), there are many symmetries and modules that could be simplified for better performances. Different quantum algorithms are presented to deal with SAT, they fall in different classes of quantum algorithms: Quantum walks, Harrow-Hassidim-Lloyd (HHL) based algorithms, Adiabatic algorithms, Chaotic dynamics, Ground state quantum computer algorithms, Parallel quantum algorithm, Cooperative search algorithm, Divide and Quantum. For the PSA problem, in addition to many of the SAT algorithms that can be also used, we present other more specific algorithms: Direct implementation with reversible game pebbling or ZX directed optimization, a vertex separator quantum algorithm, quantum unconstrained binary optimization a counting/grover algorithm We present some tests on different small instances of fault trees and show that scaling remains an important question and therefore requires a focus on efficient hybrid approaches that combine performant classical solvers with a relevant use of quantum superposition when it matters.