Sudoku

Sudoku are a logic-based, combinatorial number placement puzzle. The objective is to fill a grid with digits such that each column, row and sub-grid contains all the required digits.

This is usually a 9x9 grid, with 9 3x3 sub-grids.

Solving a 4x4 sudoku with SAT

In this vignette, this 4x4 sudoku will be solved using SAT techniques.

Nomenclature

To start, assign a name to each cell.

E.g. c23 is the cell in the second row, third column.

Each cell is represented by 4 variables - one for each possible digit that can exist at the location.

E.g.

  • c231 indicates that the number 1 is present in the cell in the second row, third column.
  • c413 indicates that the number 3 is present in the cell in the fourth row, first column.

Constraints

  • Each cell must contain one (and only one) of the numbers 1-4
    • E.g. c111 and c112 cannot both be true
  • Each of the numbers (1-4) must appear in each row, each column, and within each of the 2x2 sub-squares
  • In the definition of this particular problem, there is a 3 in the second column of the first row. This means that c123 is true (and c121, c122 and c124 are false)
    • Similarly: c222, c233 and c444 are true as they are the starting state of the problem

Defining a SAT problem - building blocks

A SAT problem is defined by combinations of expressions about the variables. Each of these expressions is constructed as a string.

Building block: at least one of a set of variables must be true.

If a, b and c are Boolean variables, to state that at least one of them must be true is:

a | b | c

To add this constraint to a sat object, use the cardinality helper function i.e. sat_card_atleast_one()

sat <- sat_new()
sat <- sat_card_atleast_one(sat, c('a', 'b', 'c'))
sat$exprs
   [1] "a | b | c"

Building block: at most one of a set of variables must be true

To express that only one variable is true out of a set of variables, one method is to state that “for all possible pairings, one of them must be false”.

If a, b and c are Boolean variables, to state that at most one of them must be true is:

(!a | !b) & (!a | !c) & (!b | !c)

To add this constraint to a sat object, use the cardinality helper function i.e. sat_card_atmost_one()

sat <- sat_new()
sat <- sat_card_atmost_one(sat, c('a', 'b', 'c'))
sat$exprs
   [1] "!a | !b" "!a | !c" "!b | !c"

Building block: exactly one of a set of variables must be true

A common way to express that exactly one out of a set of variables is true is to state that “at least one is true” and “at most one is true” at the same time i.e.

(a | b | c) & (!a | !b) & (!a | !c) & (!b | !c)

To add this constraint to a sat object, use the cardinality helper function i.e. sat_card_exactly_one()

sat <- sat_new()
sat <- sat_card_exactly_one(sat, c('a', 'b', 'c'))
sat$exprs
   [1] "!a | !b"   "!a | !c"   "!b | !c"   "a | b | c"

Defining the SAT problem with {satire}

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Create a new SAT problem
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat <- sat_new()

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# For each cell in the puzzle, it must contain exactly one of 1,2,3 or 4.
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_exactly_one(sat, c('c111', 'c112', 'c113', 'c114'))
sat_card_exactly_one(sat, c('c121', 'c122', 'c123', 'c124'))
sat_card_exactly_one(sat, c('c131', 'c132', 'c133', 'c134'))
sat_card_exactly_one(sat, c('c141', 'c142', 'c143', 'c144'))

sat_card_exactly_one(sat, c('c211', 'c212', 'c213', 'c214'))
sat_card_exactly_one(sat, c('c221', 'c222', 'c223', 'c224'))
sat_card_exactly_one(sat, c('c231', 'c232', 'c233', 'c234'))
sat_card_exactly_one(sat, c('c241', 'c242', 'c243', 'c244'))

sat_card_exactly_one(sat, c('c311', 'c312', 'c313', 'c314'))
sat_card_exactly_one(sat, c('c321', 'c322', 'c323', 'c324'))
sat_card_exactly_one(sat, c('c331', 'c332', 'c333', 'c334'))
sat_card_exactly_one(sat, c('c341', 'c342', 'c343', 'c344'))

sat_card_exactly_one(sat, c('c411', 'c412', 'c413', 'c414'))
sat_card_exactly_one(sat, c('c421', 'c422', 'c423', 'c424'))
sat_card_exactly_one(sat, c('c431', 'c432', 'c433', 'c434'))
sat_card_exactly_one(sat, c('c441', 'c442', 'c443', 'c444'))
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Column 1 must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c111', 'c211', 'c311', 'c411'))
sat_card_atleast_one(sat, c('c112', 'c212', 'c312', 'c412'))
sat_card_atleast_one(sat, c('c113', 'c213', 'c313', 'c413'))
sat_card_atleast_one(sat, c('c114', 'c214', 'c314', 'c414'))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Column 2 must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c121', 'c221', 'c321', 'c421'))
sat_card_atleast_one(sat, c('c122', 'c222', 'c322', 'c422'))
sat_card_atleast_one(sat, c('c123', 'c223', 'c323', 'c423'))
sat_card_atleast_one(sat, c('c124', 'c224', 'c324', 'c424'))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Column 3 must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c131', 'c231', 'c331', 'c431'))
sat_card_atleast_one(sat, c('c132', 'c232', 'c332', 'c432'))
sat_card_atleast_one(sat, c('c133', 'c233', 'c333', 'c433'))
sat_card_atleast_one(sat, c('c134', 'c234', 'c334', 'c434'))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Column 4 must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c141', 'c241', 'c341', 'c441'))
sat_card_atleast_one(sat, c('c142', 'c242', 'c342', 'c442'))
sat_card_atleast_one(sat, c('c143', 'c243', 'c343', 'c443'))
sat_card_atleast_one(sat, c('c144', 'c244', 'c344', 'c444'))
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Row 1 must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c111', 'c121', 'c131', 'c141'))
sat_card_atleast_one(sat, c('c112', 'c122', 'c132', 'c142'))
sat_card_atleast_one(sat, c('c113', 'c123', 'c133', 'c143'))
sat_card_atleast_one(sat, c('c114', 'c124', 'c134', 'c144'))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Row 2 must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c211', 'c221', 'c231', 'c241'))
sat_card_atleast_one(sat, c('c212', 'c222', 'c232', 'c242'))
sat_card_atleast_one(sat, c('c213', 'c223', 'c233', 'c243'))
sat_card_atleast_one(sat, c('c214', 'c224', 'c234', 'c244'))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Row 3 must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c311', 'c321', 'c331', 'c341'))
sat_card_atleast_one(sat, c('c312', 'c322', 'c332', 'c342'))
sat_card_atleast_one(sat, c('c313', 'c323', 'c333', 'c343'))
sat_card_atleast_one(sat, c('c314', 'c324', 'c334', 'c344'))

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Row 4 must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c411', 'c421', 'c431', 'c441'))
sat_card_atleast_one(sat, c('c412', 'c422', 'c432', 'c442'))
sat_card_atleast_one(sat, c('c413', 'c423', 'c433', 'c443'))
sat_card_atleast_one(sat, c('c414', 'c424', 'c434', 'c444'))
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Top-left sub-square must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c111', 'c211', 'c121', 'c221')) 
sat_card_atleast_one(sat, c('c112', 'c212', 'c122', 'c222')) 
sat_card_atleast_one(sat, c('c113', 'c213', 'c123', 'c223')) 
sat_card_atleast_one(sat, c('c114', 'c214', 'c124', 'c224')) 

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Bottom-left sub-square must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c311', 'c411', 'c321', 'c421')) 
sat_card_atleast_one(sat, c('c312', 'c412', 'c322', 'c422')) 
sat_card_atleast_one(sat, c('c313', 'c413', 'c323', 'c423')) 
sat_card_atleast_one(sat, c('c314', 'c414', 'c324', 'c424')) 

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Top-right sub-square must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c131', 'c231', 'c141', 'c241')) 
sat_card_atleast_one(sat, c('c132', 'c232', 'c142', 'c242')) 
sat_card_atleast_one(sat, c('c133', 'c233', 'c143', 'c243')) 
sat_card_atleast_one(sat, c('c134', 'c234', 'c144', 'c244')) 

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Bottom-right sub-square must have at least one 1, one 2, one 3 and one 4
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_card_atleast_one(sat, c('c331', 'c431', 'c341', 'c441')) 
sat_card_atleast_one(sat, c('c332', 'c432', 'c342', 'c442')) 
sat_card_atleast_one(sat, c('c333', 'c433', 'c343', 'c443')) 
sat_card_atleast_one(sat, c('c334', 'c434', 'c344', 'c444'))
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# The initially defined numbers in the puzzle are set to TRUE 
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat_add_exprs(sat, "c123 & c222 & c233 & c444")

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# Ready to solve
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sat
   <sat> vars = 64 , clauses = 164

Solving

There are 64 variables in this SAT problem, which means a brute-force approach would have to try ~1.8E19 combinations which is not feasible.

Instead, use the DPLL-based solver which uses unit propagation, pure-literal elimination, pruning and backtracking to find a solution.

The solution returned is the TRUE/FALSE state of every variable. It is up to the user to interpret what this means in the context of their problem

#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# 'sol' is a data.frame.  Column names are the variables, and each row
# is a solution to the problem.
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sol <- sat_solve_dpll(sat)
sol
     c111  c112  c113  c114  c121  c122 c123  c124  c131  c132  c133 c134  c141
   1 TRUE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE TRUE FALSE
     c142  c143  c144  c211  c212  c213 c214  c221 c222  c223  c224  c231  c232
   1 TRUE FALSE FALSE FALSE FALSE FALSE TRUE FALSE TRUE FALSE FALSE FALSE FALSE
     c233  c234 c241  c242  c243  c244  c311 c312  c313  c314  c321  c322  c323
   1 TRUE FALSE TRUE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE FALSE
     c324 c331  c332  c333  c334  c341  c342 c343  c344  c411  c412 c413  c414
   1 TRUE TRUE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE TRUE FALSE
     c421  c422  c423  c424  c431 c432  c433  c434  c441  c442  c443 c444
   1 TRUE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE FALSE TRUE
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
# The actual solution needed for this sudoku is where the actual numbers
# exist, I.e. where the variables are true
#~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
sol <- names(sol)[unlist(sol)]
sol
    [1] "c111" "c123" "c134" "c142" "c214" "c222" "c233" "c241" "c312" "c324"
   [11] "c331" "c343" "c413" "c421" "c432" "c444"

Plotting these true variables gives the solution to the sudoku