Number-link solver

numberlink-sample.txt

....321
....1..
.......
..2....
.......
.35..4.
4.....5

numberlink.js

#! /usr/bin/env node

'use strict';

const Logic = require('logic-solver')

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

  const max = field.flat().reduce((a, b) => Math.max(a, b))
  let nbit = 0
  for (nbit = 0; ; ++nbit) {
    if (max < 1 << nbit)
      break
  }

  const h = field.length
  const w = field[0].length
  const numbers = [...Array(h)].map((_, r) =>
    [...Array(w)].map((_, c) => Logic.variableBits(`N${r},${c}`, nbit)))

  // Constraints
  for (let r = 0; r < h; ++r) {
    for (let c = 0; c < w; ++c) {
      const terms = [
        r > 0     ? vertLine(r - 1, c) : null,
        r < h - 1 ? vertLine(r    , c) : null,
        c > 0     ? horzLine(r, c - 1) : null,
        c < w - 1 ? horzLine(r, c    ) : null,
      ].filter(term => term)
      if (field[r][c] !== 0) {
        logicSolver.require(Logic.exactlyOne(terms))
        logicSolver.require(Logic.equalBits(numbers[r][c], Logic.constantBits(field[r][c])))
      } else {
        logicSolver.require(
          // Logic.or(
          //   Logic.and(terms.map(term => Logic.not(term))),
            exactlyN(terms, 2)
          // )
        )
      }
    }
  }
  // Number is linked if line exists.
  for (let r = 0; r < h - 1; ++r)
    for (let c = 0; c < w; ++c)
    logicSolver.require(Logic.implies(vertLine(r, c), Logic.equalBits(numbers[r][c], numbers[r + 1][c])))
  for (let r = 0; r < h; ++r)
    for (let c = 0; c < w - 1; ++c)
    logicSolver.require(Logic.implies(horzLine(r, c), Logic.equalBits(numbers[r][c], numbers[r][c + 1])))
  for (const number of numbers.flat()) {
    logicSolver.require(Logic.greaterThanOrEqual(number, Logic.constantBits(1)))
    logicSolver.require(Logic.lessThanOrEqual(number, Logic.constantBits(max)))
  }
  // Forbid simple detour.
  for (let r = 0; r < h - 1; ++r) {
    for (let c = 0; c < w - 1; ++c) {
      const terms = [
        horzLine(r, c),
        vertLine(r, c + 1),
        horzLine(r + 1, c),
        vertLine(r, c),
      ]
      for (let i = 0; i < 4; ++i)
        logicSolver.forbid(Logic.and(terms.filter((_, j) => i !== j)))
    }
  }

  const solutions = []
  for (;;) {
    const sol = logicSolver.solve()
    if (sol == null)
      break

    solutions.push(sol)
    logicSolver.forbid(sol.getFormula())
  }

  return solutions
}

function exactlyN(terms, n) {
  if (n <= 0)
    return Logic.not(Logic.or(terms))
  if (terms.length < n)
    return Logic.FALSE
  if (n === 1)
    return Logic.exactlyOne(terms)

  const head = terms[0]
  const tail = terms.slice(1)
  return Logic.or(
    Logic.and(head, exactlyN(tail, n - 1)),
    Logic.and(Logic.not(head), exactlyN(tail, n))
  )
}

function horzLine(r, c) {
  return `H${r},${c}`
}

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

function dispSolution(field, sol) {
  const CrossLines = [' ', '・', '・', '━', '・', '┛', '┗', '┻', '・', '┓', '┏', '┳', '┃', '┫', '┣', '╋']
  const digits = '　１２３４５６７８９ＡＢＣＤＥＦＧＨＩＪＫＬＭＮＯＰＱＲＳＴＵＶＷＸＹＺ'

  const h = field.length
  const w = field[0].length
  const horz = [...Array(h)].map((_, r) => [...Array(w - 1)].map((_, c) => sol.evaluate(horzLine(r, c))))
  const vert = [...Array(h - 1)].map((_, r) => [...Array(w)].map((_, c) => sol.evaluate(vertLine(r, c))))

  for (let r = 0; r < h; ++r) {
    const line = [...Array(w)].map((_, c) => {
      const n = field[r][c]
      if (n !== 0)
        return digits[n]
      let v = 0
      if (c > 0     && horz[r][c - 1] > 0)  v |= 1 << 0
      if (c < w - 1 && horz[r][c    ] > 0)  v |= 1 << 1
      if (r > 0     && vert[r - 1][c] > 0)  v |= 1 << 2
      if (r < h - 1 && vert[r    ][c] > 0)  v |= 1 << 3
      return `${CrossLines[v]} `
    })
    console.log(line.join(''))
  }
}

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

  const solutions = solveNumberLink(field)
  if (solutions.length <= 0) {
    console.error('No solution')
  } else {
    if (solutions.length >= 2) {
      console.error(`Multiple solutions (#${solutions.length})`)
    }

    for (const sol of solutions)
      dispSolution(field, sol)
  }
}

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()