CODEWITHSUNDEEP
satcnfconjunctive-normal-form
joeforker
joeforker

Reputation: 41817

How are objective functions represented in SAT solvers?

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?

Upvotes: 0

Views: 139

Answers (1)

tphilipp
tphilipp

Reputation: 466

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.

Upvotes: 1

Related Questions