initial commit

.gitignore

@@ -0,0 +1 @@
+solver

.vscode/tasks.json

@@ -0,0 +1,27 @@
+{
+    // See https://go.microsoft.com/fwlink/?LinkId=733558
+    // for the documentation about the tasks.json format
+    "version": "2.0.0",
+    "tasks": [
+        {
+            "label": "build",
+            "type": "shell",
+            "command": "nim c solver.nim",
+            "group": "build",
+            "presentation": {
+                // Reveal the output only if unrecognized errors occur.
+                "reveal": "silent"
+            },
+        },
+        {
+            "label": "build-release",
+            "type": "shell",
+            "command": "nim c -d:release --opt:speed solver.nim",
+            "group": "build",
+            "presentation": {
+                // Reveal the output only if unrecognized errors occur.
+                "reveal": "silent"
+            },
+        }
+    ]
+}

README.md

@@ -0,0 +1,21 @@
+Sudoku Solver
+=============
+
+Solves a sudoku input of arbitrary format (see [`./input.sudoku.txt`](./input.sudoku.txt)) by
+encoding it as a SAT problem in CNF format, and feeding it to arbitrary
+SAT Solver (e.g. `riss`, `glucose`, defaults to `riss`).
+Then it parses the satisfiable model and finally outputs the completed
+sudoku.
+
+## Compiling
+1. Make sure you have installed [nim](https://nim-lang.org/install.html)
+2. `nim c solver.nim` or `nim c -d:release solver.nim` for release build
+
+## Running
+```sh
+./solver --solver glucose input.sudoku.txt
+```
+
+---
+
+Encoding is based on the works of [Kwon and Jain](http://www.cs.cmu.edu/~hjain/papers/sudoku-as-SAT.pdf) and at-most-one encoding by [Klieber and Kwon](https://www.cs.cmu.edu/~wklieber/papers/2007_efficient-cnf-encoding-for-selecting-1.pdf).

cnf.nim

@@ -0,0 +1,32 @@
+import strutils
+import streams
+import intsets
+
+type Literal* = int
+type Clause* = seq[Literal]
+type Cnf* = object
+    numLiterals*: int
+    clauses*: seq[Clause]
+
+
+proc addLiterals*(cnf: var Cnf, n: int) =
+    cnf.numLiterals += n
+
+proc initCNF*(numLiterals: int): Cnf =
+    let clauses = newSeq[Clause]()
+
+    return Cnf(
+        numLiterals: numLiterals,
+        clauses: clauses,
+    )
+
+proc add*(cnf: var Cnf, clause: Clause) =
+    cnf.clauses.add(clause)
+
+
+proc print*(cnf: Cnf, stream: Stream) =
+    stream.writeLine("p cnf " & $cnf.numLiterals & " " & $cnf.clauses.len)
+    for clause in cnf.clauses:
+        for item in clause:
+            stream.write($item & " ")
+        stream.writeLine("0")

encodings.nim

@@ -0,0 +1,92 @@
+import cnf
+import sequtils
+import utils
+
+proc atLeastOne*(literals: seq[Literal]): seq[Clause] = @[literals]
+
+proc atMostOnePairwise*(literals: seq[Literal]): seq[Clause] =
+    result = newSeq[Clause]()
+    for i in 0..<literals.len:
+        for j in i+1..<literals.len:
+            result.add(@[-literals[i], -literals[j]])
+
+proc getCommanders(binaries: seq[Literal], index: int): seq[Literal] =
+    var power = 1
+    result = newSeq[Literal]()
+    for i in 0..<binaries.len:
+        if (index and power) == power:
+            result.add(binaries[i])
+        else:
+            result.add(-binaries[i])
+        power = power shl 1
+
+proc exactlyOne*(cnf: var Cnf, literals: seq[Literal], pairwise: bool = false): seq[Clause]
+
+proc atMostOneCommander*(cnf: var Cnf, literals: seq[Literal]): seq[Clause] =
+    # Commander Encoding [Klieber and Kwon]
+    if literals.len < 6:
+        return atMostOnePairwise(literals)
+
+    let m = literals.len div 3
+    let groups = literals.distribute(m)
+    let commanders = toSeq(cnf.numLiterals+1..cnf.numLiterals+groups.len)
+    cnf.addLiterals(groups.len)
+    result = newSeq[Clause]()
+
+    # at most one variable in a group can be true
+    for group in groups:
+        result.add(atMostOnePairWise(group))
+
+    for zipped in zip(commanders, groups):
+        let (commander, group) = zipped
+        let commanderAndGroup = @[-commander].concat(group)
+        result.add(atLeastOne(commanderAndGroup))
+        result.add(atMostOnePairwise(commanderAndGroup))
+
+    if commanders.len >= 3:
+        result.add(cnf.exactlyOne(commanders))
+    else:
+        result.add(cnf.exactlyOne(commanders, pairwise=true))
+
+
+proc getGroupSize(n: int): int =
+    let limit = n div 2
+    result = 1
+    while (result shl 1) - 1 <= limit:
+        result = result shl 1
+    result -= 1
+
+# Not used for the moment since it's somehow takes too long
+# to solve with this encoding
+proc atMostOne*(cnf: var Cnf, literals: seq[Literal]): seq[Clause] =
+    # Bimander Encoding [Hölldobler and Nguyen, 2013]
+    let m = getGroupSize(literals.len)
+    let numDigits = log2(m)
+    if literals.len <= m:
+        return atMostOnePairwise(literals)
+    let groups = literals.distribute(m)
+    let binaries = toSeq(cnf.numLiterals+1..cnf.numLiterals+numDigits)
+    cnf.addLiterals(numDigits)
+    result = newSeq[Clause]()
+
+    # at most one variable in a group can be true
+    for group in groups:
+        result.add(atMostOnePairWise(group))
+
+    # constraints between each variable in a group and commander variables
+    for pair in groups.pairs():
+        let (index, group) = pair
+        let commanders = binaries.getCommanders(index)
+        for literal in group:
+            for commander in commanders:
+                result.add(@[-literal, commander])
+
+proc exactlyOne*(cnf: var Cnf, literals: seq[Literal], pairwise: bool = false): seq[Clause] =
+    if literals.len == 0: return @[]
+    result = newSeq[Clause]()
+    if not pairwise:
+        # result.add(cnf.atMostOne(literals))
+        result.add(cnf.atMostOneCommander(literals))
+    else:
+        result.add(atMostOnePairwise(literals))
+    result.add(atLeastOne(literals))

input.sudoku.txt

@@ -0,0 +1,25 @@
+experiment: 4x4
+number of tasks: 1
+task: 1
+puzzle size: 4x4
++-------------+-------------+-------------+-------------+
+| __ __ __  5 | __ __ __ __ | __ 12 __ __ |  7 10 __ __ |
+| 13 __ __  4 | __ __ __ 12 |  5 15  9 __ |  8 __ 14 11 |
+|  3 14  7 __ | __ __  8 __ | __ __  1 __ | __ __ 13  2 |
+|  6  8  1 __ | 16 11 __ 14 |  2  7 13  4 | 15  3 __ __ |
++-------------+-------------+-------------+-------------+
+| __ __ __  7 | 10 __ __ __ | __  2 __ __ | 14 __ __  6 |
+| __  6 __ __ | __ __ 14 __ | __  3 16 12 | 11 __  1 __ |
+| __ 10 __ __ | 15  1 12 __ | __ __  6 __ |  2  4  3  7 |
+|  5 12 __ 11 | __ __  9  2 | 14  1 __ __ | __ 15 16 10 |
++-------------+-------------+-------------+-------------+
+|  4  7  3 __ | __ __  6  9 | 12 11 __ __ |  1 __ 10 16 |
+| 14 15 11  1 | __ 10 __ __ | __  9  7  3 | __ __  8 __ |
+| __  9 __ 13 | 11 12 15 __ | __  5 __ __ | __ __  7 __ |
+| 12 __ __  6 | __ __  1 __ | __ __ __  2 |  9 __ __ __ |
++-------------+-------------+-------------+-------------+
+| __ __ 12 16 |  6 14  3  5 |  1 __  2  9 | __  7 11 15 |
+| 15  1 __ __ | __  9 __ __ | __ 16 __ __ | __ 13  4 12 |
+|  7 11 __  3 | __ 13  2  1 | 15 __ __ __ | 16 __ __ 14 |
+| __ __ 14 10 | __ __  4 __ | __ __ __ __ |  5 __ __ __ |
++-------------+-------------+-------------+-------------+

solver.nim

@@ -0,0 +1,62 @@
+import cnf
+import os
+import osproc
+import parseopt
+import streams
+import sudoku
+import times
+import utils
+
+proc main() =
+    var
+        start = cpuTime()
+        before = 0
+        fileName = ""
+        solver = "riss"
+
+    for kind, key, val in getopt():
+        case kind
+        of cmdArgument:
+            fileName = key
+        of cmdShortOption, cmdLongOption:
+            case key
+            of "g", "glucose": solver = "glucose"
+            of "r", "riss": solver = "riss"
+            of "s", "solver": solver = val
+            of "h", "help": printHelpAndExit()
+        of cmdEnd: assert(false)
+
+    if filename == "": printHelpAndExit()
+
+
+    let inputStream = newFileStream(fileName)
+    let sudoku: Sudoku = deserialize(inputStream)
+    inputStream.close()
+    log "Parsed input in ", cpuTime() - start
+
+    start = cpuTime()
+    var cnf = sudoku.generateBaseCNF()
+    log "Generated ", cnf.clauses.len, " base clauses in ", cpuTime() - start
+
+    const CNF_FILENAME = "sudoku.cnf"
+    start = cpuTime()
+    let cnfStream = openFileStream(CNF_FILENAME, mode = fmWrite)
+    cnf.print(cnfStream)
+    cnfStream.close()
+
+    log "Writes cnf in ", cpuTime() - start
+
+    var p: Process
+    case solver
+        of "glucose": p = startProcess("glucose", args=["-model", CNF_FILENAME], options={poUsePath})
+        of "riss": p = startProcess("riss", args=[CNF_FILENAME], options={poUsePath})
+        else: p = startProcess(solver, args=[CNF_FILENAME], options={poUsePath})
+
+    start = cpuTime()
+    sudoku.serialize(p.outputStream, newFileStream(stdout))
+    log "Serialized cnf solution in ", cpuTime() - start
+    p.close()
+
+    discard tryRemoveFile(CNF_FILENAME)
+
+when isMainModule: main()