SAT@home
SAT@home is a volunteer computing project built on the BOINC platform, dedicated to solving hard combinatorial problems that can be reduced to instances of the Boolean satisfiability problem (SAT).[1] The project was launched on September 29, 2011 by the A.A. Matrosov Institute for System Dynamics and Control Theory of the Siberian Branch of the Russian Academy of Sciences (ISDCT SB RAS) in Irkutsk, jointly with the Institute for Information Transmission Problems of RAS (IITP RAS) in Moscow.[2] Rather than searching for extraterrestrial signals or folding proteins, SAT@home applies idle volunteer CPU time to combinatorics and cryptanalysis problems that are NP-complete in the general case, but whose specific hard instances can be decomposed and searched in parallel across thousands of computers.
History
SAT@home was developed using the BOINC middleware together with the SZTAKI Desktop Grid package, and was added to the official list of BOINC projects on February 7, 2012 with alpha status; its status was later upgraded to beta.[2] The project was conceived and led by Alexander Semenov, with Oleg Zaikin, Stepan Kochemazov, and Ilya Otpuschennikov as principal collaborators throughout its active years.[3] All three researchers are affiliated with ISDCT SB RAS in Irkutsk.[4]
By 2019, the project's own news feed had gone quiet, and its original portal at sat.isa.ru/pdsat/ shows no activity beyond 2014.[5] A successor site, SAT@home 2.0, later appeared at sat.isa.ru/sat2/, continuing the project's general aim of solving hard SAT instances through volunteer computing, though it is run separately from the original project instance documented here.[6]
Research
SAT-based cryptanalysis
A major research thread of SAT@home involved encoding the internal state-recovery problem of stream ciphers as a Boolean satisfiability instance and searching for a solution across the volunteer grid. Problems were translated into SAT form using an in-house tool called Transalg, and were decomposed into families of sub-problems using a Monte Carlo method-based partitioning technique before distribution to volunteers.[2]
The project's earliest and best-known cryptanalytic result targeted the A5/1 stream cipher used to encrypt over-the-air GSM voice traffic. Using a single known 114-bit keystream burst, SAT@home successfully completed ten inversion experiments against A5/1, with the first finishing on May 7, 2012.[7] The keystream-recovery problem was expressed as an instance of SAT over a search space that a brute-force approach would need roughly trials to exhaust, corresponding to A5/1's effective key length; the divide-and-conquer partitioning method let volunteer hosts search disjoint slices of this space in parallel.[7]
Later cryptanalytic campaigns on SAT@home addressed weakened variants of the Bivium generator,[2] and estimated the cryptographic resistance of ciphers in the Trivium family to SAT-based attack.[8] A separate line of work formalized the underlying combinatorial technique, describing an algorithm for finding good problem partitionings for hard SAT instances and applying it to the inversion of several cryptographic functions.[9]
Diagonal Latin squares
Alongside cryptanalysis, SAT@home was used to search for diagonal Latin squares of order 10 — an array, with , in which every symbol appears exactly once in each row, column, and on both main diagonals. Finding sets of mutually compatible diagonal Latin squares of this order is a long-standing hard combinatorial search problem, related to the unresolved question of how many mutually orthogonal Latin squares of order 10 can exist.[10]
Using SAT@home, the project's team reported new triples of diagonal Latin squares of order 10, encoding the search as a Boolean satisfiability problem and distributing candidate partitions to volunteers in the same way as the cryptanalysis experiments.[10][11][12] Later BOINC-based projects run by overlapping teams, including RakeSearch and ODLK, continued this line of diagonal Latin square research after SAT@home wound down.
Technology
SAT@home ran on standard BOINC server daemons (transitioner, feeder, scheduler, validator, and assimilator), combined with the SZTAKI Desktop Grid package used for work generation and result validation.[2] A dedicated work generator daemon decomposed each original SAT problem into subproblems according to a partitioning found by the project's Monte Carlo-based partitioning method, which was itself implemented as a parallel application run on ISDCT SB RAS computing clusters before being handed off to volunteers.[2] A follow-up architectural paper described extending this model into a hybrid grid that incorporated idle resources of computational clusters alongside ordinary BOINC volunteer hosts.[3]
Publications
The following publications, listed on the official BOINC "Publications by BOINC Projects" page under SAT@home, report results computed using the project.
Zaikin, Oleg.(2019})."SAT-Based Cryptanalysis: From Parallel Computing to Volunteer Computing".pp. 701–712.link.DOI: 10.1007/978-3-030-36592-9_57.
Zaikin, Oleg.(2017})."A Volunteer-Computing-Based Grid Architecture Incorporating Idle Resources of Computational Clusters".link.DOI: 10.1007/978-3-319-57099-0_89.
(2016).Algorithm for finding partitionings of hard variants of boolean satisfiability problem with application to inversion of some cryptographic functions. SpringerPlus. DOI: 10.1186/s40064-016-2187-4.
(2016).On the Construction of Triples of Diagonal Latin Squares of Order 10. Electronic Notes in Discrete Mathematics. DOI: 10.1016/j.endm.2016.09.053.
(2016).Estimations of cryptographic resistance of ciphers in the trivium family to sat-based cryptanalysis. Prikladnaya diskretnaya matematika. Prilozhenie. DOI: 10.17223/2226308X/9/19.
Zaikin, Oleg.(2016})."SAT-based search for systems of diagonal latin squares in volunteer computing project SAT@home".link.DOI: 10.1109/MIPRO.2016.7522152.
(2015).The search for systems of diagonal Latin squares using the SAT@home project. International Journal of Open Information Technologies.
(2015).Solving weakened cryptanalysis problems for the Bivium cipher in the volunteer computing project SAT@home. International Journal of Open Information Technologies.
See also
References
- ↑ Zaikin, Oleg.(2019})."SAT-Based Cryptanalysis: From Parallel Computing to Volunteer Computing".pp. 701–712.link.DOI: 10.1007/978-3-030-36592-9_57.
- ↑ 2.0 2.1 2.2 2.3 2.4 2.5 (2015).Solving weakened cryptanalysis problems for the Bivium cipher in the volunteer computing project SAT@home. International Journal of Open Information Technologies.
- ↑ 3.0 3.1 Zaikin, Oleg.(2017})."A Volunteer-Computing-Based Grid Architecture Incorporating Idle Resources of Computational Clusters".link.DOI: 10.1007/978-3-319-57099-0_89.
- ↑ (2017). "Fast Algorithm for Enumerating Diagonal Latin Squares of Small Order". arXiv: 1709.02599.
- ↑ SAT@home news archive. sat.isa.ru. Retrieved 2026-07-04.
- ↑ SAT@home 2.0. sat.isa.ru. Retrieved 2026-07-04.
- ↑ 7.0 7.1 (2013). "On estimating total time to solve SAT in distributed computing environments: Application to the SAT@home project". arXiv: 1308.0761.
- ↑ (2016).Estimations of cryptographic resistance of ciphers in the trivium family to sat-based cryptanalysis. Prikladnaya diskretnaya matematika. Prilozhenie. DOI: 10.17223/2226308X/9/19.
- ↑ (2016).Algorithm for finding partitionings of hard variants of boolean satisfiability problem with application to inversion of some cryptographic functions. SpringerPlus. DOI: 10.1186/s40064-016-2187-4.
- ↑ 10.0 10.1 (2016).On the Construction of Triples of Diagonal Latin Squares of Order 10. Electronic Notes in Discrete Mathematics. DOI: 10.1016/j.endm.2016.09.053.
- ↑ Zaikin, Oleg.(2016})."SAT-based search for systems of diagonal latin squares in volunteer computing project SAT@home".link.DOI: 10.1109/MIPRO.2016.7522152.
- ↑ (2015).The search for systems of diagonal Latin squares using the SAT@home project. International Journal of Open Information Technologies.