As title says, what I am trying to do is to find a way to sum integers and later compare them with another integer W, in a manner that when the sum of integers is less or equal than W, using only CNF.

My best approach to the sum was to convert every integer in its binary form and use a XOR to perform the addition. However I'm not sure how to generate a carry.

About the comparison part, I was thinking to compare each bit starting from the one with higher significance and checking if the bit in W is zero and the bit in the sum is one, so it will mean that the sum is bigger than W, in other case, W is greater or equal than the sum.

  • $\begingroup$ I can't understand the problem statement. The first sentence is rather vague and I don't understand what that means. Some words seem missing and the sentence doesn't seem grammatical ("in manner that when..." - something seems missing from that clause; when the sum is <= W, what then?). We need a clear specification of the problem. If you are looking for an algorithm to do something, can you list what are the inputs to the algorithm, what are the outputs, and what is the precise requirement for an output to be considered correct? $\endgroup$
    – D.W.
    Commented Mar 8 at 6:27
  • $\begingroup$ That's easily doable mechanically with a couple of assumptions. First, you need to know the upper bound of integer value (how many bits it has). Next, you just add the values and compare. See this: blog.adamfurmanek.pl/2021/10/30/sat-part-1 and this blog.adamfurmanek.pl/2021/11/06/sat-part-2 Once you have that, you can do the comparison as in ILP blog.adamfurmanek.pl/2015/09/12/ilp-part-4 and this is how you reduce ILP to SAT blog.adamfurmanek.pl/2021/11/13/sat-part-3 $\endgroup$ Commented Mar 11 at 7:09
  • $\begingroup$ Continuing my comment above: this whole logic could be a little simplified. All you need to do is just add the numbers, then subtract $W$, and finally check the most significant bit to see if the result is negative. That's just an optimization which doesn't change the core logic of the approach. $\endgroup$ Commented Mar 11 at 7:14


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.