Lock-free структуры данных в Rust

Но ведь DashMap под капотом шардирует и на каждый шард использует RwLock, разве нет?

Решение японских кроссвордов с помощью SAT солвера

Я добавил в свой солвер опцию для использования SAT-солвера, некоторые кроссворды стали решаться в сотни раз быстрее, чем с моим на коленке написанным бэктрэкингом. На основе идей из этой статьи вот такой получился код, если кому-то еще интересно. В ближайшее время планирую дополнить алгоритм генерации дизъюнктов и для цветных кроссвордов тоже.

Решение цветных японских кроссвордов со скоростью света

Переписал свой питоновский солвер на Rust, он решает все 252 задачи за 1.76 секунд (в таблице правда написано 2.10, но там первый успешный результат указан).

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Половину этих подходов я пытался выяснить, почему выдает 'Wrong Answer' и при этом не дает никаких подсказок, что же пошло не так. Оказалось, что никакие другие символы, кроме '.' и '#' нельзя писать, иначе задача сразу считается проваленной. А у меня для неопределенных (нерешенных) клеток раньше выводил символ '?'.

Вторая половина запусков — это да, здесь я пытался поменять стратегию бэктрэкинга так, чтобы без таймаута все решить.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

поменял стратегию выбора кандидата для бэктрэкинга и все тесты удалось решить

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Попробовал загнать туда минимальный пример — получил таймаут. Возможно там билдится без оптимизаций, поэтому получается медленный debug-код.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Написал в личке, чтобы не спойлерить для других желающих порешать

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Круто, что нашелся автор одного из самых быстрых солверов!

По пунктам 1 и 2: я для стратегии выбора лучшего кандидата изучал это исследование и на моем солвере лучший результат показала стратегия Sqrt (см. раздел V. EXPERIMENTS).

Пункт 3 — это что-то новенькое, надо будет у себя попробовать сделать.

Пункт 4 очень похож на стратегию «срезания» ветвей дерева поиска, называемую «backjumping». У меня были планы по ее реализации, но руки пока не дошли.

Спасибо за подробное описание идей.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Запустил #22336 на машине послабее — через 26 часов нашлось два решения (94020 сек). Все же получилось значительно меньше года. Конечно ваш солвер решает ту же задачу меньше чем за 2 минуты и это очень круто.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Это дело конечно хорошее, только там Rust 1.14.0 используется, где куча сахара еще не введена и, например, у итераторов значительно меньше методов. Но для спортивного интереса думаю можно попробовать переделать под Rust образца 2016.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Все этапы решения — параметрические по типу блока (BinaryBlock или ColoredBlock). То есть все функции имеют примерно такую сигнатуру fn solve<B: Block>(...);. Алгоритмы ничего не знают, о том что они решают, потенциально можно добавить еще какую-нибудь пару типов impl Block for SomeOtherBlock; impl Color for SomeOtherColor помимо имеющихся сейчас BinaryColor + BinaryBlock; MultiColor + ColoredBlock, которые будут задавать еще какую-то схему взаимодействия между отдельными числовыми блоками и клетками нонограмм и все алгоритмы должны без проблем эту схему подхватить. Короче говоря, черно-белые — это не частный случай цветных, а совершенно отдельная схема.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

У меня написано «умеет решать», а вы трактуете как «может решить». Вы ведь не станете говорить, что шахматист, который проигрывает партию другому «не умеет играть», он скорее «не смог победить». А вот те солверы, которые не умеют решать цветные — они как шахматисты, которые в принципе не умеют играть в го. Иначе говоря, несмотря на то что, глаголы «решать» и «решить» похожи — это все таки разные глаголы. Первый — о процессе, второй — о результате.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

«решать» != «находить решения». Речь здесь о принципиальной возможности, а не о конечном результате. Например большинство солверов не умеют решать цветные кроссворды. Хотя формально вы правы — я не добавил поддержку blotted-кроссвордов, хотя в Python-солвере она была.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Никогда не слышал о них до этого, но на первый взгляд кажется, что с ними попроще должно быть.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

Да, из всего сайта webpbn.com 6 черно-белых не решаются до конца и еще больше цветных.

Решение японских кроссвордов c P̶y̶t̶h̶o̶̶n̶ Rust и WebAssembly

За час не решилась, остановлено по таймауту — это то, что обозначено '+' в оригинальной таблице-сравнении. Для графиков я просто подставил значение 10000 секунд, чтобы не с бесконечностью оперировать.

Решение японских кроссвордов с помощью SAT солвера

Я вот только не знаю, есть ли нонограммы, у которых логически есть только одно решение, но формально подходит несколько раскрасок.

Насколько я понял под «логически» вы понимаете метод решения line-by-line, в котором не используются методы вида «закрасим вот эту произвольную клетку и посмотрим, что будет дальше». С этой точки зрения все паззлы можно разделить на два больших класса: те, которые решаются итеративным применением построчных алгоритмов (логические) и все остальные.

Так вот первая группа паззлов всегда имеет не более одного решения (то, к которому и можно прийти «логически»). С точки зрения солвера сложных паззлов (второй группы) нет никакого разделения между «правильным» и «подходящим» решениями — они все правильные. Другой вопрос в том, что составитель паззла, скорее всего, имел ввиду одно из решений.

Думаю некорректно будет противопоставлять «логику» и «перебор»: cамый популярный метод решения паззлов второй группы — это бэктрекинг, который представляет собой очень даже логичный перебор. Например, указанный вами пример «Зима» — хоть и второго типа, но имеет единственное правильное решение и оно достигается путем единственного логического предположения: «предположим, что клетка (10, 18) — пустая», которое приводит к противоречию. Закрашиваем (10,18) и дальше все решается так же — просто построчно.

Решение японских кроссвордов с помощью SAT солвера

Не нужно никакой внешней валидации. Вся валидация решения сводится к тому, чтобы из найденного решения сгенерировать описания строк и столбцов (это тривиальная операция) и сравнить их с начальными описаниями.

Решение японских кроссвордов с помощью SAT солвера

В статье webpbn.com/survey автор пишет о 'Solving vs. Validation':

A program to do puzzle validation has a bit of a tougher job than a simple solver. A solver can stop after finding one solution. A validator must try to find a second. In the case of a puzzle that only has one solution, it must completely explore the solution space, eliminating every possible alternative solution.

Далее он сравнивает в основном солверы, которые могут находить более одного решения.

In the run-time tests performed for this survey, I always ask the solvers to find two solutions, unless the solver doesn't support that option.

Как я понял по вашему описанию, сейчас бенчмарки замеряют режим «найти первое возможное решение и выйти». Для корректного сравнения с другими солверами возможно правильнее все же сравнивать в режиме «найти как минимум два решения».

Решение цветных японских кроссвордов со скоростью света

Делал недавно похожее на Python, в основном использовал паззлы с webpbn.com. Интересно было бы сравнить скорость с вашей версией на одинаковых задачах.