Допустим, у вас есть логическая функция, которая принимает два числа (в двоичном формате) и возвращает значение true, если они равны шестнадцати:
01000 + 01000 = 10000
8 + 8 = 16 -> true
00110 + 01000 = 01110
6 + 8 = 14 -> false
В этом примере функция принимает десять входных данных, назовем их abcde + fghij.
Под капотом он напрямую моделируется логикой вентиля и использует два сумматора и несколько вентилей xnor для проверки эквивалентности двоичной строке 10000.
Затем мы передаем эту бинарную функцию логическому алгоритму выполнимости, чтобы найти набор входных данных, который дает истинный результат (например, первый пример выше).
Мой вопрос таков: найдет ли алгоритм SAT решение быстрее, если мы будем явно указывать наблюдаемые ограничения?
Что я имею в виду под «наблюдаемыми ограничениями»? Что ж, одним из наблюдаемых ограничений может быть «если какое-либо число больше 16, то не утруждайте себя выполнением сложения и возвращайте false».
Вы можете включить это ограничение следующим образом:
(a ^ ¬b ^ ¬c ^ ¬d ^ ¬e) ^ (f ^ ¬g ^ ¬h ^ ¬i ^ ¬j) ^ (функция, которая у вас была раньше)
Другим ограничением может быть «если одно число четное, а другое нечетное, то вернуть false».
((e ^ ¬j) v (¬e ^ j)) ^ (функция, которая у вас была раньше)
Эти логические функции эквивалентны по корректности, но в логике вентилей последняя была бы (вероятно) более эффективной. Является ли моделирование проблемы единственной заботой при переходе к SAT, или это помогает включить эти наблюдаемые ограничения?
Я понимаю, что это не лучший пример, но, надеюсь, он объясняет, о чем я спрашиваю.
заранее спасибо
