CODEWITHSUNDEEP
constraint-programmingsatsat-solvers
lava_07
lava_07

Reputation: 93

Atleast K out of N encoding in SAT solvers

I know that given an at most k out of N tool I can get an at least K out of N by changing it to at most (n-k) out of N.

But I can't seem to wrap my head around how this is true. I might be missing something very trivial

For example, if K=2 and N=6 how is at least 2 out of 6 equivalent to at most 4 out of 6

any help would be appreciated

Upvotes: 1

Views: 744

Answers (2)

Thibault Joan
Thibault Joan

Reputation: 21

a bit late to the party but your idea was right, the problem was in you formulation.

When you say "at most k out of N" you must be specific about the "at most" (resp. "at least")

to be more specific let us define four operators:

  • count_le_k : count strictly lower than k
  • count_leq_k : count lower or equal to k
  • count_geq_k : count greater or equal to k
  • count_ge_k : count greater lower than k

Assuming you have at least one of them, you can retrieve the others. I'll assume you have count_le_k

# L is a list of literals
# k is a positive integer
# returns a list of clauses encoding a DIMACS CNF such that
# count(sigma, L) <= k
def count_leq_k(L, k):
  return count_le_k(L, k+1)

# count(sigma, L) >= k
#   = count(sigma, not L) < len(L) - k
def count_geq_k(L, k):
  return count_leq_k((-x for x in L), len(L) - k)

# count(sigma, L) > k
def count_ge_k(L, k):
  return count_geq_k(L, k+1)

As a bonus, you can easily write the count_equal_k as follows:

def count_eq_k(L, k):
  return count_geq_k(L, k) + count_leq_k(L, k)

Finally, for completeness, here is the count_le_k function:

import itertools

# count(sigma, L) < k
def count_le_k(lits, k):
  assert(1 <= k)
  negs = [-x for x in lits]
  return list(itertools.combinations(negs, k))

Upvotes: 1

alias
alias

Reputation: 30428

As you put it, the equivalence just isn't true. So, don't feel bad about not understanding it. To see, let's take an example. Let's say we have booleans only, N=6 and K=2, and the assignment:

True False False False False False

to these 6 variables. The statement At most 2 out of 6 are True is obviously satisfied by this assignment, but At least 4 out of 6 are True is not.

Maybe what you meant is:

at least K out of N is True

is equivalent to

at most N-K out of N is False

which can be further generalized to say:

at least K out of N objects have property P

is equivalent to:

at most N-K out of N objects do not have the property P

Is this what you were trying to express? Hope that's more clear!

Upvotes: 2

Related Questions