History

The puzzle was introduced to Japan in 1980 by McKee Kaji, the founder of Nikoli, Japan's best-known publisher of puzzle books. During a visit to the United States, Kaji became frustrated that he didn't know enough English to complete any of the crossword puzzles he encountered in American magazines. He then spotted a lone digit puzzle called Cross Sums, which had been a minor pursuit in US puzzle magazines since the 1960s. Kaji enjoyed this "mathematical transliteration" of the crossword puzzle so much that he began designing his own version of it. Back in Japan, he published the new puzzle under the name "kasan kurosu" (the Japanese word for "addition" and the Japanese pronunciation of the English word "cross"), which was soon abbreviated to the catchier "kakro" or "kakuro". The puzzle quickly became an obsession among Japan's many puzzle enthusiasts, and has been incredibly popular there ever since.

Rules

Ka Kuro is best described as a kind of mathematical crossword. Similar to Su Doku, it is all about logical thinking, but it does require a small degree of mathematical reasoning as well. However, despite the need for basic addition, it is really a game of logic, not arithmetic.

A Ka Kuro grid looks very similar to a crossword grid, containing both blacked out and white cells. The blacked out cells divide the grid into "blocks", i.e. orthogonal lines of white cells. Some of the blacked out cells contain a diagonal line from top left to bottom right and a number in one or both halves. These numbers are called "clues". The number in the top right corner is called an "across clue" as it relates to the horizontal block of cells next to it, and the number in the bottom left corner is called a "down clue" as it relates to the vertical block of cells underneath it.

The object of the game is to fill in the empty cells, following three simple rules:

1. Each cell must contain a single digit from 1 to 9 inclusive.
2. The sum of the digits in each vertical or horizontal block must equal the clue at the top or on the left of that block.
3. Digits may only be used once in each block. (However, a digit may re-occur in the same row or column in a different block.)

Challenge

You are challenged to give a boolean encoding of the Ka Kuro puzzles above in order to find the solution or solutions -- you may first want to give a boolean encoding of numbers between 1 and 15 (assuming that the sum never exceeds 15)!!