On estimating total time to solve SAT in distributed computing environments: Application to the SAT@home project
This work addresses the challenge of predicting computational effort for SAT-based problems in distributed settings, which is incremental as it builds on existing partitioning and estimation techniques.
The paper tackles the problem of estimating total solving time for SAT problems in distributed computing environments, proposing a method based on Monte Carlo estimation and optimal partitioning search, and applies it to logical cryptanalysis of A5/1 and Bivium ciphers, solving 10 previously unsolved A5/1 problems in the SAT@home project.
This paper proposes a method to estimate the total time required to solve SAT in distributed environments via partitioning approach. It is based on the observation that for some simple forms of problem partitioning one can use the Monte Carlo approach to estimate the time required to solve an original problem. The method proposed is based on an algorithm for searching for partitioning with an optimal solving time estimation. We applied this method to estimate the time required to perform logical cryptanalysis of the widely known stream ciphers A5/1 and Bivium. The paper also describes a volunteer computing project SAT@home aimed at solving hard combinatorial problems reduced to SAT. In this project during several months there were solved 10 problems of logical cryptanalysis of the A5/1 cipher thatcould not be solved using known rainbow tables.