CODEWITHSUNDEEP
z3smtsat
hjfreyer
hjfreyer

Reputation: 569

Modeling crossword-construction in z3

I'm working on a program to generate crossword puzzles. The task is: given a grid, is there a way to fill the grid with letters such that each clue (acrosses and downs) is a valid word?

This can be pretty naturally reduced to boolean satisfiablity - have booleans for "does $LETTER appear at $ROW, $COL?" and "is $WORD the answer to $CLUE?", and then add constraints between the two sets of booleans. I've had some success modeling it this way with SAT solvers.

I've been wondering if I can get better results with the richer API that z3 provides, but I feel like I'm holding it wrong. I've started by attempting to replicate the SAT approach (a bunch of Bools and assertions), but just creating the O(10k) constraint clauses takes around 15 minutes, never mind actually solving it. I've tried using both the Python and Rust bindings with the same results. For comparison's sake, varisat (a less mature SAT-solver written in Rust) does the loading and the solving in well under a second.

Is there a better way to programmatically specify this many constraints? Is there a better way of modeling this problem for z3? Is this just not the kind of thing z3 is good at?

Upvotes: 0

Views: 161

Answers (1)

alias
alias

Reputation: 30525

Did you see https://bohlender.pro/blog/generating-crosswords-with-sat-smt/?

It’s hard to opine without seeing your exact program. But looks like the above blog has a good handle on this problem. Reading through it and asking specific questions would be more suitable in the stack overflow context.

Upvotes: 0

Related Questions