Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

214 lines (204 sloc) 5.46 kb
// Solve a sudoku with ZDDs.
#include <stdint.h>
#include <stdlib.h>
#include <stdio.h>
#include "inta.h"
#include "zdd.h"
#include <stdarg.h>
#include "io.h"
// Construct ZDD of sets containing exactly 1 digit at forall boxes
// (r, c), starting at pool entry d.
//
// The ZDD begins:
// 1 ... 2
// 1 --- 10
// 2 ... 3
// 2 --- 10
// ...
// 9 ... F
// 9 --- 10
//
// and repeats every 10 levels:
// 10 ... 11
// 10 --- 19
// and so on until 729 --- F, 729 ... T.
//
// This ZDD has 9^81 members.
void global_one_digit_per_box() {
zdd_push();
int next = 9;
uint32_t n = zdd_next_node();
for(int i = 1; i <= 729; i++) {
zdd_add_node(i, (i % 9) ? 1 : 0, -1);
if (next < 729) {
zdd_set_hi(zdd_last_node(), n + next);
}
if (!(i % 9)) next += 9;
}
}
// Construct ZDD of sets containing exactly 1 occurrence of digit d in row r.
// For instance, if d = 3, r = 0:
//
// 1 === 2 === 3
// 3 ... 4a, --- 4b
// 4a === 5a === ... === 9a === ... === 11a === 12
// 4b === 5b === ... === 9b === ... === 11b === 13b
// 12 ... 13a, --- 13b
// 13a === ... === 20a === 21
// 13b === ... === 20b === 22b
// and so on until:
// 74a === 75 ... F, --- 76
// 74b === 76
// 76 === ... === 729 === T
//
// This ZDD has 9*2^720 members.
// When intersected with the one-digit-per-box set, the result has
// 9*8^8*9^72 members. (Pick 1 of 9 positions ford, leaving 8 possible choices
// forthe remaining 8 boxes in that row. The other 81 - 9 boxes can contain
// any single digitS.)
// The intersection forall d and a fixed r has 9!*9^72 members.
// The intersection forall r and a fixed d has 9^9*8^72 members.
void unique_digit_per_row(int d, int r) {
zdd_push();
// The order is determined by sorting by number, then by letter.
int next = 81 * r + d; // The next node involving the digit d.
int v = 1;
int state = 0;
while (v <= 729) {
if (v == next) {
next += 9;
state++;
if (state == 1) {
// The first split in the ZDD.
zdd_add_node(v, 1, 2);
} else if (state < 9) {
// Fix previous node. We must not have a second occurrence of d.
uint32_t n = zdd_last_node();
zdd_set_hilo(n, n + 3);
// If this is the first occurrence of d, we're on notice.
zdd_add_node(v, 1, 2);
} else {
// If we never saw d, then branch to FALSE.
// Otherwise reunite the branches.
zdd_add_node(v, 0, 1);
next = -1;
}
} else if (state == 0 || state == 9) {
zdd_add_node(v, 1, 1);
} else {
zdd_add_node(v, 2, 2);
zdd_add_node(v, 2, 2);
}
v++;
}
// Fix last nodes.
uint32_t n = zdd_last_node();
if (zdd_lo(n - 1) > n) zdd_set_lo(n - 1, 1);
if (zdd_hi(n - 1) > n) zdd_set_hi(n - 1, 1);
if (zdd_lo(n) > n) zdd_set_lo(n, 1);
if (zdd_hi(n) > n) zdd_set_hi(n, 1);
}
// Construct ZDD of sets containing all elements in the given list.
// The list is terminated by -1.
void contains_all(int *list) {
zdd_push();
int v = 1;
int *next = list;
while (v <= 729) {
if (v == *next) {
next++;
zdd_add_node(v, 0, 1);
} else {
zdd_add_node(v, 1, 1);
}
v++;
}
// Fix 729.
uint32_t n = zdd_last_node();
if (zdd_lo(n) > n) zdd_set_lo(n, 1);
if (zdd_hi(n) > n) zdd_set_hi(n, 1);
}
void unique_digit_per_col(int d, int col) {
int list[9];
for(int i = 0; i < 9; i++) {
list[i] = 81 * i + 9 * col + d;
}
zdd_contains_exactly_1(list, 9);
}
void unique_digit_per_3x3(int d, int row, int col) {
int list[9];
for(int i = 0; i < 3; i++) {
for(int j = 0; j < 3; j++) {
list[i * 3 + j] = 81 * (i + 3 * row) + 9 * (j + 3 * col) + d;
}
}
zdd_contains_exactly_1(list, 9);
}
int main() {
zdd_init();
// The universe is {1, ..., 9^3 = 729}.
zdd_set_vmax(729);
// Number rows and columns from 0. Digits are integers [1..9].
// The digit d at (r, c) is represented by element 81 r + 9 c + d.
inta_t list;
inta_init(list);
for(int i = 0; i < 9; i++) {
for(int j = 0; j < 9; j++) {
int c = getchar();
if (EOF == c) die("unexpected EOF");
if ('\n' == c) die("unexpected newline");
if (c >= '1' && c <= '9') {
inta_append(list, 81 * i + 9 * j + c - '0');
}
}
int c = getchar();
if (EOF == c) die("unexpected EOF");
if ('\n' != c) die("expected newline");
}
inta_append(list, -1);
contains_all(inta_raw(list));
inta_clear(list);
global_one_digit_per_box();
zdd_intersection();
// Number of ways you can put nine 1s into a sudoku is
// 9*6*3*6*3*4*2*2.
printf("rows\n");
fflush(stdout);
for(int i = 1; i <= 9; i++) {
for(int r = 0; r < 9; r++) {
unique_digit_per_row(i, r);
if (r) zdd_intersection();
}
zdd_intersection();
}
for(int i = 1; i <= 9; i++) {
for(int c = 0; c < 3; c++) {
for(int r = 0; r < 3; r++) {
printf("3x3 %d: %d, %d\n", i, r, c);
fflush(stdout);
unique_digit_per_3x3(i, r, c);
if (r) zdd_intersection();
}
if (c) zdd_intersection();
}
zdd_intersection();
}
for(int i = 1; i <= 9; i++) {
for(int c = 0; c < 9; c++) {
printf("cols %d: %d\n", i, c);
fflush(stdout);
unique_digit_per_col(i, c);
if (c) zdd_intersection();
}
zdd_intersection();
}
void printsol(int *v, int vcount) {
for(int i = 0; i < vcount; i++) {
putchar(((v[i] - 1) % 9) + '1');
if (8 == (i % 9)) putchar('\n');
}
putchar('\n');
}
zdd_forall(printsol);
return 0;
}
Jump to Line
Something went wrong with that request. Please try again.