Somme d'entiers uniques à la contrainte CNF

Question

En tant que projet d'étude, j'essaie de résoudre le kakuro Problème de puzzle en utilisant le solveur SAT. Je ne trouve pas vraiment un moyen efficace de convertir la somme de K entiers uniques (1 ... 9) en une contrainte CNF. Ce que j'avais en tête:

Pour un groupe de cellules K (1, ... k) et une somme de 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

Je remplit comme ceci est tout à fait implémenté et non efficace du tout. Comment le résoudre correctement?