Конвертирование задачи с поиском max/min в SAT?

Question

[floppa322]

Можно ли преобразовать комбинаторную задачу с поиском максимума/минимума в SAT?

Например, для задачи поиска максимального пути в графе или хроматического числа графа, ну или, например, замощение N фигурками разной формы и разного веса доски mxn, так, чтобы каждая клетка доски была покрыта фигуркой и суммарный вес фигурок был максимальным