How can Synopsys VC Formal solve Sudoku puzzles?

[unixdaemon]

Synopsys and Intel posted the challenge to solve Sudoku puzzles using the VC Formal software.
They say that at Intel they use Sudoku puzzles to train formal verification engineers.

I am a little familiar with VC Formal: it can analyze Verilog code and find issues like arithmetic overflows, deadlocks, livelocks.

But I don't understand how can VC Formal be used to solve Sudoku puzzles.

Any hints?

 

[dvmonkey]

By writing constraints (assume property) and assertions (assert property), one can find a solution to Sudoku.

In dynamic simulation you can write SVTB constraints to do the same.