Interactive SudokuCurtis Bright, Maplesoft# Interactive Sudoku by Curtis Bright
with(Maplets):
with(Elements):
with(DocumentTools):
with(Layout):
with(Components):
with(StringTools):
with(Logic):
with(plots):
with(plottools):
with(ColorTools):
# Public domain Sudoku puzzle by Tim Stellmach
gameData := [
[5,3,0,0,7,0,0,0,0],
[6,0,0,1,9,5,0,0,0],
[0,9,8,0,0,0,0,6,0],
[8,0,0,0,6,0,0,0,3],
[4,0,0,0,0,3,0,0,1],
[7,0,0,0,2,0,0,0,6],
[0,6,0,0,0,0,2,8,0],
[0,0,0,4,1,9,0,0,5],
[0,0,0,0,8,0,0,7,9]]:
# Set of Boolean variables conerning digit k in the same row as (i, j)
rowVars := proc(i, j, k)
local x;
return {seq(S[x, j, k], x=1..9)} minus {S[i, j, k]};
end proc:
# Set of Boolean variables conerning digit k in the same column as (i, j)
colVars := proc(i, j, k)
local y;
return {seq(S[i, y, k], y=1..9)} minus {S[i, j, k]};
end proc:
# Set of Boolean variables conerning digit k in the same block as (i, j)
blockVars := proc(i, j, k)
local x, y, block_x, block_y;
block_x := 3*floor((i-1)/3)+1;
block_y := 3*floor((j-1)/3)+1;
return {seq(seq(S[x, y, k], y=block_y..block_y+2), x=block_x..block_x+2)} minus {S[i, j, k]};
end proc:
# Set of Boolean variables conerning digit k in the same row, column, or block as (i, j)
allVars := proc(i, j, k)
return rowVars(i, j, k) union colVars(i, j, k) union blockVars(i, j, k);
end proc:
# The rules of Sudoku encoded in Boolean logic
atLeastOneDigit := seq(seq(&or(seq(S[i,j,k], k=1..9)), j=1..9), i=1..9):
atMostOneDigit := seq(seq(seq(seq(&or(¬(S[i, j, k]), ¬(S[i, j, l])), l=k+1..9), k=1..9), j=1..9), i=1..9):
distinctnessConstraints := seq(seq(seq(seq(&or(¬(S[i, j, k]), ¬(A)), A in allVars(i, j, k)), k=1..9), j=1..9), i=1..9):
# Clauses in Boolean logic that encode the current state of the board
entryClauses := proc()
global currentBoard;
local i, j, k, clauses;
clauses := Array(1..9, 1..9);
for i from 1 to 9 do
for j from 1 to 9 do
k := currentBoard[i, j];
if k <> 0 then
# Generate unit clauses with &or to save overhead later
clauses[i, j] := &or(S[i, j, k]);
end if;
end do;
end do;
return remove(x->x=0, [entries(clauses, nolist)])[];
end proc:
# Check if the current board state is solvable by calling MapleSAT
checkGame := proc()
global gameOver;
local allClauses;
allClauses := atLeastOneDigit, atMostOneDigit, distinctnessConstraints, entryClauses();
if Satisfiable(&and(allClauses)) = false then
if nops([entryClauses()]) < 9*9 then
Display(Maplet(MessageDialog(`error`, "The current board is not solvable.")));
else
Display(Maplet(MessageDialog(`error`, "Sorry, the board was not filled correctly.")));
end if;
elif nops([entryClauses()]) < 9*9 then
Display(Maplet(MessageDialog(information, "The current board is solvable.")));
else
Display(Maplet(MessageDialog(information, "Congratulations, you finished the game.")));
gameOver := true;
end if;
end proc:
# Solve the current board state by calling MapleSAT
solveGame := proc()
global currentBoard;
global gameOver := true;
local allClauses, satisfyingAssignment, i, j, k, eq;
allClauses := atLeastOneDigit, atMostOneDigit, distinctnessConstraints, entryClauses();
satisfyingAssignment := Satisfy(&and(allClauses));
if satisfyingAssignment = NULL then
Display(Maplet(MessageDialog(`error`, "The current board is not solvable.")));
else
for eq in satisfyingAssignment do
if rhs(eq) then
i, j, k := op(lhs(eq));
currentBoard[i, j] := k;
end if;
end do;
end if;
refreshGrid();
end proc:
# Generate a new random game by calling MapleSAT
randomGame := proc()
global gameData;
local solutionEntries, i, j, k, cl, satisfyingAssignment, eq, hi, lo, mid, newData, allClauses;
local finishedGeneration := false;
while not finishedGeneration do
solutionEntries := Array(1..9, 1..9);
# Find a Sudoku grid completely filled with valid digits by calling MapleSAT with a random seed
allClauses := atLeastOneDigit, atMostOneDigit, distinctnessConstraints;
satisfyingAssignment := Satisfy(&and(allClauses), method="maplesat", solveroptions=[rnd_init_act=true,random_seed=floor(1000*time[real]())]);
for eq in satisfyingAssignment do
if rhs(eq) then
i, j, k := op(lhs(eq));
solutionEntries[i, j] := S[i, j, k];
end if;
end do;
# Fix a random ordering of the digits in the grid
solutionEntries := combinat:-randperm([entries(solutionEntries, nolist)]);
# Lower and upper bounds on how many digits we want to initially set
lo := 20;
hi := 80;
# Run MapleSAT a couple of times to find out approximately how many digits we need to initially set
for i from 1 to 3 do
mid := round((hi+lo)/2);
# Check if setting the first mid digits leads to a puzzle with a unique solution
if Satisfiable(&and(allClauses, map(`&or`, solutionEntries[1..mid])[], &or(map(`¬`, solutionEntries)[]))) then
lo := mid;
# If first attempt at finding a unique solution fails then start over
if i = 1 and hi = 80 then
break;
end if;
else
# Setting the first mid digits has a unique solution so decrease upper bound
hi := mid;
end if;
finishedGeneration := true;
end do;
end do;
# Set initial game data to the game generated by MapleSAT
newData := [seq([seq(0, j=1..9)], i=1..9)];
for cl in solutionEntries[1..hi] do
i, j, k := op(cl);
newData[i, j] := k;
end do;
gameData := newData;
restartGame();
end proc:
# Commands to draw the game play area and buttons
drawGame := proc()
return Worksheet(Table(widthmode=pixels, width=400, interior=none, exterior=none, alignment=center, hiddenborderdisplay=never, Row(Cell(Plot(identity = "boardPlot", showborders=false, clickaction="performClick()"), columnspan=3)), Row(Button("Restart", action="restartGame()"), Button("Check", action="checkGame()"), Button("Solve", action="solveGame()")), Row(Cell(), "New Game:", Cell()), Row(Button("Random", action="randomGame()"), Button("From File", action="loadGameFile()"), Button("From Web", action="loadGameWeb()"))));
end proc:
# Restart the game and redraw the grid
restartGame := proc()
global currentBoard := gameData;
global gameOver := false;
refreshGrid();
end proc:
# Procedure to run whenever the board is clicked on
performClick := proc()
global currentBoard, gameOver;
local i, j, k;
i := 10-floor(GetProperty(boardPlot, clicky));
j := floor(GetProperty(boardPlot, clickx));
# If the clicked square does not initially contain a digit then allow the player to edit the contents
if gameData[i, j] = 0 then
k := parse(Display(Maplet(BoxLayout(BoxColumn(seq(BoxRow(seq(BoxCell(Elements:-Button(cat("&", convert(j+3*i, string)), Shutdown(value=j+3*i))), j=1..3)), i=0..2), BoxRow(BoxCell(Elements:-Button("&Clear", Shutdown(value=0)))))))));
if type(k, integer) then
currentBoard[i, j] := k;
refreshGrid();
end if;
end if;
if gameOver = false and nops([entryClauses()]) = 9*9 then
checkGame();
end if;
end proc:
# Load a new game from a file with filename fn in Sudoku sdk format
readFile := proc(fn)
global gameData;
local i, j;
local ok := true;
local newData := [seq([seq(0, j=1..9)], i=1..9)];
local f := fopen(fn, READ);
local line := readline(f);
i := 1;
while line <> 0 do
if Length(line) <> 9 then
ok := false;
break;
end if;
for j from 1 to 9 do
if Ord(line[j]) >= Ord("1") and Ord(line[j]) <= Ord("9") then
newData[i, j] := parse(line[j]);
end if;
end do;
line := readline(f);
i := i+1;
end do;
fclose(f);
if ok then
gameData := newData;
restartGame();
end if;
end proc:
# Show a FileDialog to allow the player to select a Sudoku sdk file
loadGameFile := proc()
local fn;
fn := Display(Maplet(FileDialog[FD](filefilter="sdk", filterdescription="Sudoku sdk file", onapprove=Shutdown([FD]))));
if fn <> NULL then
readFile(op(fn));
end if;
end proc:
# Load a new game from the web
loadGameWeb := proc()
global gameData;
local status, data, headers;
status, data, headers := HTTP:-Get("https://sudoku-puzzles.herokuapp.com/board?difficulty=easy", timeout=100);
if status = 200 then
gameData := JSON:-ParseString(data)["board"];
restartGame();
else
Display(Maplet(MessageDialog(`error`, "Could not read game data from the web.")));
end if;
end proc:
# Generate plotting commands to draw the empty Sudoku grid
drawSudokuGrid := proc()
local i, j, squares, blocks;
squares := seq(seq(rectangle([i,j+1], [i+1,j], style=line, thickness=0), j=1..9), i=1..9);
blocks := seq(seq(rectangle([3*(i-1)+1,3*j+1], [3*i+1,3*(j-1)+1], thickness=2, color=`if`(type(i+j, even), "White", "LightGray")), j=1..3), i=1..3);
return squares, blocks;
end proc:
# Generate plotting commands to draw the digits
drawDigit := proc(i, j, k, given)
local colors := map(Color, [[0,0,255],[0,128,0],[255,0,0],[0,0,128],[128,0,0],[0,128,128],[0,0,0],[128,128,128],[128,128,0]]):
textplot([j+0.5, 10-i+0.5, k], font=[Arial, `if`(given, bold, roman), 18], color=colors[k]);
end proc:
# Draw the current state of the Sudoku game
refreshGrid := proc()
local digits, i, j, plotCommands;
digits := Array(1..9, 1..9):
for i from 1 to 9 do
for j from 1 to 9 do
if gameData[i, j] <> 0 then
digits[i, j] := drawDigit(i, j, gameData[i, j], true);
elif currentBoard[i, j] <> 0 then
digits[i, j] := drawDigit(i, j, currentBoard[i, j], false);
end if;
end do;
end do;
plotCommands := display(remove(x->x=0,[entries(digits, nolist)])[], drawSudokuGrid(), scaling=constrained, axes=none):
SetProperty(boardPlot, value, plotCommands, refresh=true);
SetProperty(boardPlot, clickdefault, true, refresh=true);
end proc:
# Start the game
InsertContent(drawGame()):
restartGame():<Text-field style="Heading 1" layout="Heading 1">Instructions</Text-field>Select "Yes" after opening the worksheet, or press the !!! button, to run the code to start the game (or see the "implementation details" to study and manually run the code).The Restart button clears the entries that were entered by the player.The Check button checks if it is possible to fill the remaining entries in a consistent way (every row, column, and block contains distinct digits).The Solve button fills the remaining entries in a consistent way if it is possible to do so. The check and solve functions are done by reducing the problem to SAT and calling Maple's built-in SAT solver as described in the "implementation details".The Random button randomly generates a new Sudoku puzzle with a unique solution. The generation is done using a SAT solver as described in the "implementation details".The From File button loads a new Sudoku puzzle from a Sudoku sdk file selected by the player.The From Web button loads a new Sudoku puzzle of easy difficulty using an online source.LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYjLUkjbWlHRiQ2I1EhRic=<Text-field style="Heading 1" layout="Heading 1">Implementation details</Text-field>The game uses Maple's plotting commands to draw the board, Maplets for the dialog boxes, and embedded components for the buttons.No knowledge of Sudoku solving or generation algorithms were used in the implementation. Instead, the rules of Sudoku were encoded into Boolean logic and Maple's built-in SAT solver was used to automatically generate and solve Sudoku puzzles. See the Satisfy command for more information about SAT solvers.The source code of the game may be viewed by executing the following line of code:DocumentTools:-SetProperty(InteractiveSudokuCode, visible, true):<Text-field style="Heading 2" layout="Heading 2">Encoding the rules of Sudoku</Text-field>To encode the rules of Sudoku in Boolean logic we use the Boolean variables LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUklbXN1YkdGJDYmLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUYjNiotRi82JlEiaUYnRjJGNUY4LUkjbW9HRiQ2LlEiLEYnRjUvRjlRJ25vcm1hbEYnLyUmZmVuY2VHRjcvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNy8lKnN5bW1ldHJpY0dGNy8lKGxhcmdlb3BHRjcvJS5tb3ZhYmxlbGltaXRzR0Y3LyUnYWNjZW50R0Y3LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRi82JlEiakYnRjJGNUY4RkAtRi82JlEia0YnRjJGNUY4RjJGNUY4LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJy8lJXNpemVHUSMxMkYnRjVGRA== with LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYuLUkjbW5HRiQ2JVEiMUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ25vcm1hbEYnLUkjbW9HRiQ2LlEmJmxlcTtGJ0YvRjIvJSZmZW5jZUdGMS8lKnNlcGFyYXRvckdGMS8lKXN0cmV0Y2h5R0YxLyUqc3ltbWV0cmljR0YxLyUobGFyZ2VvcEdGMS8lLm1vdmFibGVsaW1pdHNHRjEvJSdhY2NlbnRHRjEvJSdsc3BhY2VHUSwwLjI3Nzc3NzhlbUYnLyUncnNwYWNlR0ZJLUkjbWlHRiQ2JlEiaUYnLyUnaXRhbGljR1EldHJ1ZUYnRi8vRjNRJ2l0YWxpY0YnLUY2Ni5RIixGJ0YvRjJGOS9GPEZSRj1GP0ZBRkNGRS9GSFEmMC4wZW1GJy9GS1EsMC4zMzMzMzMzZW1GJy1GTTYmUSJqRidGUEYvRlNGVS1GTTYmUSJrRidGUEYvRlNGNS1GLDYlUSI5RidGL0YyLyUlc2l6ZUdRIzEyRidGL0Yy to denote that the square at LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB contains the digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic=.The rules of Sudoku state that each square must be filled with a digit between 1 and 9 and that the same digit cannot appear twice in the same row, column, or block. The first constraint has the form LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYvLUklbXN1YkdGJDYmLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUYjNiotRi82JlEiaUYnRjJGNUY4LUkjbW9HRiQ2LlEiLEYnRjUvRjlRJ25vcm1hbEYnLyUmZmVuY2VHRjcvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNy8lKnN5bW1ldHJpY0dGNy8lKGxhcmdlb3BHRjcvJS5tb3ZhYmxlbGltaXRzR0Y3LyUnYWNjZW50R0Y3LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRi82JlEiakYnRjJGNUY4RkAtSSNtbkdGJDYlUSIxRidGNUZERjJGNUY4LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJy1GQTYuUSYmdmVlO0YnRjVGREZGL0ZJRjdGSkZMRk5GUEZSL0ZVUSwwLjE2NjY2NjdlbUYnL0ZYRmZvLUYsNiZGLi1GIzYqRj1GQEZaRkAtRmhuNiVRIjJGJ0Y1RkRGMkY1RjhGW29GXm9GYW8tRkE2LlEnJnNkb3Q7RidGNUZERkZGZG9GSkZMRk5GUEZSRlQvRlhGVkZfcEZfcEZhby1GLDYmRi4tRiM2KkY9RkBGWkZALUZobjYlUSI5RidGNUZERjJGNUY4RltvRl5vLUYvNiNRIUYnLyUlc2l6ZUdRIzEyRidGNUZE for each LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYsLUkjbW5HRiQ2JVEiMUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ25vcm1hbEYnLUkjbW9HRiQ2LlEmJmxlcTtGJ0YvRjIvJSZmZW5jZUdGMS8lKnNlcGFyYXRvckdGMS8lKXN0cmV0Y2h5R0YxLyUqc3ltbWV0cmljR0YxLyUobGFyZ2VvcEdGMS8lLm1vdmFibGVsaW1pdHNHRjEvJSdhY2NlbnRHRjEvJSdsc3BhY2VHUSwwLjI3Nzc3NzhlbUYnLyUncnNwYWNlR0ZJLUkjbWlHRiQ2JlEiaUYnLyUnaXRhbGljR1EldHJ1ZUYnRi8vRjNRJ2l0YWxpY0YnLUY2Ni5RIixGJ0YvRjJGOS9GPEZSRj1GP0ZBRkNGRS9GSFEmMC4wZW1GJy9GS1EsMC4zMzMzMzMzZW1GJy1GTTYmUSJqRidGUEYvRlNGNS1GLDYlUSI5RidGL0YyLyUlc2l6ZUdRIzEyRidGL0Yy and the second constraint has the form LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYqLUklbXN1YkdGJDYmLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUYjNiotRi82JlEiaUYnRjJGNUY4LUkjbW9HRiQ2LlEiLEYnRjUvRjlRJ25vcm1hbEYnLyUmZmVuY2VHRjcvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNy8lKnN5bW1ldHJpY0dGNy8lKGxhcmdlb3BHRjcvJS5tb3ZhYmxlbGltaXRzR0Y3LyUnYWNjZW50R0Y3LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRi82JlEiakYnRjJGNUY4RkAtRi82JlEia0YnRjJGNUY4RjJGNUY4LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJy1GQTYuUSomSW1wbGllcztGJ0Y1RkRGRi9GSUY3L0ZLRjRGTEZORlBGUi9GVVEsMC4yNzc3Nzc4ZW1GJy9GWEZmby1GQTYuUSJ+RidGNUZERkZGY29GSkZMRk5GUEZSRlQvRlhGVi1GQTYuUSYmbm90O0YnRjVGREZGRmNvRkpGTEZORlBGUkZURmdvLUYsNiZGLi1GIzYsRj0tRkE2LlEiJ0YnRjVGREZGRmNvRkpGTEZORlBGUi9GVVEsMC4xMTExMTExZW1GJ0ZbcEZARlpGY3BGQEZnbkYyRjVGOEZqbkZdby8lJXNpemVHUSMxMkYnRjVGRA== where LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzY0LUkjbW5HRiQ2JVEiMUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ25vcm1hbEYnLUkjbW9HRiQ2LlEmJmxlcTtGJ0YvRjIvJSZmZW5jZUdGMS8lKnNlcGFyYXRvckdGMS8lKXN0cmV0Y2h5R0YxLyUqc3ltbWV0cmljR0YxLyUobGFyZ2VvcEdGMS8lLm1vdmFibGVsaW1pdHNHRjEvJSdhY2NlbnRHRjEvJSdsc3BhY2VHUSwwLjI3Nzc3NzhlbUYnLyUncnNwYWNlR0ZJLUkjbWlHRiQ2JlEiaUYnLyUnaXRhbGljR1EldHJ1ZUYnRi8vRjNRJ2l0YWxpY0YnLUY2Ni5RIixGJ0YvRjJGOS9GPEZSRj1GP0ZBRkNGRS9GSFEmMC4wZW1GJy9GS1EsMC4zMzMzMzMzZW1GJy1GTTYmUSJqRidGUEYvRlNGVUZMLUY2Ni5RIidGJ0YvRjJGOUY7Rj1GP0ZBRkNGRS9GSFEsMC4xMTExMTExZW1GJy9GS0ZaRlVGZ25Gam5GVS1GTTYmUSJrRidGUEYvRlNGNS1GLDYlUSI5RidGL0YyLyUlc2l6ZUdRIzEyRidGL0Yy and LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNiotSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSInRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGOS8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSwwLjExMTExMTFlbUYnLyUncnNwYWNlR1EmMC4wZW1GJy1GPjYuUSIsRidGN0ZBRkMvRkZGNkZHRklGS0ZNRk8vRlJGVi9GVVEsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjpGPS8lJXNpemVHUSMxMkYnRjdGQUY3RkFGW29GN0ZB does not equal LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB but is in the same row, column, or block as LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB.<Text-field style="Heading 2" layout="Heading 2">The Check and Solve implementations</Text-field>In addition to the constraints encoding the rules of Sudoku, the Check and Solve implementations call the SAT solver with the unit clauses LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUklbXN1YkdGJDYmLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUYjNiotRi82JlEiaUYnRjJGNUY4LUkjbW9HRiQ2LlEiLEYnRjUvRjlRJ25vcm1hbEYnLyUmZmVuY2VHRjcvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNy8lKnN5bW1ldHJpY0dGNy8lKGxhcmdlb3BHRjcvJS5tb3ZhYmxlbGltaXRzR0Y3LyUnYWNjZW50R0Y3LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRi82JlEiakYnRjJGNUY4RkAtRi82JlEia0YnRjJGNUY4RjJGNUY4LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJy8lJXNpemVHUSMxMkYnRjVGRA== where the square at LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB contains the digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= in the current board's state.The Check implementation just calls Satisfiable to determine if some solution exists. The Solve implementation calls Satisfy and if a satisfying assignment is found then for each LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUklbXN1YkdGJDYmLUkjbWlHRiQ2JlEiU0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLUYjNiotRi82JlEiaUYnRjJGNUY4LUkjbW9HRiQ2LlEiLEYnRjUvRjlRJ25vcm1hbEYnLyUmZmVuY2VHRjcvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNy8lKnN5bW1ldHJpY0dGNy8lKGxhcmdlb3BHRjcvJS5tb3ZhYmxlbGltaXRzR0Y3LyUnYWNjZW50R0Y3LyUnbHNwYWNlR1EmMC4wZW1GJy8lJ3JzcGFjZUdRLDAuMzMzMzMzM2VtRictRi82JlEiakYnRjJGNUY4RkAtRi82JlEia0YnRjJGNUY4RjJGNUY4LyUvc3Vic2NyaXB0c2hpZnRHUSIwRicvSSttc2VtYW50aWNzR0YkUSdhdG9taWNGJy8lJXNpemVHUSMxMkYnRjVGRA== that has been assigned to true the square at LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkobWZlbmNlZEdGJDYlLUYjNigtSSNtaUdGJDYmUSJpRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSIsRidGNy9GO1Enbm9ybWFsRicvJSZmZW5jZUdGOS8lKnNlcGFyYXRvckdGNi8lKXN0cmV0Y2h5R0Y5LyUqc3ltbWV0cmljR0Y5LyUobGFyZ2VvcEdGOS8lLm1vdmFibGVsaW1pdHNHRjkvJSdhY2NlbnRHRjkvJSdsc3BhY2VHUSYwLjBlbUYnLyUncnNwYWNlR1EsMC4zMzMzMzMzZW1GJy1GMTYmUSJqRidGNEY3RjovJSVzaXplR1EjMTJGJ0Y3RkFGN0ZBRlpGN0ZB is filled with the digit LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEia0YnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic=.<Text-field style="Heading 2" layout="Heading 2">The Random implementation</Text-field>The Random implementation begins by calling the SAT solver with the clauses encoding the rules of Sudoku but no clauses encoding the starting configuration. The result produced by the SAT solver gives a completed Sudoku grid LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEiUkYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= (a random seed is passed to the SAT solver so that a different LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEiUkYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= is produced each time). A random ordering of the entries is generated and the first 50 entries are selected as the potential starting configuration of a Sudoku puzzle. This puzzle has the solution LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEiUkYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= by construction, though other solutions may also exist.To verify that the generated solution is unique, we re-run the SAT solver with the additional 50 unit clauses corresponding to the starting configuration along with the constraint LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYpLUklbXN1YkdGJDYmLUkjbW9HRiQ2L1ElJm9yO0YnLyUlc2l6ZUdRIzI2RicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1Enbm9ybWFsRicvJSZmZW5jZUdGNy8lKnNlcGFyYXRvckdGNy8lKXN0cmV0Y2h5R1EldHJ1ZUYnLyUqc3ltbWV0cmljR0Y3LyUobGFyZ2VvcEdGNy8lLm1vdmFibGVsaW1pdHNHRjcvJSdhY2NlbnRHRjcvJSdsc3BhY2VHUSwwLjIyMjIyMjJlbUYnLyUncnNwYWNlR0ZMLUYjNiktSSNtaUdGJDYmUSJSRicvJSdpdGFsaWNHRkFGNS9GOVEnaXRhbGljRictSShtZmVuY2VkR0YkNictRiM2KC1GUjYmUSJpRidGVUY1RlctRi82LlEiLEYnRjVGOEY7L0Y+RkEvRkBGN0ZCRkRGRkZIL0ZLUSYwLjBlbUYnL0ZOUSwwLjMzMzMzMzNlbUYnLUZSNiZRImpGJ0ZVRjVGV0ZVRjVGV0Y1RjgvJSVvcGVuR1EiW0YnLyUmY2xvc2VHUSJdRictRi82LlEiPUYnRjVGOEY7Rj1GX29GQkZERkZGSC9GS1EsMC4yNzc3Nzc4ZW1GJy9GTkZhcC1GUjYmUSJrRidGVUY1RldGVUY1RlcvJS9zdWJzY3JpcHRzaGlmdEdRIjBGJy9JK21zZW1hbnRpY3NHRiRRJ2F0b21pY0YnLUYvNi5RIn5GJ0Y1RjhGO0Y9Rl9vRkJGREZGRkhGYG8vRk5GYW8tRi82LlEmJm5vdDtGJ0Y1RjhGO0Y9Rl9vRkJGREZGRkhGYG9GYnAtRiw2Ji1GUjYmUSJTRidGVUY1RlctRiM2KkZobkZbb0Zkb0Zbb0ZjcEZVRjVGV0ZmcEZpcC9GM1EjMTJGJ0Y1Rjg= which blocks the solution LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEiUkYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic=. If the SAT solver returns another solution then we start over and find a new LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEiUkYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= to try. Otherwise the first 50 entries of LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEiUkYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic= form a legal Sudoku puzzle.Additionally, it may be the case that we could use fewer than 50 entries and still obtain a Sudoku puzzle with a unique solution. To estimate how many entries we need to assign using only a few extra calls to the SAT solver we define LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYoLUkjbWlHRiQ2JlEjbG9GJy8lJ2l0YWxpY0dRJXRydWVGJy8lK2V4ZWN1dGFibGVHUSZmYWxzZUYnLyUsbWF0aHZhcmlhbnRHUSdpdGFsaWNGJy1JI21vR0YkNi5RKiZjb2xvbmVxO0YnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EsMC4yNzc3Nzc4ZW1GJy8lJ3JzcGFjZUdGTi1JI21uR0YkNiVRIzIwRidGMkY8LyUlc2l6ZUdRIzEyRidGMkY8, LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYoLUkjbWlHRiQ2JlEjaGlGJy8lJ2l0YWxpY0dRJXRydWVGJy8lK2V4ZWN1dGFibGVHUSZmYWxzZUYnLyUsbWF0aHZhcmlhbnRHUSdpdGFsaWNGJy1JI21vR0YkNi5RKiZjb2xvbmVxO0YnRjIvRjZRJ25vcm1hbEYnLyUmZmVuY2VHRjQvJSpzZXBhcmF0b3JHRjQvJSlzdHJldGNoeUdGNC8lKnN5bW1ldHJpY0dGNC8lKGxhcmdlb3BHRjQvJS5tb3ZhYmxlbGltaXRzR0Y0LyUnYWNjZW50R0Y0LyUnbHNwYWNlR1EsMC4yNzc3Nzc4ZW1GJy8lJ3JzcGFjZUdGTi1JI21uR0YkNiVRIzUwRidGMkY8LyUlc2l6ZUdRIzEyRidGMkY8, LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYpLUkjbWlHRiQ2JlEkbWlkRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRictSSNtb0dGJDYuUSomY29sb25lcTtGJ0YyL0Y2USdub3JtYWxGJy8lJmZlbmNlR0Y0LyUqc2VwYXJhdG9yR0Y0LyUpc3RyZXRjaHlHRjQvJSpzeW1tZXRyaWNHRjQvJShsYXJnZW9wR0Y0LyUubW92YWJsZWxpbWl0c0dGNC8lJ2FjY2VudEdGNC8lJ2xzcGFjZUdRLDAuMjc3Nzc3OGVtRicvJSdyc3BhY2VHRk4tRiw2JlEmcm91bmRGJy9GMEY0RjJGPC1JKG1mZW5jZWRHRiQ2JS1GIzYoLUZWNiUtRiM2KC1GLDYmUSNsb0YnRi9GMkY1LUY5Ni5RIitGJ0YyRjxGPkZARkJGREZGRkhGSi9GTVEsMC4yMjIyMjIyZW1GJy9GUEZfby1GLDYmUSNoaUYnRi9GMkY1LyUlc2l6ZUdRIzEyRidGMkY8RjJGPC1GOTYuUSIvRidGMkY8Rj5GQC9GQ0YxRkRGRkZIRkovRk1RLDAuMTY2NjY2N2VtRicvRlBGXHAtSSNtbkdGJDYlUSIyRidGMkY8RmRvRjJGPEYyRjxGZG9GMkY8 and repeat the last step except using only the first LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEkbWlkRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRicvJSVzaXplR1EjMTJGJ0YyL0Y2USdub3JtYWxGJw== entries of LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEiUkYnLyUnaXRhbGljR1EldHJ1ZUYnLyUrZXhlY3V0YWJsZUdRJmZhbHNlRicvJSxtYXRodmFyaWFudEdRJ2l0YWxpY0YnLyUlc2l6ZUdRIzEyRidGMi9GNlEnbm9ybWFsRic=. If the resulting SAT instance is satisfiable then we need to use more than LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEkbWlkRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRicvJSVzaXplR1EjMTJGJ0YyL0Y2USdub3JtYWxGJw== entries to ensure a unique solution and if the resulting SAT instance is unsatisfiable then we can perhaps use fewer than LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEkbWlkRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRicvJSVzaXplR1EjMTJGJ0YyL0Y2USdub3JtYWxGJw== entries. Either way we improve the bounds on how many entries to assign (in the former case we can update LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEjbG9GJy8lJ2l0YWxpY0dRJXRydWVGJy8lK2V4ZWN1dGFibGVHUSZmYWxzZUYnLyUsbWF0aHZhcmlhbnRHUSdpdGFsaWNGJy8lJXNpemVHUSMxMkYnRjIvRjZRJ25vcm1hbEYn to LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEkbWlkRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRicvJSVzaXplR1EjMTJGJ0YyL0Y2USdub3JtYWxGJw== and in the latter case we can update LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEjaGlGJy8lJ2l0YWxpY0dRJXRydWVGJy8lK2V4ZWN1dGFibGVHUSZmYWxzZUYnLyUsbWF0aHZhcmlhbnRHUSdpdGFsaWNGJy8lJXNpemVHUSMxMkYnRjIvRjZRJ25vcm1hbEYn to LUklbXJvd0c2Iy9JK21vZHVsZW5hbWVHNiJJLFR5cGVzZXR0aW5nR0koX3N5c2xpYkdGJzYmLUkjbWlHRiQ2JlEkbWlkRicvJSdpdGFsaWNHUSV0cnVlRicvJStleGVjdXRhYmxlR1EmZmFsc2VGJy8lLG1hdGh2YXJpYW50R1EnaXRhbGljRicvJSVzaXplR1EjMTJGJ0YyL0Y2USdub3JtYWxGJw==) and this step can be repeated a few times to find more precise bounds on how many entries need to be assigned to ensure a unique solution exists.JSFH