Как постоянные входные данные влияют на постановку задачи SAT?

Question

Допустим, у меня есть схема черного ящика с N входами и 1 выходом.

Я хочу зафиксировать значение M входов и найти значение остальных входов (NM), для которых схема является удовлетворительной.Если я вручную исправлю вводы M в RTL Verilog и преобразую его в CNF (используя abc), это даст правильный результат?Правильный ли подход к такого рода проблемам?

Answer 1

Исходное пространство поиска вашей проблемы содержит 2^N записей.Путем фиксирования M входных данных пространство поиска уменьшается в 2^M раза и имеет 2^(N-M) записей.

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

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

Для учета фиксированных входных данных называется Boolean ConstraintРаспространение .Это в основном упрощает вашу схему, так как могут быть удалены все элементы, которые имеют предопределенный выход.Примеры: AND с одним или несколькими ложными входами имеет выход false .OR с одним или несколькими входами true имеет выход true и т. Д.Другие упрощения включают в себя удаление двойных отрицаний и инвертированных входных пар в ворота XOR/XNOR.

Вы могли бы взглянуть на bc2cnf , переводчик из логического формата списка соединений в усваиваемый SAT-решательФайл DIMACS / CNF .Аналогично ABC , bc2cnf будет распространять постоянные входы и выдавать довольно оптимизированный CNF .