In this video we translate this code for checking a solution described by a function s :: Int -> Int -> Int -> Bool into an expression in our language of Forms.

This form uses 729 propositional letters Si,j,k, where i,j,k are numbers in [1..9].

The idea is that the way the Sudoku puzzle is filled in corresponds to a valuation of these letters: the value of Si,j,k is True iff k is written in square i,j, and the rules are obeyed iff this valuation satisfies the Form.

So to solve a sudoku puzzle we need only to find a valuation that for each of the initial entries given in the puzzle, makes the corresponding Si,j,k True, and satisfies the Formthat expresses the rules.