January 12, 2013 4:30 pm

Nonconsecutive sudoku

 

Non-consecutive Sudoku puzzles look like your ordinary Sudokus. However, there is one extra rule: two consecutive numbers MUST NOT be placed next to each other (horizontally or vertically).

 

Example of the input and solution

 

Input file format

000|000|400
000|000|060
000|460|000
---+---+---
000|000|006
060|000|040
004|000|000
---+---+---
000|604|000
600|000|000
040|000|000

 

python-constraint solution

http://labix.org/python-constraint

Easy to use tool for constraint processing. Variable definition and many types of constraints. Implements backtracking and recursive backtracking. Quite slow though.

nonc-sudoku6.py: 

"""

Nonconsecutive sudoku solved by python-constrain library using its recursive backtracking solver

Based on:
http://code.activestate.com/recipes/491275/

"""
from itertools import islice
from sys import stdin
import constraint
from constraint import FunctionConstraint, BacktrackingSolver, RecursiveBacktrackingSolver, MinConflictsSolver

def make_problem(blocks=9, block_size=3, possible_values=range(1, 10), recursive=True):
	indices = list(range(i*blocks, i*blocks+blocks) for i in xrange(blocks))
	
	solver=None
	
	if (recursive):
		solver = RecursiveBacktrackingSolver()
	else:
		solver = BacktrackingSolver()
	
	problem = constraint.Problem(solver)
	
	def nonconsecutives(a,b):
		# used as parameter for creating FunctionConstraint-s to ensure nonconsecutivness
		return (abs(a - b) > 1)			

	def ensure_unique_values(varnames):
		# we don't want variable names to interfere with values,
		# so we convert them to strings
		problem.addConstraint(constraint.AllDifferentConstraint(), map(str, varnames))

	for vars in indices:
		problem.addVariables(map(str, vars), possible_values)
		# ensure all values are unique per row
		ensure_unique_values(vars)

	for vars in zip(*indices):
		# ensure all values are unique per column
		ensure_unique_values(vars)

	def block_indices(n):
		(x, y) = divmod(n, block_size)
		x *= block_size
		y *= block_size
		g_indices = list()
		for i in xrange(block_size):
			g_indices.extend(indices[x+i][y:y+block_size])
		return g_indices

	for i in xrange(blocks):
		# ensure all values are unique per block
		ensure_unique_values(block_indices(i))

	# for nonconsecutiveness
	for i in xrange(0,81):

    	# if there is any variable above
		if ((i - 9) >= 0):
			# we can add nonconsecutive constraint by using nonconsecutives function as FunctionContraint for current variable and variable above
			problem.addConstraint(FunctionConstraint(nonconsecutives), [str(i), str(i - 9)])
    			
		# if we are not at the start of the row
		if (i != 0) & (i != 9) & (i != 18) & (i != 27) & (i != 36) & (i != 45) & (i != 54) & (i != 63) & (i != 72):
			# we can add nonconsecutive constraint by using nonconsecutives function as FunctionContraint for current variable and variable to the left
			problem.addConstraint(FunctionConstraint(nonconsecutives), [str(i), str(i - 1)])
    		
	return problem

class Unsolvable(Exception):
	pass

def solve(matrix, problem=None):
    if problem is None:
        problem = make_problem()
    for (varn, val) in enumerate(sum(matrix, [])):
    
    	# if there is a number in input we have to put it as new constraint "==" 
        if val is not None:
            problem.addConstraint(lambda var, val=val: var==int(val), variables=(str(varn),))

    soln = problem.getSolution()
    if soln is None:
        raise Unsolvable()

    # soln is a dictionary of indices to values
    values = (v for (k, v) in sorted(soln.iteritems(), key=lambda (k, v): int(k)))
    cols = len(matrix)

    while True:
        row = list(islice(values, cols))
        if not row:
            break
        yield row

def read_input():
    values=[]
    for line in stdin:
        l=[]
        for char in line:
            if char not in ['-','+','|','\n']:
               if char!='0':
                  l.append(char)
               else:
                  l.append(None)
        if len(l)!=0:
           values.append(l)
    return values

def print_solution(a):
    chars = list()
    for r in range(1, 10):
      for c in range(1, 10):
        if c in (4, 7):
          chars.append("|")
        chars.append(a[(r-1)*9+(c-1)])
      if r != 9:
        chars.append("\n")
        if r in (3, 6):
          chars.append("---+---+---\n")
    print("".join(chars))

if __name__ == '__main__':
    out=[]
    for r in solve(read_input()):
       for v in r:
          out.append(str(v))
    print_solution(out)

Usage:  python nonc-sudoku6.py < [input file]

 

 

Recursive brute-force algorithm

Not so efficient obviously..

nonc-sudoku5.py: 

"""

Recursive brute-force method to solve nonconsecutive sudoku

"""

import sys

def read_input():
  values=''
  for line in sys.stdin:
    for char in line:
      if char not in ['-','+','|','\n']: values+=char
  return values

def print_solution(a):
  chars = list()
  for r in range(1, 10):
    for c in range(1, 10):
      if c in (4, 7):
        chars.append("|")
      chars.append(a[(r-1)*9+(c-1)]+' ')
    if r != 9:
      chars.append("\n")
      if r in (3, 6):
        chars.append("------+------+-----\n")
  print("".join(chars))

# testing if i and j are in same row
def same_row(i,j): return (i/9 == j/9)

# testing if i and j are in same column
def same_col(i,j): return (i-j) % 9 == 0

# testing if i and j are in same block
def same_block(i,j): return (i/27 == j/27 and i%9/3 == j%9/3)

# testing if a and b values are consecutives or not
def nonconsecutives(a,b):
  return (abs(int(a) - int(b)) > 1)
  
# main function called recursively
def r(a):
  i = a.find('0')
  if i == -1:
    print_solution(a)
    sys.exit(0)

  excluded_numbers = set()
  for j in range(81):
    if same_row(i,j) or same_col(i,j) or same_block(i,j):
         excluded_numbers.add(a[j])

  for m in '123456789':
    if m not in excluded_numbers:
   
      nonconsecutive_up = False
      nonconsecutive_left = False
      
      if (i != 0) & (i != 9) & (i != 18) & (i != 27) & (i != 36) & (i != 45) & (i != 54) & (i != 63) & (i != 72):
         nonconsecutive_left = nonconsecutives(m,a[i - 1])
      else:
         nonconsecutive_left = True
         
      if ((i - 9) >= 0):
         nonconsecutive_up  = nonconsecutives(m,a[i - 9])
      else:
         nonconsecutive_up = True
         
      if (nonconsecutive_left & nonconsecutive_up):
         r(a[:i]+m+a[i+1:])

if __name__ == '__main__':
  r(read_input())

Usage:  python nonc-sudoku5.py < [input file]

 

 

SMT generation for CVC4 solver

SMT is format for SMT-LIB (The Satisfiability Modulo Theories Library): http://www.smtlib.org/

Popis formátu: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf

CVC4 solver: http://cvc4.cs.nyu.edu/web/

 

nonc-sudoku-smt-gen.py: 

""""

Nonconsecutive sudoku SMT file generator

Based on:
https://gist.github.com/3904180

"""

from sys import stdin

def select(list):
    return ' '.join('(select a {0})'.format(l) for l in list)
    
def flatten(l):
    for el in l:
        if isinstance(el, collections.Iterable) and not isinstance(el, basestring):
            for sub in flatten(el):
                yield sub
        else:
            yield el
            
def make_flat(l):
    res = []
    iters_stack = [iter(l)]
    while iters_stack:
        for e in iters_stack[-1]:
            if isinstance(e, (tuple,list)):
                iters_stack.append(iter(e))
                break
            res.append(e)
        else:
            iters_stack.pop()
    return res
    
def generate(model):
    lines = []
    lines.append('(set-logic AUFLIRA)')
    lines.append('(set-option :produce-models true)')
    lines.append('(declare-fun a () (Array Int Int))')
    
    index =[[0]*9 for i in range(9)]
    
    n=0
    for i in range(9):
    	for j in range(9):
    		index[i][j]=n
    		n+=1

    for i in xrange(9):

    	lines.append('(assert (distinct {}))'.format(select(index[:][i])))
    	lines.append('(assert (distinct {}))'.format(select(index[i][:])))

        r0 = (i % 3) * 3
        c0 = (i // 3) * 3
   
        (x, y) = divmod(i, 3)
        x *= 3
        y *= 3
        blok = list()
        for j in xrange(3):
            blok.extend(index[x+j][y:y+3])
            
        lines.append('(assert (distinct {}))'.format(select(blok)))

    for i in xrange(0,81):
        if ((i - 9) >= 0):
            lines.append('(assert (not (= (select a {0}) (select a {1}))))'.format(i-9,i))
            lines.append('(assert (not (= (+ (select a {0}) 1) (select a {1}))))'.format(i-9,i))
            lines.append('(assert (not (= (- (select a {0}) 1) (select a {1}))))'.format(i-9,i))	
        if (i != 0) & (i != 9) & (i != 18) & (i != 27) & (i != 36) & (i != 45) & (i != 54) & (i != 63) & (i != 72):
            lines.append('(assert (not (= (select a {0}) (select a {1}))))'.format(i-1,i))
            lines.append('(assert (not (= (+ (select a {0}) 1) (select a {1}))))'.format(i-1,i))
            lines.append('(assert (not (= (- (select a {0}) 1) (select a {1}))))'.format(i-1,i))

    for i in xrange(81):
        lines.append('(assert (< 0 (select a {0})))'.format(i))
        lines.append('(assert (> 10 (select a {0})))'.format(i))

    for i, n in zip(xrange(81), model):
        if n != '0':
            lines.append('(assert (= {0} (select a {1})))'.format(n, i))

    lines.append('(check-sat)')
    lines.append('(get-value ({}))'.format(select(xrange(81))))

    return lines
    
def read_input():
  values=''
  for line in stdin:
    for char in line:
      if char not in ['-','+','|','\n']: values+=char
  return values
  
if __name__ == '__main__':
  print('\n'.join(generate(read_input())))
  print('\n')

nonc-sudoku-ans-out.py: 

"""

Script to parse output from CVC4 solver


"""

import sys

resultLine = "";

for line in sys.stdin:
	if line.startswith("sat"):
		continue
	resultLine = line
	break

results = resultLine.split(") (")

sudoku =[[0]*9 for i in range(9)]

i=0
j=0
n=0
for result in results:
	r=0
	if n<80:
		r=result.split(") ")[1]
	else:
		r=result.split(") ")[1].split("))")[0]
	sudoku[j][i]=r
	i+=1
	n+=1
	if (n % 9==0):
		j+=1
		i=0
		
print("")
chars = list()
for r in range(0, 9):
	for c in range(0, 9):
		if c in (3, 6):
			chars.append("|")
		chars.append(sudoku[r][c]+' ')
	if r != 9:
		chars.append("\n")
		if r in (2, 5):
			chars.append("------+------+-----\n")
print("".join(chars))

run.sh: 

#!/bin/bash
python nonc-sudoku-smt-gen.py < $1 > sudoku-problem.smt
./cvc4-1.0-x86_64-linux-opt --lang smt sudoku-problem.smt > sudoku-problem.ans
python nonc-sudoku-ans-out.py < sudoku-problem.ans > out.txt

Usage: ./run.sh [input file]

 

 

PyEDA

http://pyeda.readthedocs.org/en/latest/
Tool for hardware circuits design but can be used for other problems with constraints.

nonc-sudoku3.py: 

"""

Nonconsecutive sudoku solving by generating cnf for pyeda

Based on "Abusing PyEDA to Solve Sudoku":
http://pyeda.readthedocs.org/en/latest/sudoku.html

"""

from pyeda import *
from sys import stdin

DIGITS = "123456789"

X = bitvec("x", (1, 10), (1, 10), (1, 10))

V = And(*[
        And(*[
            OneHot(*[ X[r][c][v]
                for v in range(1, 10) ])
            for c in range(1, 10) ])
        for r in range(1, 10) ])

R = And(*[
        And(*[
            OneHot(*[ X[r][c][v]
                for c in range(1, 10) ])
            for v in range(1, 10) ])
        for r in range(1, 10) ])

C = And(*[
        And(*[
            OneHot(*[ X[r][c][v]
                for r in range(1, 10) ])
            for v in range(1, 10) ])
        for c in range(1, 10) ])

B = And(*[
        And(*[
            OneHot(*[ X[3*br+r][3*bc+c][v]
                for r in range(1, 4) for c in range(1, 4) ])
            for v in range(1, 10) ])
        for br in range(3) for bc in range(3) ])

N = And(*[
        And(*[ 
            And( Or( Not(Equal(X[r][c][1],1)), Not(Equal(X[r-1][c][2],1)) ), Or( Not(Equal(X[r][c][1],1)), Not(Equal(X[r][c-1][2],1))) ) if v == 1 else (
        	And( Or( Not(Equal(X[r][c][9],1)), Not(Equal(X[r-1][c][8],1)) ), Or( Not(Equal(X[r][c][9],1)), Not(Equal(X[r][c-1][8],1))) ) if v == 9 else 
                And( And( Or( Not(Equal(X[r][c][v],1)), Not(Equal(X[r-1][c][v+1],1)) ), Or( Not(Equal(X[r][c][v],1)), Not(Equal(X[r-1][c][v-1],1)) ) ),     
                    Or(Not(Equal(X[r][c][v],1)),Not(Equal(X[r][c-1][v+1],1))),Or(Not(Equal(X[r][c][v],1)),Not(Equal(X[r][c-1][v-1],1))))) 
                        for r in range(2, 10)
                    for c in range(2, 10)])
                for v in range(1, 10) ])
"""
Same as N=... above but very slow:

N=True
for r in range(2, 10):
    for c in range(2, 10):
        for v in range(1, 10):
            if v == 1:
                N=And(N,And(Or(Not(Equal(X[r][c][1],1)),Not(Equal(X[r-1][c][2],1)))))
                N=And(N,And(Or(Not(Equal(X[r][c][1],1)),Not(Equal(X[r][c-1][2],1)))))
    	    elif v == 9:
                N=And(N,And(Or(Not(Equal(X[r][c][9],1)),Not(Equal(X[r-1][c][8],1)))))
                N=And(N,And(Or(Not(Equal(X[r][c][9],1)),Not(Equal(X[r][c-1][8],1)))))
            else:
                N=And(N,And(Or(Not(Equal(X[r][c][v],1)),Not(Equal(X[r-1][c][v+1],1))),Or(Not(Equal(X[r][c][v],1)),Not(Equal(X[r-1][c][v-1],1)))))
                N=And(N,And(Or(Not(Equal(X[r][c][v],1)),Not(Equal(X[r][c-1][v+1],1))),Or(Not(Equal(X[r][c][v],1)),Not(Equal(X[r][c-1][v-1],1)))))
"""


S = CNF_And(V, R, C, B, N)

def parse_grid(grid):
    chars = [c for c in grid if c in DIGITS or c in "0"]
    assert len(chars) == 9 ** 2
    I = And(*[ X[i // 9 + 1][i % 9 + 1][int(c)]
               for i, c in enumerate(chars) if c in DIGITS ])
    return expr2cnf(I)

def get_val(point, r, c):
    for v in range(1, 10):
        if point[X[r][c][v]]:
            return DIGITS[v-1]
    return "X"

def print_output(point):
    chars = list()
    for r in range(1, 10):
        for c in range(1, 10):
            if c in (4, 7):
                chars.append("|")
            chars.append(get_val(point, r, c))
        if r != 9:
            chars.append("\n")
            if r in (3, 6):
                chars.append("---+---+---\n")
    print("".join(chars))

def solve(grid):
    I = parse_grid(grid)
    cnf = I * S
    return cnf.satisfy_one()
    
def read_input():
    values=''
    for line in stdin:
        for char in line:
            if char not in ['-','+','|','\n']: values+=char
    return values
    
if __name__ == '__main__':
    print_output(solve(read_input()))

Usage:  python nonc-sudoku3.py < [input file]

 

 

CNF generation for Minisat solver

Mapping of the CNF in python is very memory and computationally complex, better soliution is generate CNG to text file first and then solve it by Minisat solver.
For classic sudoku, input file has 8842 lines, after adding constraints of nonconsecutive sudoku it’s 10890

nonc-sudoku-cnf-gen.py: 

"""

Nonconsecutive sudoku solving by generating cnf file for Minisat solver

Based on: 
http://www.cybergarage.org/twiki/bin/view/Main/SatStudy

"""
from sys import stdin

print "p cnf 0 0"

sudokuProblem =[[0]*9 for i in range(9)]

i,j,n=[0,0,0]
for line in stdin:
	for char in line:
		if char not in ['-','+','|','\n']:
			if (n==9 or n==18 or n==27 or n==36 or n==45 or n==54 or n==63 or n==72):
				j+=1
				i=0
			sudokuProblem[j][i]=int(char)
			n+=1
			i+=1

for i in range(9):
	for j in range(9):
		x = sudokuProblem[i][j]
		if x != 0:
			print str(i+1) + str(j+1) + str(x) + " 0"

for i in range(9):
	for j in range(9):
		for x in range(9):
			print str(i+1) + str(j+1) + str(x+1) + " ",
		print "0"

for i in range(9):
	for x in range(9):
		for j in range(9-1):
			for n in range((j+1),9):
				print "-" +  str(i+1) + str(j+1) + str(x+1) + " " + "-" + str(i+1) + str(n+1) + str(x+1) + " 0"

for j in range(9):
	for x in range(9):
		for i  in range(9-1):
			for n in range((i+1),9):
				print "-" +  str(i+1) + str(j+1) + str(x+1) + " " + "-" + str(n+1) + str(j+1) + str(x+1) + " 0"

for x in range(9):
	for n in range(3):
		for k in range(3):
			massList = []
			for i in [0+(n*3),1+(n*3),2+(n*3)]:
				for j in [0+(k*3),1+(k*3),2+(k*3)]:
					massNum = str(i+1) + str(j+1) + str(x+1)
					massList.append(massNum)
			for i in range(9):
				for j in range((i+1),9):
					print "-" +  massList[i] + " " + "-" + massList[j] + " 0"

for r in range(2, 10):
    for c in range(2, 10):
        for v in range(1, 10):
            if v == 1:
                print "-" + str(r) + str(c) + "1" + " " + "-" + str(r-1) + str(c) + "2" + " 0"
                print "-" + str(r) + str(c) + "1" + " " + "-" + str(r) + str(c-1) + "2" + " 0"
    	    else:
                if v == 9:
                    print "-" + str(r) + str(c) + "9" + " " + "-" + str(r-1) + str(c) + "8" + " 0"
                    print "-" + str(r) + str(c) + "9" + " " + "-" + str(r) + str(c-1) + "8" + " 0"
                else:
                    print "-" + str(r) + str(c) + str(v) + " " + "-" + str(r-1) + str(c) + str(v+1) + " 0"
                    print "-" + str(r) + str(c) + str(v) + " " + "-" + str(r-1) + str(c) + str(v-1) + " 0"
                    print "-" + str(r) + str(c) + str(v) + " " + "-" + str(r) + str(c-1) + str(v+1) + " 0"
                    print "-" + str(r) + str(c) + str(v) + " " + "-" + str(r) + str(c-1) + str(v-1) + " 0"

nonc-sudoku-ans-out.py: 

"""

Script to parse output from MiniSat solver


"""

import sys

resultLine = "";

for line in sys.stdin:
	if line.startswith("SAT"):
		continue
	resultLine = line
	break

results = resultLine.split(" ")

sudoku =[[0]*9 for i in range(9)]
i=0
j=0
n=0
for result in results:
	x = int(result)
	if x < 0 or x < 100:
		continue
	sudoku[j][i]=result[2]
	i+=1
	n+=1
	if (n % 9==0):
		j+=1
		i=0
		
print("")
chars = list()
for r in range(0, 9):
	for c in range(0, 9):
		if c in (3, 6):
			chars.append("|")
		chars.append(sudoku[r][c]+' ')
	if r != 9:
		chars.append("\n")
		if r in (2, 5):
			chars.append("------+------+-----\n")
print("".join(chars))

run.sh: 

#!/bin/bash
python nonc-sudoku-cnf-gen.py < $1 > sudoku-problem.cnf
./MiniSat_v1.14_linux sudoku-problem.cnf sudoku-problem.ans > minisat.log
python nonc-sudoku-ans-out.py < sudoku-problem.ans > out.txt

Usage: ./run.sh [input file]

 

 

Constraint propagation

Using this method it’s easy to find inconsistency. It’s necesarry to use depth-first search. But the process is optimized – unwanted combinations are excluded.

nonc-sudoku.py: 

"""

Lightweight nonconsecutive sudoku solving by constraint propagation and recursive depth-first search.

Based on "Solve Every Sudoku Puzzle" by Google's Director of Research Peter Norvig:
http://norvig.com/sudoku.html

"""

from sys import stdin

## Throughout this program we have:
##   r is a row,    e.g. 'A'
##   c is a column, e.g. '3'
##   s is a square, e.g. 'A3'
##   d is a digit,  e.g. '9'
##   u is a unit,   e.g. ['A1','B1','C1','D1','E1','F1','G1','H1','I1']
##   grid is a grid,e.g. 81 non-blank chars, e.g. starting with '.18...7...
##   values is a dict of possible values, e.g. {'A1':'12349', 'A2':'8', ...}

def cross(A, B):
    "Cross product of elements in A and elements in B:"
    return [a+b for a in A for b in B]

digits   = '123456789'
rows     = 'ABCDEFGHI'
cols     = digits
squares  = cross(rows, cols)
unitlist = ([cross(rows, c) for c in cols] +
            [cross(r, cols) for r in rows] +
            [cross(rs, cs) for rs in ('ABC','DEF','GHI') for cs in ('123','456','789')])
units = dict((s, [u for u in unitlist if s in u])
             for s in squares)
peers = dict((s, set(sum(units[s],[]))-set([s]))
             for s in squares)

################ Parse a Grid ################

def parse_grid(grid):
    "Convert grid to a dict of possible values, {square: digits}, or return False if a contradiction is detected:"
    ## To start, every square can be any digit; then assign values from the grid.
    values = dict((s, digits) for s in squares)
    for s,d in grid_values(grid).items():
        if d in digits and not assign(values, s, d):
            return False ## (Fail if we can't assign d to square s.)
    return values

def grid_values(grid):
    "Convert grid into a dict of {square: char} with '0' or '.' for empties:"
    chars = [c for c in grid if c in digits or c in '0.']
    assert len(chars) == 81
    return dict(zip(squares, chars))

################ Constraint Propagation ################

def neighbours(of):
    "Find possible neighbours of a square:"
    neighbours=[]
    row,col=[ of[0], of[1] ]
    up,down,left,right=[True,True,True,True]
    if row == 'A': up = False
    if row == 'I': down = False
    if col == '1': left = False
    if col == '9': right = False
    if up: neighbours.append(chr(ord(row) - 1) + col)
    if down: neighbours.append(chr(ord(row) + 1) + col)
    if left: neighbours.append(row + str(int(col) - 1))
    if right: neighbours.append(row + str(int(col) + 1))
    return neighbours

def assign(values, s, d):
    "Eliminate all the other values (except d) from values[s] and propagate. Return values, except return False if a contradiction is detected."
    other_values = values[s].replace(d, '')
    if all(eliminate(values, s, d2) for d2 in other_values):
        "Nonconsecutive Sudoku condition: eliminate consecutive_values from all possible neighbours:"
        if all(eliminate(values, neighbour, consecutive_value) for consecutive_value in [str(int(d) + 1), str(int(d) - 1)] for neighbour in neighbours(s)):
           return values
    else:
        return False

def eliminate(values, s, d):
    "Eliminate d from values[s]; propagate when values or places <= 2.Return values, except return False if a contradiction is detected:"
    if d not in values[s]:
        return values ## Already eliminated
    values[s] = values[s].replace(d,'')
    ## (1) If a square s is reduced to one value d2, then eliminate d2 from the peers.
    if len(values[s]) == 0:
        return False ## Contradiction: removed last value
    elif len(values[s]) == 1:
        d2 = values[s]
        if not all(eliminate(values, s2, d2) for s2 in peers[s]):
            return False
    ## (2) If a unit u is reduced to only one place for a value d, then put it there.
    for u in units[s]:
        dplaces = [s for s in u if d in values[s]]
        if len(dplaces) == 0:
            return False ## Contradiction: no place for this value
        elif len(dplaces) == 1:
            # d can only be in one place in unit; assign it there
            if not assign(values, dplaces[0], d):
                return False
    return values
    
################ Search ################
    
def some(seq):
    "Return some element of seq that is true:"
    for e in seq:
        if e: return e
    return False

def search(values):
    "Using depth-first search and propagation, try all possible values:"
    if values is False:
        return False ## Failed earlier
    if all(len(values[s]) == 1 for s in squares):
        return values ## Solved!
    ## Chose the unfilled square s with the fewest possibilities
    n,s = min((len(values[s]), s) for s in squares if len(values[s]) > 1)
    return some(search(assign(values.copy(), s, d))
                for d in values[s])
                            
def solve(grid):
    return search(parse_grid(grid))
    
def read_input():
    "Read sudoku input file from standard input:"
    values=''
    for line in stdin:
        for char in line:
            if char not in ['-','+','|','\n']: values+=char
    return values
    
def print_output(values):
    "Display these values as a 2-D grid:"
    width = 1+max(len(values[s]) for s in squares)
    line = '+'.join(['-'*(width*3)]*3)
    print("")
    for r in rows:
        print ''.join(values[r+c].center(width)+('|' if c in '36' else '') for c in cols)
        if r in 'CF': print line
    print    
    
################ Main  ################
    
if __name__ == '__main__':
    print_output(solve(read_input()))

Usage:  python nonc-sudoku.py < [input file]

 

 

Testing

sudoku.run is script for running all mentioned algorithms and calculate duration times


#!/bin/bash
echo " ____________________________________________ "
echo "/ Nonconsecutive Sudoku algorithms benchmark \\"
echo "\\ ARUO project by cis027 /"
echo " -------------------------------------------- "
if [ "$#" -ne 2 ] || ! [ -f "$2" ]; then
echo ""
echo " Usage:"
echo " sudoku.run {123456} [input file name]"
echo ""
echo " Parameters:"
echo ""
echo "(1) Solve by constraint propagation and search"
echo "(2) Generate CNF and execute Minisat solver"
echo "(3) Solve using PyEDA module"
echo "(4) Generate SMT and execute CVC4 solver"
echo "(5) Solve by recursive brute-force algorithm"
echo "(6) Solve using python-constraint module"
echo ""
echo " Input file format example:"
echo ""
echo " 000|000|400"
echo " 000|000|060"
echo " 000|460|000"
echo " ---+---+---"
echo " 000|000|006"
echo " 060|000|040"
echo " 004|000|000"
echo " ---+---+---"
echo " 000|604|000"
echo " 600|000|000"
echo " 040|000|000"
echo ""
exit 1
fi
echo "Input file $2:"
echo ""
cat $2
echo ""
if [[ "$1" == *1* ]]; then
echo "================================================"
echo -ne "1) Solving by constraint propagation and search: "
cd constraint-propagation
/usr/bin/time -f "Done\nDuration:%E" python nonc-sudoku.py < ../$2 > out.txt
echo "Output:"
cat out.txt
cd ..
fi
if [[ "$1" == *2* ]]; then
echo "==============================================="
echo -ne "2) Generating CNF and executing Minisat solver: "
cd cnf-to-minisat
/usr/bin/time -f "Done\nDuration:%E" ./run.sh ../$2
echo "Output:"
cat out.txt
cd ..
fi
if [[ "$1" == *3* ]]; then
echo "==============================================="
echo -ne "3) Solving by PyEDA module: "
cd pyeda-sat
/usr/bin/time -f "Done\nDuration:%E" python nonc-sudoku3.py < ../$2 > out.txt
echo "Output:"
cat out.txt
cd ..
fi
if [[ "$1" == *4* ]]; then
echo "================================================"
echo -ne "4) Generating SMT and executing CVC4 solver: "
cd smt-to-cvc4
/usr/bin/time -f "Done\nDuration:%E" ./run.sh ../$2
echo "Output:"
cat out.txt
cd ..
fi
if [[ "$1" == *5* ]]; then
echo "================================================"
echo -ne "4) Solving by recursive brute-force algorithm: "
cd brute-force
/usr/bin/time -f "Done\nDuration:%E" python nonc-sudoku5.py < ../$2 > out.txt
echo "Output:"
cat out.txt
cd ..
fi
if [[ "$1" == *6* ]]; then
echo "================================================"
echo -ne "4) Solving by python-constraint module: "
cd brute-force
/usr/bin/time -f "Done\nDuration:%E" python nonc-sudoku6.py < ../$2 > out.txt
echo "Output:"
cat out.txt
cd ..
fi

Usage: sudoku.run {123456} [input file] 

{123456} : solving method (for example sudoku run 135 input.txt)

 

 

Conclusion

Time needed to solve same (test) input file:

  1. Constraint propagation : 0.142 s
  2. CNF pre Minisat solver : 0.513 s
  3. PyEDA : 35.032 s
  4. SMT pre CVC4 solver : 1 m 17.802 s
  5. Brute-force : 2 m 52.068 s
  6. Python-constraint : 3 m 2.848 s

 

Download

  • All source codes with Linux binaries MiniSat_v1.14_linuxcvc4-1.0-x86_64-linux-opt a python modulmi pyedapython-constraint are compressed in one zip archíve: nonconsecutive-sudoku.zip

 

“Sudoku is a denial of service attack on human intellect”

security expert Ben Laurie

Tagy:

@cisary on twitter


Bitcoin, web applications, constraint processing, AI, soft-computing - evolution inspired algorithms, integration with the blockchain technology and more.    


Contact



Agile Software Development


cisary @ Github cisary @ Bitbutcket






Newest articles





Twitter & Delicious




  • New (beta) website