Equality by Exact Cover

We'll restrict ourselves to so come from the set . Written in binary it contains all 3-bit numbers: .

If we create one column per bit, we can represent the assignment as since only the least significant bit is set. The columns still need to be covered.

Now we need to encode in a way that covers these missing columns. The bitwise inverse is , covering exactly .

So far, both and would be encoded as a row with no way to recover the variable name from the output of DLX.

Similarly would be encoded as a row already covering all columns, with no need to include encoded as the empty row into the solution.

To avoid these issues, we can add a column covered by all assignments to and a column covered by all assignments to . Now is encoded as and is encoded as .

As a quick check we can set up the rows for and by hand and verify that the solver finds one solution.

<<init_problem>>

s = Solver()
p = Problem({"va", "vb", "c0", "c1", "c2"})
p.add_row(["va", "c0"])
p.add_row(["vb", "c1", "c2"])

print(s.solve(p))

{'1:': [{'vb', 'c2', 'c1'}, {'c0', 'va'}]}

For larger sets of input numbers, we'll want to automate the encoding and decoding of rows.

Inverting a k-bit binary number is equivalent to subtracting it from , a number where the lowest bits a all 1.

For example , so the inverse of is .

def invert(val: int, n_bits: int) -> int:
    full = (2**n_bits) - 1
    return full - val

To encode an assignment of var = val , we invert val if var is "b", then read bits one by one to determine which columns are covered.

def encode_row(var: str, val: int, n_bits: int):
    if var == "b":
        val = invert(val, n_bits)

    res = {f"v{var}"}
    for i in range(n_bits):
        if val & 1 == 1:
            res.add(f"c{i}")
        val //= 2
    return res

When decoding, we add the powers of two corresponding to the covered columns and invert again val if var is "b".

def decode_row(row: set[str], n_bits: int) -> tuple[str, int]:
    var = None
    val = 0

    for col in row:
        if col[0] == "v":
            var = col[1:]
        elif col[0] == "c":
            val += 2**int(col[1:])

    assert var in ("a", "b")
    if var == "b":
        val = invert(val, n_bits)
    return (var, val)

To decode a solution, we decode rows one by one and collect the values assigned to each variable (here just "a" and "b").

def decode_solution(solution: Solution, n_bits: int):
    res = {}
    for row in solution:
        var, val = decode_row(row, n_bits)
        if var in res:
            raise KeyError("Duplicate assignment")
        res[var] = val
    return res

Finally we can connect everything and verify that the solutions to are in fact , , …, .

<<init_problem>>
<<invert>>
<<encode>>
<<decode>>
<<decode-solution>>

s = Solver()
p = Problem({"va", "vb", "c0", "c1", "c2"})

n_bits = 3
for i in range(2**n_bits):
    p.add_row(encode_row("a", i, n_bits))
    p.add_row(encode_row("b", i, n_bits))

solutions = s.solve(p)

for solution in solutions.values():
    print(decode_solution(solution, n_bits))

{'b': 3, 'a': 3}
{'a': 6, 'b': 6}
{'b': 0, 'a': 0}
{'a': 7, 'b': 7}
{'b': 1, 'a': 1}
{'a': 4, 'b': 4}
{'b': 2, 'a': 2}
{'a': 5, 'b': 5}