Телеграм канал «Математика не для всех»

Остаются два принципиальных условия. Каждая клетка прямоугольника должна быть покрыта хотя бы одним выбранным уголком. И ни одна клетка не должна быть покрыта дважды, то есть нельзя одновременно выбрать два уголка, которые перекрываются. Оба условия естественным образом записываются в виде булевых формул в конъюнктивной нормальной форме — именно в том виде, с которым SAT-солверы умеют работать особенно эффективно. После этого задача полностью готова. Мы передаём SAT-солверу набор логических ограничений и задаём единственный вопрос: существует ли присваивание переменных, при котором все они выполняются. Если ответ положительный, найденное присваивание буквально и есть корректное разрезание прямоугольника. Если отрицательный — никакого разрезания не существует в принципе, и это уже не эвристическое рассуждение, а строгий логический вывод. Именно поэтому пример с прямоугольником 5×9 так показателен. Для него не существует простого инварианта, который «на глаз» запрещал бы разрезание. Но SAT-солвер спокойно перебирает логическое пространство возможностей и находит допустимую конфигурацию. А если бы её не существовало, он столь же уверенно доказал бы невозможность. Самое удивительное в этом подходе — его универсальность. Мы не писали специальный алгоритм для разрезания уголками, не анализировали симметрии и не придумывали конструктивные трюки. Мы просто свели задачу к вопросу о логической выполнимости. Точно так же SAT-солверы применяются к судоку, расписаниям экзаменов, задачам упаковки, верификации программ и тысячам других задач, которые внешне выглядят совершенно по-разному.

Как SAT-солверы решают задачи про разрезания и почему прямоугольник 5×9 всё-таки режется на уголки На математических кружках для начинающих часто дают задачи, в которых нужно разрезать клетчатую фигуру на одинаковые маленькие кусочки. Классический пример — L-образный «уголок» из трёх клеток. Формулировка выглядит безобидно: можно ли разрезать данный прямоугольник на такие уголки без наложений и пропусков? Первое рассуждение почти всегда арифметическое. Каждый уголок состоит из трёх клеток, значит, общее число клеток обязано делиться на 3. Это необходимое условие сразу отсекает множество случаев. Например, прямоугольники вида 3×(2n+1) выглядят подозрительно, а 3×(2n), наоборот, легко режутся. Возникает ощущение, что картина ясна и будто бы число клеток должно делиться ещё и на 6. Однако эта интуиция быстро ломается. Прямоугольник 5×9 состоит из 45 клеток и тем не менее допускает разрезание на такие уголки. Простой арифметики оказывается недостаточно. Чтобы понять, почему так происходит, приходится либо искать хитрые конструктивные идеи, либо сменить сам способ мышления о задаче. Вместо того чтобы искать разрезание как геометрический объект, можно попытаться описать задачу в чисто логических терминах. Именно здесь появляется SAT-солвер — инструмент, который на первый взгляд кажется слишком простым для подобных задач, но на практике оказывается удивительно мощным. SAT-солвер — это программа, предназначенная для решения задачи булевой выполнимости. На вход ей подаётся логическая формула, составленная из булевых переменных и операций «и», «или» и «не». Вопрос, который решает SAT-солвер, формулируется предельно строго: существуют ли такие значения переменных, при которых вся формула становится истинной. Если такие значения существуют, формула выполнима; если нет — невыполнима. Простейший пример — формула вида «(x или y) и (x или не y)». Она выполнима, потому что при x = истина вся формула становится истинной независимо от значения y. SAT-солвер должен обнаружить этот факт и, как правило, вернуть не только ответ «выполнимо», но и конкретное присваивание переменных. С теоретической точки зрения SAT занимает центральное место в теории вычислительной сложности. Согласно теореме Кука — Левина, задача булевой выполнимости является NP-полной. Это означает, что в общем случае к ней можно свести любую задачу из класса NP и что не существует алгоритма, который гарантированно решал бы все SAT-задачи за полиномиальное время. В худшем случае сложность остаётся экспоненциальной, и этого принципиально нельзя избежать. Тем не менее, начиная с конца 1990-х и особенно в 2000-х годах, произошёл резкий скачок в практической эффективности SAT-решателей. Современные алгоритмы научились справляться с формулами, содержащими десятки и сотни тысяч переменных и миллионы ограничений. Это стало возможным благодаря развитию алгоритмов семейства DPLL, анализу конфликтов, обучению на противоречиях и множеству эвристик и оптимизаций. В результате SAT-солверы превратились в мощные инженерные инструменты, широко применяемые в верификации программ и аппаратуры, автоматизации проектирования электронных схем, анализе программ и задачах искусственного интеллекта. Как всё это связано с задачей про уголки? Связь возникает в тот момент, когда мы меняем постановку задачи. Мы больше не спрашиваем: «как именно разрезать прямоугольник». Вместо этого мы задаём вопрос: «существует ли разрезание вообще». Для этого мы перечисляем все возможные способы положить уголок внутри прямоугольника. Каждое допустимое положение становится отдельной булевой переменной. Истинность переменной означает, что соответствующий уголок выбран, ложность — что он не используется. После этого геометрия почти полностью исчезает, уступая место логике.

Ищу желающих заполнять карточки товаров на ВБ! Работа полностью на удаленке с зп до150 000 рублей в месяц. Без опыта, нужен только телефон, занятость 3-6 часов в день. Всему обучат на бесплатном курсе и после возьму на работу: ✅ 3 дня уроков по 30 минут ✅ Домашки с проверкой и оплатой бонусами ✅ Плачу 10 тыс за каждую выполненную домашку Все кто пройдет курс, получат сертификат от школы с образовательной лицензией. ⚡ Набор заканчивается завтра. 👍 Для регистрации жмите кнопку "Зарегистрироваться": Зарегистрироваться #реклама 16+ course.wildmanager.ru О рекламодателе

⚡️ На платформе "Сириус.Курсы" появился новый БЕСПЛАТНЫЙ онлайн-курс "Дополнительные главы стереометрии. 10-11 классы. v1.0". Для регистрации можно не указывать личные данные, нужна только почта. Курс для любителей геометрии, которые хотят погрузиться в новое измерение. На курсе нет однообразных вычислительных задач, зато много задач, для решения которых нужно сделать геометрическое наблюдение. В этом смысле курс стереометрии – продолжение курсов по планиметрии. Задач много – у большинства тем есть второй уровень, целиком состоящий из задач посложнее.

⚡️ 314 триллионов знаков π за 4.3 МВт⋅ч Компания StorageReview вновь вернула себе мировую корону в гонке за числом π, вычислив его сразу до 314 000 000 000 000 знаков. Рекорд был установлен не в облаке и не на распределённом кластере, а на одном коммерческом сервере. Запуск стартовал 31 июля 2025 года и завершился 18 ноября 2025 года, проработав 110 дней подряд без единой секунды простоя — что само по себе уже достижение уровня HPC. Для вычислений использовался сервер Dell PowerEdge R7725 форм-фактора 2U, оснащённый двумя процессорами AMD EPYC 9965 по 192 ядра каждый, то есть 384 ядра в сумме. В системе было установлено 1,5 ТБ DDR5 DRAM и 40 NVMe-накопителей Micron 6550 ION по 61,44 ТБ, что дало более 2,4 ПБ физического флеш-хранилища. Для работы y-cruncher было выделено 34 SSD, обеспечивших около 2,1 ПБ под временные данные, а ещё 6 SSD использовались в программном RAID10 для финальной записи результата. Само вычисление выполнялось с помощью y-cruncher v0.8.6.9545 на алгоритме Чудновского под Ubuntu 24.04 LTS Server. Чистое время расчёта числа π составило 8 793 223 секунды (примерно 101,8 дня), общее вычислительное время — 9 274 878 секунд, а полное «время по стене» от старта до финиша — 9 463 226 секунд. Самая крупная логическая контрольная точка достигала 850 538 385 064 992 цифр, а максимальное использование логического диска — 1 605 960 520 636 440 байт, то есть около 1,43 ПБ. Ключевым фактором рекорда стало хранилище. В конфигурации с 40 SSD платформа обеспечивала до 280 ГБ/с суммарной пропускной способности. По сравнению с предыдущим рекордом StorageReview на 202 трлн цифр, последовательная запись выросла с 47 до 107 ГиБ/с, последовательное чтение — с 56,7 до 127 ГиБ/с, а чтение с «перешагиванием порога» увеличилось сразу на 383 % — с 20,9 до 101 ГиБ/с. За время расчёта было прочитано около 148,4 ПиБ данных и записано 126,7 ПиБ, при этом износ SSD составил в среднем 7,3 ПБ на диск. Отдельного внимания заслуживает энергоэффективность. Средняя потребляемая мощность сервера составляла около 1600 Вт, а общее энергопотребление за весь 314-триллионный расчёт — всего 4304,7 кВт⋅ч. Это эквивалентно 13,7 кВт⋅ч на один триллион цифр π. Для сравнения, предыдущий рекорд на 300 трлн цифр, выполненный на большом кластере с общим хранилищем, оценивался примерно в 33 600 кВт⋅ч, что в 7–8 раз больше.

Топ-3 книги на новогодние каникулы! Хотя Кнут, конечно, самый крутой)