Speculative programming for solving computationally difficult problems
- Advisor :
- Gilles Audemard
- Funding : Artois, Région HdF
For some years now, SAT solvers have been used to solve a wide variety of problems, ranging from cryptanalysis (Trimoska, Dequen, and Ionica 2021) to bioinformatics (Guerra and Lynce 2012), mathematical conjecture closure (Heule, Kullmann, and Marek 2016), decision tree learning (Schidler and Szeider 2021), and neural network verification (Narodytska et al. 2018). Indeed, it is common today to use SAT solvers as oracles to solve problems of higher complexity.
It is then interesting to use parallel programming to solve such problems. This has been widely studied in the past (Audemard and Simon 2014; Heule, Kullmann, and Biere 2018). Despite this, most of the proposed approaches are based on two complementary paradigms, the portfolio approach and the divide and conquer approach. The goal of this thesis is to explore another parallel search paradigm, namely speculative search. Generally speaking, this type of programming consists of executing tasks before knowing if they are necessary (see for example (Osborne 1990)).
The objective of this thesis is to study and implement this speculative programming on various types of problems.
Gilles Audemard and Laurent Simon. 2014. “Lazy Clause Exchange Policy for Parallel SAT Solvers.” In Theory and Applications of Satisfiability Testing - SAT, pp 197–205.
Gilles Audemard, Jean-Marie Lagniez, Nicolas Szczepanski, Sébastien Tabary: ‘A Distributed Version of Syrup”. In Theory and Applications of Satisfiability Testing - SAT 2017.
Gilles Audemard, Jean-Marie Lagniez, Laurent Simon: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction. In Theory and Applications of Satisfiability Testing - SAT 2013.
Bacchus, Fahiem, Matti Järvisalo, and Ruben Martins. “Maximum Satisfiability.” In Handbook of Satisfiability, 2021.
Jessica Davies, Jessica, and Fahiem Bacchus. “Solving MAXSAT by Solving a Sequence of Simpler SAT Instances.” In Principles and Practice of Constraint Programming - CP 2011
Marjin Heule, Marijn, Oliver Kullmann, and Armin Biere. 2018. “Cube-and-Conquer for Satisfiability.” In Handbook of Parallel Constraint Reasoning,
Daniel Le Berre, Romain Wallon, 2021. “ On dedicated CDCL strategies for pseudo-Boolean solvers“. In Theory and Applications of Satisfiability Testing - SAT 2017.
Nina Narodytska, Shiva Prasad Kasiviswanathan, Leonid Ryzhyk, Mooly Sagiv, and Toby Walsh. 2018. “Verifying Properties of Binarized Deep Neural Networks.” In Proceedings of the Thirty-Second AAAI, 2018.
Randy Osborne, 1990. “Speculative Computation in Multilisp.” In Proceedings of the 1990 ACM Conference on LISP and Functional Programming, LFP 1990, Nice, France, 27-29 June 1990, 198–208. ACM. https://doi.org/10.114 5/91556.91644.
Wallon, Romain. 2021. “On Improving the Backjump Level in PB Solvers.” In 12th International Workshop on Pragmatics of SAT (SAT’21).
See the offer on ADUM