Как целевые функции представлены в решателях SAT?

Question

Решатели SAT могут использоваться для решения задачи коммивояжера, когда важна сумма затрат между выбранными ребрами. Я понимаю, что вы затем просите решающую программу go снова найти меньшую стоимость. Как этот максимум представлен в соединительной нормальной форме?

Answer 1

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

Примечание: я соавтор следующей публикации: вы можете найти PBLib полезно, поскольку предоставляет различные кодировки.