Википедия
SAT@home — российский проект добровольных вычислений на платформе BOINC , запущенный в сентябре 2011 года. Научной целью проекта является решение дискретных задач путём сведения их к задаче о выполнимости булевых формул (SAT, от — выполнимость) в конъюнктивной нормальной форме . Отыскание решения выбранной задачи производится с использованием одного из известных SAT-решателей, реализующего алгоритм DPLL . Проект поддерживается лабораторией Дискретного анализа и прикладной логики Института динамики систем и теории управления Сибирского отделения РАН и Центром распределённых вычислений Института проблем передачи информации . По состоянию на 19 сентября 2014 года в проекте приняли участие 18394 компьютеров 7239 пользователей из 124 стран, обеспечивая производительность порядка 3,1 тера флопс . Участвовать в проекте может любой желающий, обладающий компьютером с выходом в Интернет , установив на него программу BOINC .