# CSP Spec

Paradigm(s) | Declarative |
---|---|

Designed by | User:Hakerh400 |

Appeared in | 2021 |

Computational class | Category:Turing complete |

Major implementations | Implementation in Electron |

File extension(s) | `.txt` |

**CSP Spec** is a work-in-progress declarative esoteric programming language invented by User:Hakerh400 in 2021. CSP stands for Constraint satisfaction problem and Spec stands for "Specification".

## Overview

This programming language is intended to be used for specifying and implementing puzzle games. The language is not finished yet, but most of the features are already implemented. The goal is to be able to specify a puzzle game in a short, concise way.

A program written in **CSP Spec** defines a puzzle game. It includes: shape of the board, rules, controls, options, parameters, user input, graphical rendering of the game, level generator and level solver. Therefore, **CSP Spec** can be considered a framework for defining puzzle games.

## Examples

Currently, there is only one game implemented in **CSP Spec**: Sudoku.

### Sudoku

params | dim | pair pnat def n | mulv dim clues grid | grid_squares n n | fin n def f \(v p) div p dim [rows, cols, group f].all \f (f grid).all neqv grid.render_group f \(v p g) [bg white, text v.inc <g black blue>] grid.input_int [1, n] dec

The code above is the entire specification and implementation of the Sudoku game. Let's analyze it line by line.

The first line `params | dim | pair pnat`

defines the parameters for the game. Function `params`

takes parameters from the level generator form and passes them to the program. Here we specify parameter `dim`

, which represents the dimensions of the board (grid). The pipe character `|`

is like the dollar operator in Haskell. The `pair pnat`

defined the type of the parameter `dim`

. The type `pair pnat`

represents a pair of two positive natural numbers. The `dim`

represents width and height of sections of the grid (for the regular `9x9`

sudoku, `dim`

has value `(3, 3)`

).

Next, `def n | mulv dim`

defines constant `n`

which is equal to the product of elements of `dim`

. Function `mulv`

is like `product`

in Haskell. The number `n`

represents the size (width and height) of the sudoku puzzle (for `9x9`

sudoku, `n`

is `9`

).

`clues grid | grid_squares n n | fin n`

defines clues (numbers on the grid that are "given" to the player). It is defined as a grid of dimensions . Each grid cell (tile) is of type `fin n`

, which represents the type of natural numbers smaller than `n`

. It means that the numbers in the grid are internally represented as numbers from `0`

to `n-1`

, instead of `1`

to `n`

.

`def f \(v p) div p dim`

defines function `f`

which takes two arguments `v`

and `p`

. Then we return the result of dividing `p`

with `dim`

(division of natural numbers rounds down). Dividing two pairs represents dividing corresponding elements.

The line `[rows, cols, group f].all \f (f grid).all neqv`

specifies the rules of the game. It says that in each row, collumn and section all numbers are different. Function `group`

partitions the grid based on the given partition function.

`grid.render_group f \(v p g) [bg white, text v.inc <g black blue>]`

- this specifies how the game is rendered (displayed on screen). The `<>`

brackets represent ternary if-then-else statement. Basically, we render the grid by highlighting grid regions based on partition function `f`

. We render each tile by taking three variables `v`

, `p`

and `g`

, and then we pass two monadic actions to the rendering monad. Variable `v`

represents the value of the current tile (in the `Maybe`

monad, so all actions are implicitly lifted to `Maybe`

). Variable `p`

represents the coordinates of the tile. Variable `g`

is boolean which is true iff the value of the given tile has been "given" to the user at the start of the game. The first action we execute is `bg white`

, which paints the background of the tile in `white`

. The second action is `text v.inc <g black blue>`

, which renders the text representing the value (number) of the current tile. The colors `white`

, `black`

and `blue`

are global constants (there is also a way to specify color by RGB values).

Finally, `grid.input_int [1, n] dec`

specifies user input. It says that the user can input a number from interval `[1, n]`

to any tile of the grid as long as the number is not "given". The post-processing function `dec`

decrements the number to adapt it to the internal representation, which is in interval `[0, n - 1]`

.

## Level generator

The interpreter uses SAT solver to automatically generate level generator and level solver for the game, based on the game specification. The user may specify SAT solver to be used. The SAT solver must support input in DIMACS format. The interpreter has been tested on CaDiCaL, Cryptominisat and Kissat solvers.

The level generator starts with the empty grid. Generator represents all tiles as placeholders for lists of bits. Generator then picks a random bit and assigns it a random value (0 or 1). Then generator asks the SAT solver whether there exists a level that has a bit with that value in that position. If the SAT solver says "yes", then the generator picks the next bit and proceeds. If the answer is "no", the generator flips the bit and proceeds. This is repeated until all bits have values.

Next, the generator starts removing clues in groups, as long as the level has a unique solution. Generator picks a random tile and removes the clue from that tile. Then asks the SAT solver whether there exists a unique solution. If the answer is "yes", then it proceeds to next random tile. If the answer is "no", the generator restores the clue and moves on. It keeps doing so until it checks all clues.

The resulting generated level has a unique solution according to the rules of the game. Moreover, removing any given clue will introduce another solution. So, in some sense, it contains the minimal number of clues (although it's not the global minimum).