Message Boards Message Boards

Chess queen armies with SAT solvers

Christopher Wolfram, WOLFRAM
Posted 1 year ago

Thumbnail

Also available online at https://christopherwolfram.com/projects/queen-armies/
POSTED BY: Christopher Wolfram
7 Replies
Sort By:

Yes, of course there's some variance to be expected, but typically I've seen a fairly constant rate of results generation. The "proving completion" effect at the end of a calculation is very startling and easy to notice because the time lag can be orders of magnitude larger than anything else seen in the computation thus far. An annoying drawback of trying to use this method for larger searches...
POSTED BY: Brad Klee

Hi Christopher. I wonder if you've noticed the following behavior: The SAT solver is ticking along at a normal pace, finding more and more results, maybe in parallel, maybe not. After finding all results to a particular problem, it hangs for a noticeable amount of time trying to find more solutions that don't exist. This may have just happened to me again on another calculation about Cellular Automata. I don't know if it's a bug, or is it just an unavoidable consequence of SAT difficulty? Is it more difficult to show that no additional solutions exist than to find one that does? Any thoughts? --Brad

POSTED BY: Brad Klee

I think this is just a property of DPLL. Just because it found one solution quickly, doesn't mean that it will find the next one quickly because it may have to do significant backtracking. It probably depends a lot on your usage though.
POSTED BY: Christopher Wolfram

enter image description here -- you have earned Featured Contributor Badge enter image description here Your exceptional post has been selected for our editorial column Staff Picks http://wolfr.am/StaffPicks and Your Profile is now distinguished by a Featured Contributor Badge and is displayed on the Featured Contributor Board. Thank you!
POSTED BY: Moderation Team

Thanks for sharing! Looks very nice and performant! I was wondering: how do these SAT solvers work under-the-hood? Is this also not similar to some recursive backtracking algorithm? Or do these fundamentally work differently? by leveraging some matrix algebra or polynomial solving or …?

Btw: The images show up a bit strange on this website:

enter image description here

but they show up fine on your own website.
POSTED BY: Sander Huisman

About the images: That appears to be a bug in ArrayPlot rendering for cloud notebooks in Safari. I've reported it.

About SAT Solvers: Most SAT solvers (including the built-in one) use something called the DPLL algorithm, which does use recursive backtracking in the end. However, there are some very nice ways that it can 1) prune and 2) rank possible branches that make it very efficient. (It also helps that there are highly optimized implementations too.) The core DPLL algorithm is actually quite simple and elegant though.
POSTED BY: Christopher Wolfram

I see, that's what I thought. I was actually thinking of doing the branching also a bit smarter; basically rank the cells by their 'influence/importance' such that the pruning is faster. But it can't beat any compiled sat solver likely :-)
POSTED BY: Sander Huisman
Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Tag limit exceeded
Note: Only the first five people you tag will receive an email notification; the other tagged names will appear as links to their profiles.
Reply Preview
Attachments
Remove
or Discard

Group Abstract Group Abstract