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?