Al Piskun: add IDGF logo and web archive link

2026-07-04T13:10:13Z

add IDGF logo and web archive link

← Older revision		Revision as of 13:10, 4 July 2026
Line 35:		Line 35:
	}}		}}

	'''SAT@home''' is a [[wikipedia:volunteer computing\|volunteer computing]] project built on the [[wikipedia:BOINC\|BOINC]] platform, dedicated to solving hard combinatorial problems that can be reduced to instances of the [[wikipedia:Boolean satisfiability problem\|Boolean satisfiability problem]] (SAT).<ref name="zaikin2019">{{Cite conference		'''[https://web.archive.org/web/20180829063323/http://sat.isa.ru/pdsat/ SAT@home]''' is a [[wikipedia:volunteer computing\|volunteer computing]] project built on the [[wikipedia:BOINC\|BOINC]] platform, dedicated to solving hard combinatorial problems that can be reduced to instances of the [[wikipedia:Boolean satisfiability problem\|Boolean satisfiability problem]] (SAT).<ref name="zaikin2019">{{Cite conference
	\|last1=Zaikin \|first1=Oleg		\|last1=Zaikin \|first1=Oleg
	\|title=SAT-Based Cryptanalysis: From Parallel Computing to Volunteer Computing		\|title=SAT-Based Cryptanalysis: From Parallel Computing to Volunteer Computing
Line 112:		Line 112:

	=== Diagonal Latin squares ===		=== Diagonal Latin squares ===
			[[File:Idgf.png\|left\|frameless]]
	[[File:Sudoku.jpg\|thumb\|right\|A completed [[wikipedia:Sudoku\|Sudoku]] grid is a special case of a Latin square. SAT@home volunteers searched for diagonal Latin squares of order 10, a much harder combinatorial target.]]		[[File:Sudoku.jpg\|thumb\|right\|A completed [[wikipedia:Sudoku\|Sudoku]] grid is a special case of a Latin square. SAT@home volunteers searched for diagonal Latin squares of order 10, a much harder combinatorial target.]]

Al Piskun: first light

2026-07-04T13:01:00Z

first light

New page

{{Infobox software
| name = SAT@home
| logo =SAT@home_logo.png
| logo caption =
| screenshot =
| caption =
| description = SAT@home is a completed Mathematics and Computer Science BOINC project that used volunteer computing to solve hard instances of the Boolean satisfiability problem, including SAT-based cryptanalysis of stream ciphers and searches for diagonal Latin squares, developed by researchers at ISDCT SB RAS and IITP RAS.
| status = Completed
| category = Mathematics
| compute = CPU
| dependencies = None
| developer = Alexander Semenov, Oleg Zaikin, Stepan Kochemazov
| author = Alexander Semenov
| sponsor = [[wikipedia:Russian Academy of Sciences|Russian Academy of Sciences]] (Siberian Branch)
| maintainer = SAT@home team, ISDCT SB RAS
| released = {{Start date and age|2011|09|29}}
| completed = {{Start date and age|2019|04|01}}
| discontinued =
| repository =
| programming language =
| operating system = Windows, Linux
| size =
| stats as of =
| average performance =
| active users =
| total users =
| active hosts =
| total hosts =
| rac =
| credit per day =
| gpu performance =
| cpu performance =
| website = {{URL|http://sat.isa.ru/pdsat/}}
| license =
}}

'''SAT@home''' is a [[wikipedia:volunteer computing|volunteer computing]] project built on the [[wikipedia:BOINC|BOINC]] platform, dedicated to solving hard combinatorial problems that can be reduced to instances of the [[wikipedia:Boolean satisfiability problem|Boolean satisfiability problem]] (SAT).<ref name="zaikin2019">{{Cite conference
|last1=Zaikin |first1=Oleg
|title=SAT-Based Cryptanalysis: From Parallel Computing to Volunteer Computing
|book-title=Supercomputing: 5th Russian Supercomputing Days (RuSCDays 2019)
|year=2019
|pages=701–712
|doi=10.1007/978-3-030-36592-9_57
|url=https://link.springer.com/chapter/10.1007/978-3-030-36592-9_57
}}</ref> The project was launched on September 29, 2011 by the [[wikipedia:Russian Academy of Sciences|A.A. Matrosov]] Institute for System Dynamics and Control Theory of the Siberian Branch of the Russian Academy of Sciences (ISDCT SB RAS) in [[wikipedia:Irkutsk|Irkutsk]], jointly with the [[wikipedia:Institute for Information Transmission Problems|Institute for Information Transmission Problems]] of RAS (IITP RAS) in [[wikipedia:Moscow|Moscow]].<ref name="bivium2015">{{Cite journal
|last1=Zaikin |first1=Oleg |last2=Semenov |first2=Alexander |last3=Otpuschennikov |first3=Ilya
|title=Solving weakened cryptanalysis problems for the Bivium cipher in the volunteer computing project SAT@home
|journal=International Journal of Open Information Technologies
|year=2015
|url=https://cyberleninka.ru/article/n/solving-weakened-cryptanalysis-problems-for-the-bivium-cipher-in-the-volunteer-computing-project-sat-home
}}</ref> Rather than searching for extraterrestrial signals or folding proteins, SAT@home applies idle volunteer CPU time to [[wikipedia:combinatorics|combinatorics]] and [[wikipedia:cryptanalysis|cryptanalysis]] problems that are [[wikipedia:NP-completeness|NP-complete]] in the general case, but whose specific hard instances can be decomposed and searched in parallel across thousands of computers.

[[File:Irkutsk's Akademgorodok - panoramio.jpg|thumb|right|The Akademgorodok district of Irkutsk, home to ISDCT SB RAS, the institute that launched and maintained SAT@home.]]

== 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.<ref name="bivium2015" /> The project was conceived and led by [[wikipedia:Alexander Semenov (mathematician)|Alexander Semenov]], with Oleg Zaikin, Stepan Kochemazov, and Ilya Otpuschennikov as principal collaborators throughout its active years.<ref name="grid2017">{{Cite conference
|last1=Zaikin |first1=Oleg |last2=Manzyuk |first2=Maxim |last3=Kochemazov |first3=Stepan |last4=Bychkov |first4=Igor |last5=Semenov |first5=Alexander
|title=A Volunteer-Computing-Based Grid Architecture Incorporating Idle Resources of Computational Clusters
|year=2017
|doi=10.1007/978-3-319-57099-0_89
|url=https://link.springer.com/chapter/10.1007/978-3-319-57099-0_89
}}</ref> All three researchers are affiliated with ISDCT SB RAS in Irkutsk.<ref>{{Cite arxiv
|last1=Kochemazov |first1=Stepan |last2=Vatutin |first2=Eduard |last3=Zaikin |first3=Oleg
|title=Fast Algorithm for Enumerating Diagonal Latin Squares of Small Order
|year=2017
|eprint=1709.02599
|url=https://arxiv.org/pdf/1709.02599
}}</ref>

By 2019, the project's own news feed had gone quiet, and its original portal at <code>sat.isa.ru/pdsat/</code> shows no activity beyond 2014.<ref>{{Cite web
|url=http://sat.isa.ru/pdsat/
|title=SAT@home news archive
|website=sat.isa.ru
|access-date=2026-07-04
}}</ref> A successor site, '''SAT@home 2.0''', later appeared at <code>sat.isa.ru/sat2/</code>, 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.<ref>{{Cite web
|url=https://sat.isa.ru/sat2/
|title=SAT@home 2.0
|website=sat.isa.ru
|access-date=2026-07-04
}}</ref>

== Research ==

=== SAT-based cryptanalysis ===
A major research thread of SAT@home involved encoding the internal state-recovery problem of [[wikipedia:stream cipher|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 [[wikipedia:Monte Carlo method|Monte Carlo method]]-based partitioning technique before distribution to volunteers.<ref name="bivium2015" />

[[File:Поточный шифр.PNG|thumb|left|A generic stream-cipher diagram. SAT@home's cryptanalysis experiments targeted keystream generators such as [[wikipedia:A5/1|A5/1]], Bivium, and the Trivium cipher family.]]

The project's earliest and best-known cryptanalytic result targeted the '''[[wikipedia:A5/1|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.<ref name="estimating">{{Cite arxiv
|last1=Semenov |first1=Alexander |last2=Zaikin |first2=Oleg
|title=On estimating total time to solve SAT in distributed computing environments: Application to the SAT@home project
|year=2013
|eprint=1308.0761
|url=https://arxiv.org/pdf/1308.0761
}}</ref> The keystream-recovery problem was expressed as an instance of SAT over a search space that a brute-force approach would need roughly <math>2^{64}</math> 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.<ref name="estimating" />

Later cryptanalytic campaigns on SAT@home addressed weakened variants of the '''Bivium''' generator,<ref name="bivium2015" /> and estimated the cryptographic resistance of ciphers in the '''Trivium''' family to SAT-based attack.<ref name="trivium2016">{{Cite journal
|last1=Zaikin |first1=O.S. |last2=Otpuschennikov |first2=I.V. |last3=Semenov |first3=A.A.
|title=Estimations of cryptographic resistance of ciphers in the trivium family to sat-based cryptanalysis
|journal=Prikladnaya diskretnaya matematika. Prilozhenie
|year=2016
|doi=10.17223/2226308X/9/19
|url=http://journals.tsu.ru//pdm2/&journal_page=archive&id=1451&article_id=30028
}}</ref> 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.<ref name="partitionings">{{Cite journal
|last1=Semenov |first1=Alexander |last2=Zaikin |first2=Oleg
|title=Algorithm for finding partitionings of hard variants of boolean satisfiability problem with application to inversion of some cryptographic functions
|journal=SpringerPlus
|year=2016
|doi=10.1186/s40064-016-2187-4
|url=http://springerplus.springeropen.com/articles/10.1186/s40064-016-2187-4
}}</ref>

=== Diagonal Latin squares ===
[[File:Sudoku.jpg|thumb|right|A completed [[wikipedia:Sudoku|Sudoku]] grid is a special case of a Latin square. SAT@home volunteers searched for diagonal Latin squares of order 10, a much harder combinatorial target.]]

Alongside cryptanalysis, SAT@home was used to search for '''diagonal [[wikipedia:Latin square|Latin squares]]''' of order 10 — an <math>n \times n</math> array, with <math>n = 10</math>, 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.<ref name="dls2016">{{Cite journal
|last1=Zaikin |first1=Oleg |last2=Zhuravlev |first2=Alexey |last3=Kochemazov |first3=Stepan |last4=Vatutin |first4=Eduard
|title=On the Construction of Triples of Diagonal Latin Squares of Order 10
|journal=Electronic Notes in Discrete Mathematics
|year=2016
|doi=10.1016/j.endm.2016.09.053
|url=https://linkinghub.elsevier.com/retrieve/pii/S1571065316301470
}}</ref>

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.<ref name="dls2016" /><ref name="miprodls">{{Cite conference
|last1=Zaikin |first1=Oleg |last2=Kochemazov |first2=Stepan |last3=Semenov |first3=Alexander
|title=SAT-based search for systems of diagonal latin squares in volunteer computing project SAT@home
|book-title=2016 39th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO)
|year=2016
|doi=10.1109/MIPRO.2016.7522152
|url=http://ieeexplore.ieee.org/document/7522152/
}}</ref><ref name="injoit2015">{{Cite journal
|last1=Zaikin |first1=Oleg |last2=Kochemazov |first2=Stepan
|title=The search for systems of diagonal Latin squares using the SAT@home project
|journal=International Journal of Open Information Technologies
|year=2015
|url=https://cyberleninka.ru/article/n/the-search-for-systems-of-diagonal-latin-squares-using-the-sat-home-project
}}</ref> 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.<ref name="bivium2015" /> 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.<ref name="bivium2015" /> 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.<ref name="grid2017" />

== Publications ==
The following publications, listed on the official [https://boinc.berkeley.edu/pubs.php#SAT@home BOINC "Publications by BOINC Projects" page] under SAT@home, report results computed using the project.

{{Cite conference
|last1=Zaikin |first1=Oleg
|title=SAT-Based Cryptanalysis: From Parallel Computing to Volunteer Computing
|book-title=Supercomputing: 5th Russian Supercomputing Days (RuSCDays 2019)
|year=2019
|pages=701–712
|doi=10.1007/978-3-030-36592-9_57
|url=https://link.springer.com/chapter/10.1007/978-3-030-36592-9_57
}}

{{Cite conference
|last1=Zaikin |first1=Oleg |last2=Manzyuk |first2=Maxim |last3=Kochemazov |first3=Stepan |last4=Bychkov |first4=Igor |last5=Semenov |first5=Alexander
|title=A Volunteer-Computing-Based Grid Architecture Incorporating Idle Resources of Computational Clusters
|year=2017
|doi=10.1007/978-3-319-57099-0_89
|url=https://link.springer.com/chapter/10.1007/978-3-319-57099-0_89
}}

{{Cite journal
|last1=Semenov |first1=Alexander |last2=Zaikin |first2=Oleg
|title=Algorithm for finding partitionings of hard variants of boolean satisfiability problem with application to inversion of some cryptographic functions
|journal=SpringerPlus
|year=2016
|doi=10.1186/s40064-016-2187-4
|url=http://springerplus.springeropen.com/articles/10.1186/s40064-016-2187-4
}}

{{Cite journal
|last1=Zaikin |first1=Oleg |last2=Zhuravlev |first2=Alexey |last3=Kochemazov |first3=Stepan |last4=Vatutin |first4=Eduard
|title=On the Construction of Triples of Diagonal Latin Squares of Order 10
|journal=Electronic Notes in Discrete Mathematics
|year=2016
|doi=10.1016/j.endm.2016.09.053
|url=https://linkinghub.elsevier.com/retrieve/pii/S1571065316301470
}}

{{Cite journal
|last1=Zaikin |first1=O.S. |last2=Otpuschennikov |first2=I.V. |last3=Semenov |first3=A.A.
|title=Estimations of cryptographic resistance of ciphers in the trivium family to sat-based cryptanalysis
|journal=Prikladnaya diskretnaya matematika. Prilozhenie
|year=2016
|doi=10.17223/2226308X/9/19
|url=http://journals.tsu.ru//pdm2/&journal_page=archive&id=1451&article_id=30028
}}

{{Cite conference
|last1=Zaikin |first1=Oleg |last2=Kochemazov |first2=Stepan |last3=Semenov |first3=Alexander
|title=SAT-based search for systems of diagonal latin squares in volunteer computing project SAT@home
|book-title=2016 39th International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO)
|year=2016
|doi=10.1109/MIPRO.2016.7522152
|url=http://ieeexplore.ieee.org/document/7522152/
}}

{{Cite journal
|last1=Zaikin |first1=Oleg |last2=Kochemazov |first2=Stepan
|title=The search for systems of diagonal Latin squares using the SAT@home project
|journal=International Journal of Open Information Technologies
|year=2015
|url=https://cyberleninka.ru/article/n/the-search-for-systems-of-diagonal-latin-squares-using-the-sat-home-project
}}

{{Cite journal
|last1=Zaikin |first1=Oleg |last2=Semenov |first2=Alexander |last3=Otpuschennikov |first3=Ilya
|title=Solving weakened cryptanalysis problems for the Bivium cipher in the volunteer computing project SAT@home
|journal=International Journal of Open Information Technologies
|year=2015
|url=https://cyberleninka.ru/article/n/solving-weakened-cryptanalysis-problems-for-the-bivium-cipher-in-the-volunteer-computing-project-sat-home
}}

== See also ==
* [[BOINC Central]]
* [[SZTAKI Desktop Grid]]
* [[RakeSearch]]
* [[ODLK]]
* [[ODLK1]]
* [[World Community Grid]]

== References ==
{{Reflist}}

[[Category:BOINC projects]]
[[Category:Completed BOINC projects]]
[[Category:Mathematics]]

SAT@home - Revision history

Al Piskun: add IDGF logo and web archive link

Al Piskun: first light