  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.
