Minisat рандомизировать выбор переменных не работает на Gcloud - PullRequest
0 голосов
/ 08 июня 2018

Я хочу получать разные решения каждый раз, когда запускаю minisat для одной и той же проблемы.Я могу сделать это с помощью параметра "rnd-seed" в minisat.Это просто рандомизирует выбор переменной, чтобы каждый раз я мог найти другое решение.Хотя этот параметр отлично работает на моей машине (Ubuntu16), он не работает на gcloud (Google Cloud), работающем на машине с Ubuntu.

Я думаю, что мне не хватает небольшой части, но я не могу понять, что это такое.

Примечание. Я не хочу передавать информацию о решении в минисат для получения другого решения.Мне действительно нужно рандомизировать выбор переменной.

Редактировать: Позвольте мне объяснить, почему мне нужно рандомизированное решение.Я решаю множество проблем SAT, и обычно эти проблемы SAT очень похожи друг на друга.Поэтому, если я не могу выбрать случайную переменную, я получаю в большинстве случаев очень похожие решения, которые мне не нужны.Поэтому на самом деле я не запускаю minisat для той же проблемы.

Edit-2: @sascha хотел, чтобы я объяснил, что я имею в виду под словами «работает» и «не работает».Когда я запускаю файл cnf на моем компьютере, каждый раз я получаю разные решения.Однако, когда я запускаю один и тот же файл cnf на компьютере gcloud, я всегда получаю одно и то же решение.

1 Ответ

0 голосов
/ 09 июня 2018

Опция -rnd-seed не рандомизирует выбор переменной ветви.Скорее, он позволяет вам задать начальное число для генератора псевдослучайных чисел, который использует Minisat.

Выбор переменной для ветвления не предполагает случайности, если не используется опция -rnd-freq.Передайте значение с плавающей запятой в диапазоне от 0 до 1. 0 означает отсутствие случайности, 1 означает попытку использовать случайную переменную в каждой ветви.Код делает только одну попытку случайного выбора переменной, предположительно потому, что поиск неустановленной переменной в произвольно большой очереди с приоритетами может стать довольно дорогим.Если эта попытка не удалась, Minisat разветвляется, используя обычную очередь с приоритетами.

...