3 ms·

But the context of OP is for human-scale puzzles.

• Jtsummers 3y ago
  Human-scale puzzles can still have search spaces in the billions and trillions and beyond. You want a SAT/SMT solver that can reduce the search space rapidly or a constraint propagation system that can similarly reduce the search space if you code up solutions to them.
  • kazinator 3y ago
    That depends; do you want to figure out how to solve the puzzle programmatically from scratch, or do you want to study how to apply/integrate SAT or constraint propagation systems. Equally valid. Ad hoc brute force searches can be informed by constraint checking. Like if you're laying blocks into a box or something, your brute force search rejects placements that stick outside of the box. I think "logic problems" may be referring to to those problems that tell you Bob is Alice's neighbor, and Jack plays piano, and, ..., and so then who owns the horse? We can identify all the propositions, round up their Boolean variables, and test. I've never seen a problem like this approach anywhere near 32 variables.