Sudoku solver

sudoku-sample.txt

8....51..
..1...8..
.4.2...9.
....3...2
1234 6789
6...1....
.8...9.5.
..2...4..
..76....1

sudoku.js

#! /usr/bin/env node

'use strict';

const Logic = require('logic-solver')

const BITS = 4

function solveSudoku(field) {
  const logicSolver = new Logic.Solver()

  // Locations
  const locs = field.map((row, r) =>
    row.map((_, c) =>
      Logic.variableBits(varName(r, c), BITS)))

  // Constraints
  const h = 9  // field.length
  const w = 9  // field[0].length
  for (let r = 0; r < h; ++r) {
    for (let c = 0; c < w; ++c) {
      const loc = locs[r][c]
      const n = field[r][c]
      if (n === 0) {
        logicSolver.require(Logic.greaterThanOrEqual(loc, Logic.constantBits(1)))
        logicSolver.require(Logic.lessThanOrEqual(loc, Logic.constantBits(9)))
      } else {
        logicSolver.require(Logic.equalBits(loc, Logic.constantBits(n)))
      }
    }
  }
  // Horizontal
  for (let r = 0; r < h; ++r) {
    const terms = [...Array(w)].map((_, c) => locs[r][c])
    logicSolver.require(differentEachOther(terms))
  }
  // Vertical
  for (let c = 0; c < w; ++c) {
    const terms = [...Array(h)].map((_, r) => locs[r][c])
    logicSolver.require(differentEachOther(terms))
  }
  // Box
  for (let r = 0; r < h; r += 3) {
    for (let c = 0; c < w; c += 3) {
      const terms = [...Array(3 * 3)].map((_, i) => locs[r + ((i / 3) | 0)][c + i % 3])
      logicSolver.require(differentEachOther(terms))
    }
  }

  const solutions = []
  for (;;) {
    const sol = logicSolver.solve()
    if (sol == null)
      break
    solutions.push(sol)
    logicSolver.forbid(sol.getFormula())
  }
  if (solutions.length === 1) {
    const sol = solutions[0]
    return locs.map(row => row.map(v => sol.evaluate(v)))
  }
  if (solutions.length === 0) {
    console.error('No solution')
  } else {
    console.error(`Many solutions: #${solutions.length}`)
  }
  return null
}

function differentEachOther(terms) {
  const diffs = []
  for (var i = 0; i < terms.length - 1; ++i) {
    for (var j = i; ++j < terms.length; )
      diffs.push(Logic.not(Logic.equalBits(terms[i], terms[j])))
  }
  return Logic.and(diffs)
}

function varName(r, c) {
  return `V${r},${c}`
}

function dispSolution(solution) {
  const digits = '１２３４５６７８９'
  for (let r = 0; r < solution.length; ++r) {
    const row = solution[r]
    const line = row.map((_, c) => digits[row[c] - 1])
    console.log(line.join(''))
  }
}

function processInput(input) {
  const field = input
    .split('\n')
    .filter(line => line)
    .map(line => [...line].map(e => parseInt(e) || 0))

  const solution = solveSudoku(field)
  if (solution != null)
    dispSolution(solution)
}

async function main() {
  if (process.argv.length > 2) {
    const fs = require('fs')
    const util = require('util')
    const readFileAsync = util.promisify(fs.readFile)
    for (let i = 2; i < process.argv.length; ++i) {
      const input = await readFileAsync(process.argv[i], 'utf-8')
      processInput(input)
    }
  } else {
    const buffers = []
    for await (const chunk of process.stdin)
      buffers.push(chunk)
    const buffer = Buffer.concat(buffers)
    processInput(buffer.toString())
  }
}

if (require.main == module)
  main()