\myheading{Minesweeper}

\leveldown{}

\input{equations/minesweeper/1_SMT/main_EN.tex}
\input{equations/minesweeper/2_SAT/main_EN.tex}
\input{equations/minesweeper/3_SMT_opt/main_EN.tex}
\input{equations/minesweeper/4_Knuth/main_EN.tex}
\input{equations/minesweeper/5_SAT_SN/main_EN.tex}
\input{equations/minesweeper/6_brute/main_EN.tex}

\myheading{More theory}

In Numb3rs TV series, Dr.Charlie Eppes tried to solve "Minesweeper game":
\url{https://en.wikipedia.org/wiki/Uncertainty_Principle_(Numbers)},
\url{http://pi.math.cornell.edu/~numb3rs/luthy/num104.html}.

What he is tried to do, is to find faster/better way to solve this game, by finding better methods to solve NP-problems in general.

Solving Minesweeper is NP-complete:
\url{http://simon.bailey.at/random/kaye.minesweeper.pdf},
\url{http://web.mat.bham.ac.uk/R.W.Kaye/minesw/ordmsw.htm},
\url{http://web.mat.bham.ac.uk/R.W.Kaye/minesw/ASE2003.pdf},
\url{http://math.oregonstate.edu/~math_reu/proceedings/REU_Proceedings/Proceedings2003/2003MK.pdf}.

Our way to solve it is also called "Minesweeper Consistency Problem"
\footnote{\url{https://www.claymath.org/sites/default/files/minesweeper.pdf}}.
We did it using system of integer equation.
And solving system of integer equation is NP-complete as well.

Find better way to solve Minesweeper, and you probably will be able to solve other NP-problems!

\myheading{Further reading}

Proofsweeper -- Play Minesweeper by formally proving your moves in Idris: \url{https://github.com/A1kmm/proofsweeper}.

Raphaël Collet -- PlayingtheMinesweeperwithConstraints: \url{https://www.info.ucl.ac.be/~pvr/minesweeper.pdf}.

\levelup{}