Slither-link solver

slither-sample.txt

.02.1.3
.......
...3.31
30...30
31.2...
.......
3.3.02.

slither.js

#! /usr/bin/env node

'use strict';

const Logic = require('logic-solver')

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

  // Constraints
  const h = field.length
  const w = field[0].length
  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 ? vertLine(r    , c) : null,
        c > 0 ? horzLine(r, c - 1) : null,
        c < w ? horzLine(r, c    ) : null,
      ].filter(term => term)
      logicSolver.require(Logic.or(
          Logic.and(terms.map(term => Logic.not(term))),
          exactlyN(terms, 2))
      )
    }
  }
  for (let r = 0; r < h; ++r) {
    for (let c = 0; c < w; ++c) {
      const n = field[r][c]
      const terms = [
        vertLine(r, c),
        vertLine(r, c + 1),
        horzLine(r, c),
        horzLine(r + 1, c),
      ]
      if (n >= 0) {
        logicSolver.require(exactlyN(terms, n))
      } else {
        // Forbid simple loop
        logicSolver.forbid(Logic.and(terms))
      }
    }
  }

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

    const loops = detectLoops(w, h, sol)
    if (loops.length === 1) {
      solutions.push(sol)
    } else if (loops.length < 1) {
      console.error(`Illegal: ${loops.length}`)  // Must not happen
      break
    }

    for (const loop of loops)
      logicSolver.forbid(Logic.and(loop))
  }
  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 detectLoops(w, h, sol) {
  const checked = new Array((w + 1) * (h + 1))
  const loops = []
  for (let r = 0; r <= h; ++r) {
    for (let c = 0; c <= w; ++c) {
      const index = r * (w + 1) + c
      if (checked[index])
        continue
      const loop = getLoop(w, h, r, c, checked, sol)
      if (loop != null)
        loops.push(loop)
    }
  }
  return loops
}

function getLoop(w, h, sr, sc, checked, sol) {
  const Dirs = [[-1, 0], [0, -1], [0, 1], [1, 0]]
  const loop = []
  let r = sr
  let c = sc
  let d = -1
  do {
    checked[r * (w + 1) + c] = true
    let i = 0
    for (; i < Dirs.length; ++i) {
      if (i === Dirs.length - d - 1)
        continue
      const [dr, dc] = Dirs[i]
      const nr = r + dr
      const nc = c + dc
      if (nr < 0 || nr > h || nc < 0 || nc > w)
        continue
      const step = dr !== 0 ? vertLine(Math.min(r, nr), c) : horzLine(r, Math.min(c, nc))
      const v = sol.evaluate(step)
      if (!v)
        continue
      loop.push(step)
      d = i
      r = nr
      c = nc
      break
    }
    if (i >= Dirs.length)
      return null
  } while (r !== sr || c !== sc)
  return loop.length > 0 ? loop : null
}

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 + 1)].map((_, r) => [...Array(w)].map((_, c) => sol.evaluate(horzLine(r, c))))
  const vert = [...Array(h)].map((_, r) => [...Array(w + 1)].map((_, c) => sol.evaluate(vertLine(r, c))))

  for (let r = 0; r <= h; ++r) {
    const line1 = [...Array(w + 1)].map((_, c) => {
      let v = 0
      if (c > 0 && horz[r][c - 1])  v |= 1 << 0
      if (c < w && horz[r][c    ])  v |= 1 << 1
      if (r > 0 && vert[r - 1][c])  v |= 1 << 2
      if (r < h && vert[ r   ][c])  v |= 1 << 3
      if (c >= w)
        return CrossLines[v]

      let v2 = 0
      if (horz[r][c])               v2 |= 3 << 0
      return `${CrossLines[v]} ${CrossLines[v2]}`
    })
    console.log(line1.join(' '))
    if (r >= h)
      break

    const line2 = [...Array(w + 1)].map((_, c) => {
      let v = 0
      if (vert[r][c])  v |= 3 << 2
      if (c >= w)
        return CrossLines[v]

      const n = field[r][c]
      const d = n >= 0 ? digits[n] : '　'
      return `${CrossLines[v]} ${d}`
    })
    console.log(line2.join(''))
  }
}

function processInput(input) {
  const field = input
    .split('\n')
    .filter(line => line)
    .map(line => [...line].map(e => {
      const v = parseInt(e, 36)
      console.assert(!isFinite(v) || (v >= 0 && v <= 3))
      return isFinite(v) ? v : -1
    }))

  const solutions = solveSlither(field)
  if (solutions.length !== 1) {
    console.error(`Solution not detected: #${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()