Pseudo-Boolean Black-Box Optimization Methods in the Context of Divide-and-Conquer Approach to Solving Hard SAT Instances

Oleg ZAIKIN, Stepan KOCHEMAZOV

Abstract


Solving hard instances of the Boolean satisfiability problem (SAT) in practice is an interestingly nontrivial area. In particular, the heuristic nature of state-of-the-art SAT solvers makes it impossible to know in advance how long it will take to solve any particular SAT instance. One way of coping with this disadvantage is the divide-and-conquer approach when an original SAT instance is decomposed into several simpler subproblems. However, the way it is decomposed plays a crucial role in the resulting effectiveness of solving. In the present study, we reduce the problem of “dividing” a hard SAT instance into many simpler subproblems to a pseudo-Boolean black-box optimization problem. Then we use relevant implementations of corresponding methods to analyze hard SAT instances encoding the cryptanalysis of state-of-the-art stream ciphers proposed during the recent e-STREAM competition.

Keywords


Black-box optimization, Pseudo-Boolean optimization, SAT, Divide-and-conquer, Cryptanalysis, Stream cipher


DOI
10.12783/dtcse/optim2018/27923

Full Text:

PDF

Refbacks

  • There are currently no refbacks.