Satisfy K out of N constraints in Z3Py

Question

I have a program with logic as described in the pseudocode below. x is a string, and x[k] will return the decimal charcode of character at index k. The ^ operator returns the decimal XOR result of the operands.

x = input
int checksum = x[0] ^ x[1] ^ x[2]
int sum = 0

sum += x[36] ^ x[23] == 111
sum += x[23] ^ x[29] == 101
sum += x[29] ^ x[30] == 116
sum += x[30] ^ x[9] == 115
sum += x[9] ^ x[25] == 0

return sum == checksum and x[0] ^ x[29] == 100 and x[1] ^ x[30] == 200

I want to find input that makes this program return true. If I want to solve this problem in Z3Py, is there a way for me to do it? I need some K out of N constraint that allows me to express the constraints as expressions, but I haven't found support for this.

Psedocode for what I would like to do with Z3:

int checksum = x[0] ^ x[1] ^ x[2]

bools = []

bools.append(Bool(x[36] ^ x[23] == 111))
bools.append(Bool(x[23] ^ x[29] == 101))
bools.append(Bool(x[29] ^ x[30] == 116))
bools.append(Bool(x[30] ^ x[9] == 115))
bools.append(Bool(x[9] ^ x[25] == 0))

state.add(bools[0])
state.add(bools[1])
state.add(bools[2])
state.add(bools[3])
state.add(bools[4])
state.add(x[0] ^ x[29] == 100)
state.add(x[1] ^ x[30] == 200)

state.add(PbEq([boolean for boolean in bools], checksum))

alias alias · Accepted Answer · 2019-10-21T15:37:43

Reading your problem description, I don't see why you need K-out-of-N constraints for this problem. It seems like a straightforward encoding using bit-vector theory. But perhaps I didn't quite understand the problem you're trying to solve. It'd help to show what you tried, and what failed.

In any case, if you really need K-out-of-N constraints, then Z3 has special support for them in various forms:

Such constraints are known as "Pseudo-boolean," and hence the Pb prefix.

Satisfy K out of N constraints in Z3Py

1 Answers