\myheading{Crossword generator}

\renewcommand{\CURPATH}{puzzles/cross}

We assign an integer to each character in crossword, it reflects ASCII code of it.

Then we enumerate all possible horizontal/vertical ``sticks'' longer than 1 and assign words to them.

For example, there is a horizontal stick of length 3.
And we have such 3-letter words in our dictionary: ``the'', ``she'', ``xor''.

We add the following constraint:

\begin{lstlisting}
Or(
	And(chars[X][Y]=='t', chars[X][Y+1]=='h', chars[X][Y+2]=='e'),
	And(chars[X][Y]=='s', chars[X][Y+1]=='h', chars[X][Y+2]=='e'),
	And(chars[X][Y]=='x', chars[X][Y+1]=='o', chars[X][Y+2]=='r'))
\end{lstlisting}

One of these words would be chosen automatically.

Index of each word is also considered, because duplicates are not allowed.

Sample pattern:

\begin{lstlisting}
**** **********
 * * *  * * * *
***************
 * * *  * * * *
********* *****
 * * * * * *  *
****** ********
   * * * * *   
******** ******
*  * * * * * * 
***** *********
* * * *  * * * 
***************
* * * *  * * * 
********** ****
\end{lstlisting}

Sample result:

\begin{lstlisting}
spur stimulated
 r e c  i a h e
congratulations
 m u t  a i s c
violation niece
 s a e p e n  n
rector penitent
   i i o c e
accounts herald
s  n g e a r o
press edinburgh
e x e n  t p i
characteristics
t c l r  n e a
satisfying dull

horizontal:
((0, 0), (0, 3)) spur
((0, 5), (0, 14)) stimulated
((2, 0), (2, 14)) congratulations
((4, 0), (4, 8)) violation
((4, 10), (4, 14)) niece
((6, 0), (6, 5)) rector
((6, 7), (6, 14)) penitent
((8, 0), (8, 7)) accounts
((8, 9), (8, 14)) herald
((10, 0), (10, 4)) press
((10, 6), (10, 14)) edinburgh
((12, 0), (12, 14)) characteristics
((14, 0), (14, 9)) satisfying
((14, 11), (14, 14)) dull
vertical:
((8, 0), (14, 0)) aspects
((0, 1), (6, 1)) promise
((10, 2), (14, 2)) exact
((0, 3), (10, 3)) regulations
((10, 4), (14, 4)) seals
((0, 5), (9, 5)) scattering
((10, 6), (14, 6)) entry
((4, 7), (10, 7)) opposed
((0, 8), (4, 8)) milan
((5, 9), (14, 9)) enchanting
((0, 10), (4, 10)) latin
((4, 11), (14, 11)) interrupted
((0, 12), (4, 12)) those
((8, 13), (14, 13)) logical
((0, 14), (6, 14)) descent
\end{lstlisting}

\textit{Unsat} is possible if the dictionary is too small or have no words of length present in pattern.

Constructing a crossword puzzle by bruteforce is not feasible, especially in the presence of big dictionary.

The source code:

\lstinputlisting[style=custompy]{\CURPATH/cross_Z3.py}

The files, including my dictionary: \url{\RepoURL/\CURPATH}.

Further work: rewrite it to SAT, because it's too slow.