Разное.

Apr 03, 2015 18:56

Я тут собрал на коленке решатель задач булевской выполнимости (SAT, boolean satisfiability). Отличие от обычных решателей в том, что он позволяет запускать параллельно множество тесно взаимодействующих тупых решателей (совсем тупых), ну, и обработка конфликтов в нём отличается от обычных SAT решателей (нет отката, например).

Он показывает интересные результаты.

Например, на задачах факторизации, что я собрал на коленке же (через ToughSAT generator), увеличение количества параллельных решателей приводит к интересному эффекту. Чем больше решателей, тем меньше любому из них надо сделать шагов (распространение констант или присваивание), чтобы хотя бы один из них нашёл решение. Процесс выходит на асимптоту, что разумно предполагать, но эта асимптота находится в области 3..4*количество_шагов_идеального_оракула. Например, для задачи факторизации произведения 4194287x4194301 при количестве параллельных решателей 8000 штук, количество шагов до решения равно 145. Уменьшаем/увеличиваем количество решателей на 1000, количество шагов увеличивается/уменьшается на, примерно, 13-15.

Само собой, это дело уже параллельное - распараллелить программу на Хаскеле это раз плюнуть. Параллельный запуск чуть меняет результаты выполнения (в подробности вдаваться не буду), но количество шагов не меняется. Увеличение количества ядер практически пропорционально увеличивает производительность.

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

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

Поэтому вопрос - как мне запустить мою программу, скомпилированную под Ubuntu, на, допустим, вычислительном узле Amazon? Надо ли мне ставить VirtualBox и образ Fedora, поддерживаемый Амазоном, или как-то можно поставить Убунту на амазоновский узел? И тому подобное.

Не поделитесь ли опытом и ссылками по теме?

Если интересна сама тема решателей и есть желание погонять, то тоже пишите. Исходники не дам (по ряду причин), а бинарник могу. Могу и Cloud Haskell вариант сделать, чтобы на разных машинах гонять, это тоже просто.

PS
Писать программу на Хаскеле, будучи жутко невыспавшимся, можно. Продукт моего творчества писался в метро и в выходные (и вечерами), месяцев четыре-пять, занимает ~1200 строк кода.

sat, вопрос, Хаскель

Previous post Next post
Up