#!/usr/bin/python3
# Copyright (c) 2016 Bart Massey

# Create SAT problem in DIMACS format
# http://www.satcompetition.org/2009/format-benchmarks2009.html
# to solve a Sudoku instance.

from sys import stdin

# Generate the index number of an atom.
def atom(r, c, v):
    return r * 9 * 9 + c * 9 + v + 1

# Keep a list of all the clauses.
clauses = []
def clause(c):
    clauses.append(c)

# Input the instance.
problem = [ l for l in stdin.readlines() if l and l[0] != '#' ]
for r in range(9):
    for c in range(9):
        if problem[r][c] != '.':
            v = ord(problem[r][c]) - ord('0')
            clause([atom(r, c, v - 1)])

# Every cell must have a value.
for r in range(9):
    for c in range(9):
        clause([atom(r, c, v) for v in range(9)])

# No cell may have two values.
for r in range(9):
    for c in range(9):
        for v1 in range(9):
            for v2 in range(9):
                if v1 == v2:
                    continue
                clause([-atom(r, c, v1), -atom(r, c, v2)])

# The same value may not occur twice in the same row.
for r in range(9):
    for c1 in range(9):
        for c2 in range(9):
            if c1 == c2:
                continue
            for v in range(9):
                clause([-atom(r, c1, v), -atom(r, c2, v)])

# The same value may not occur twice in the same column.
for c in range(9):
    for r1 in range(9):
        for r2 in range(9):
            if r1 == r2:
                continue
            for v in range(9):
                clause([-atom(r1, c, v), -atom(r2, c, v)])

# The same value may not occur twice in the same sub-board.
for r1 in range(9):
    for r2 in range(9):
        if r1 // 3 != r2 // 3:
            continue
        for c1 in range(9):
            for c2 in range(9):
                if c1 // 3 != c2 // 3:
                    continue
                if (r1, c1) == (r2, c2):
                    continue
                for v in range(9):
                    clause([-atom(r1, c1, v), -atom(r2, c2, v)])

# Emit the problem description.
print("c", "generated by sudokugen")
print("p", "cnf", 9*9*9, len(clauses))
for c in clauses:
    for l in c:
        print(l, "", end="")
    print("0")
