SAT Solvers и сохранение фазы

Question

Решатели DPLL SAT обычно применяют эвристику Phase Saving .Идея состоит в том, чтобы запомнить последнее присвоение каждой переменной и использовать его first в ветвлении.

Чтобы поэкспериментировать с эффектами ветвления полярности и сохранения фазы, я попробовал несколько SAT-решателей и изменил настройки фазы.Все это Windows 64-битные порты, работающие в однопоточном режиме.Я всегда использовал один и тот же пример ввода средней сложности (5619 переменных, 11261 предложений, в решении 4% всех переменных - true, 96% false).

Ниже приведены значения времени выполнения:

Это может быть просто (неудачей) удачей, но различия весьма заметныбольшой.Это особый сюрприз, что MiniSat превзошел все современные решатели для моего примера.

Мой вопрос:

ЕстьЕсть ли объяснения различий?
Лучшие практики для сохранения полярности и фазы?

Answer 1

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