How are objective functions represented in SAT solvers?

95 views Asked by At

SAT solvers can be used to solve the traveling salesman problem, where the sum of costs between chosen edges is important. I understand that you then ask the solver to go again finding a lesser cost. How is that maximum represented in conjunctive normal form?

1

There are 1 answers

0
tphilipp On

The idea is to translate pseudo-Boolean constraints into CNF and many different encodings are available. A naive encoding is to enumerate all partial models that would result in a higher cost (which is exponential).

Note: I am co-author of the following publication: You may find the PBLib useful as it provides different encodings.