Solving newspaper puzzles with SMT solvers

[HugoPeters1024]

https://hugopeters.me/posts/15/

[LeventErkok]

Nice example.. I was able to code the same in SBV, which provides a much higher-level interface to SMT solvers. It also avoids multiple calls to the solver, since we can let the solver decide if j should be an integer or a boolean, and also easily ask for multiple-solutions. (Turns out the solution is unique in this case.) Here's the SBV solution, in case anyone is interested in comparing/contrasting the encodings: https://github.com/LeventErkok/sbv/blob/master/Documentation/SBV/Examples/Puzzles/Newspaper.hs

(To be clear, I think z3 bindings themselves are fantastic and there are use cases it addresses well. But SBV can be a good choice since it provides abstractions that makes symbolic programming much closer to Haskell programs then to SMTLib abstractions.)

[HugoPeters1024]

@LeventErkok Nice example.. I was able to code the same in SBV, which provides a much higher-level interface to SMT solvers. It also avoids multiple calls to the solver, since we can let the solver decide if j should be an integer or a boolean, and also easily ask for multiple-solutions. (Turns out the solution is unique in this case.) Here's the SBV solution, in case anyone is interested in comparing/contrasting the encodings: https://github.com/LeventErkok/sbv/blob/master/Documentation/SBV/Examples/Puzzles/Newspaper.hs

(To be clear, I think z3 bindings themselves are fantastic and there are use cases it addresses well. But SBV can be a good choice since it provides abstractions that makes symbolic programming much closer to Haskell programs then to SMTLib abstractions.)

Wow! That looks 10x more elegant than my code haha. (I didn't properly remember how much of a mess to read it was). I will definitely be checking out that package for future SMT projects. Thanks for reading :)

[FredGannett]

Filled my boots writing perl to convert newspaper puzzles into SMT-Lib grammers during lockdown. A welcome distraction that resulted in this blog https://puzzlesolvingsmtstyle.blogspot.com covering Gogen, Hidato, Sudoku ( esp the big ones ), Kakuro etc. Even managed a "Queens social distancing problem" incarnation and minesweeper ( the paper version ). There are certain types of problems that convert into SMT language very well but others are a harder twist. Currently looking at tiling problems but the combination of solving for placement order and matching rotation for edges seems unsolvable beyond a few tiles.