Somma di numeri interi unici al vincolo CNF

Question

Come progetto di studio provo a risolvere il Kakuro Problema del puzzle usando SAT Solver. Non riesco davvero a trovare un modo efficiente per convertire la somma degli interi unici K (1 ... 9) in un vincolo CNF. Quello che avevo in mente:

Per un gruppo di celle K (1, ... k) e una somma di 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

Mi riempi così, però, è molto da implementare e per niente efficiente. Come risolverlo correttamente?