CODEWITHSUNDEEP
algorithm
xuhdev
xuhdev

Reputation: 9361

Reduce 0-1 knapsack prob. to a SAT prob

Is there any way to reduce the 0-1 knapsack problem to a SAT problem in Conjunctive Norm Form?

Upvotes: 0

Views: 1368

Answers (1)

mcdowella
mcdowella

Reputation: 19601

You could always work out the digital circuits necessary to implement adders and comparators and then turn the result of that into conjunctive normal form. You can get circuits into CNF form without expanding them exponentially by making up intermediate variables which represent the outputs of small sections of circuit.

Each node of a circuit amounts to a=f(b, c) where a is the output, b and c the input, and f is some simple function like & or |. You can create a CNF function that is true only when a really is the result of f(b, c) and it can't be too unwieldy, because it is a function on only three variables.

You can rewrite any circuit into a large number of terms of the form a=f(b, c) and all you have to do with the CNF versions of these is to AND them all together. Assuming you want to solve for the output being true, you then just stick on the output variable as the final component of that big AND.

Upvotes: 1

Related Questions