Sum of unique integers to cnf constraint

Question

As a study project I try to solve the kakuro puzzle problem using SAT SOLVER. I can't really find an efficient way to convert the sum of k unique integers (1...9) to a CNF constraint. What I had in mind:

for a group of k cells (1,...k) and a sum of j:

    find all subsets with size of k from P({1,2,...9})
    correctSubSets <- filter out all subsets that SUM(subset)!= sum
    AllVars <- EMPTY_SET
    for i in 1...k:
       add to current cnf a union of correctSubSets s.t each prefixed with i
       add to AllVars a union of correctSubSets s.t each prefixed with i
       for each pair in AllVars:
              if pair represents two different cells ix,jy:
                  if there is no sum s.t x,y part of it:
                     add to cnf (-ix, -jy) (not ix or not jy)




example for sum = 5 and k=2:
AllVars={11, 24, 13, 22, 12, 23, 14, 21}
cnf = (11, 13, 12, 14), (21, 22, 23, 24), (-11, -22), (-11, -21), (-11, -23), (-12, -21), (-12,-22), (-12,-24) ....... and more and more

I fill like this is very though to implement and not efficient at all. how to solve it correctly?

Answer 1

Here's a strategy for solving Kakuro with a SAT solver.

1. Make a nine variables for each cell, each variable indicating whether that cell contains $1$, $2$, etc.

2. Add a exactly-one-out-nine constraint for the variables of each cell. You can do this naively in 37 clauses by adding a clause that at least one of the nine must be true ($x_1 \vee x_2 \vee \dots \vee x_9$) and 36 clauses that no pair of them may be true at the same time ($(\neg x_1 \vee \neg x_2) \wedge (\neg x_1 \vee \neg x_3) \wedge \dots \wedge (\neg x_8 \vee \neg x_9)$).

3. For each row/column in the puzzle add an at-most-one-out-of-k constraint in the manner above for all the variables encoding ones, twos, threes, etc in that row or column to ensure each row/column uses unique numbers.

4. For each row/column make a new set of variables $q_1, q_2, \dots $ that encode "contains $1$, contains $2$, etc". As an example, if a row contains cells $a, b, c, d$ then "contains $2$" would be $(\neg q_2 \vee a_2 \vee b_2 \vee c_2 \vee d_2)$ and $(q_2 \vee \neg a_2) \wedge \dots \wedge (q_2 \vee \neg d_2)$.

5. Now for each row/column, take the target sum and find all partitions using unique parts smaller than or equal to nine of it, excluding order, using exactly the right amount of parts that fit in the row/column. This may sound like a lot, but this is at worst 11 unique partitions for digits 1-9. Then for each partition introduce a new variable $p$. Suppose our target is $14$ and our partition is $14 = 8 + 3 +2 +1$. Then we add clauses $p \vee q_9 \vee \neg q_8 \vee q_7 \vee q_6 \vee q_5 \vee q_4 \vee \neg q_3 \vee \neg q_2 \vee \neg q_1$ and $(\neg p \vee \neg q_9) \wedge (\neg p \vee q_8) \wedge (\neg p \vee \neg q_7) \wedge (\neg p \vee \neg q_6) \wedge (\neg p \vee \neg q_5) \wedge\\(\neg p \vee \neg q_4) \wedge (\neg p \vee q_3) \wedge (\neg p \vee q_2) \wedge (\neg p \vee q_1)$

   You get the idea. The variable $p$ is now an indicator variable for the combination $q_8, q_3, q_2, q_1$ being true. It may not be necessary to also include the negated terms for $q_9, q_7, q_6, q_5, q_4$, but it may speed up (or slow down) the SAT solver. Experiment with it.

6. Finally for all partitions variables $p_k$ of a row/column add a single clause $p_1 \vee p_2 \vee \dots \vee p_k$ indicating at least one of the partitions must hold.