Операция выполнена!
Закрыть
Хабы: Алгоритмы, Программирование, Python, Игры и игровые консоли, Логические игры

Автор статьи Modern SAT solvers: fast, neat and underused утверждает, что SAT-солверы «преступно мало используются в нашей отрасли». [SAT — Boolean SATisfiability Solver, то есть солвер, способный находить присвоения, делающие истинными сложные булевы выражения. Более подробно я писал о них ранее.] Какое-то время назад я задался вопросом, почему: как получилось, что они настолько мощны, но ими никто не пользуется? Многие специалисты заявили, что причина в неудобстве кодирования SAT: они лучше предпочтут работать с инструментами, которые выполняют компиляцию в SAT.

Я вспомнил об этом, когда прочитал пост Райана Бергера о решении «задачи ферзей с LinkedIn» как задачи SAT.

Вкратце опишу задачу про ферзей (Queens). У нас есть сетка NxN, разделённая на N областей, и нам нужно разместить N ферзей так, чтобы в каждом столбце, строке и области находился ровно один. Ферзи могут находиться на одной диагонали, но не соседствовать по диагонали.

Читать далее
Читайте также
СТАТЬ АВТОРОМ
НОВОСТИ

ПИШИТЕ

Техническая поддержка проекта ВсеТут

info@vsetut.pro