Hacker News new | comments | show | ask | jobs | submit login

One thing to try, especially with Glucose: turn off the preprocessing. The preprocessing seems to help with really "hard" instances like you see in SAT competitions, but takes time and doesn't really help with simpler ones.

We use SAT solvers extensively in the Phil[0] crossword construction tool, to figure out when the grid is overconstrained, and which letters have only a single value in all possible solutions. We ended up running Glucose (compiled to wasm and running in the browser) because the simpler solvers couldn't solve many instances quickly, and with preprocessing off but most other parameters at their defaults. I didn't do a careful evaluation of all solvers, but it might be interesting.

I really need to write this stuff up.

[0]: https://github.com/keiranking/Phil




Applications are open for YC Winter 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: