‹ BackHN Continuity

Thread

Solving a corn puzzle with CP-SAT

37 points · 20 comments · luu

  1. sashank_1509 · · focus · HN ↗
    Ok, in this specific case, a puzzle with what 10 pieces, a recursive backtracker will be just as fast and more importantly, be far easier to reason about and implement.

    If this was a thousand piece puzzle, I would still venture recursive backtracker with good heuristics will beat CP-SAT, even in the sudoku case some good heuristics with backtracking beats CP-SAT. Not sure why Claude immediately jumped to using CP-SAT.

    1. CJefferson · · focus · HN ↗
      I would be shocked if a good recursive backtracker could beat a good SAT solver for large problems. I mean, if you could solve SAT with recursive backtracking people would. That is the core of a SAT or CP solver, with the all the extra clever stuff.

      I've spent significant chunks of my career help people throw away backtracking searchers people polished over years with a CP-SAT model I threw together in 30 minutes, often much to their upset.

      You can for Sudoku often beat a CP-SAT solver, but that's because the problems are trivial and take milliseconds. If you look at more difficult Sudoku variants, or 16x16 grids, backtracking solvers start to fall behind.

      1. taeric · · focus · HN ↗
        Agreed. I don't know if I would be shocked, but I would be surprised.

        This is one that is hard for people to really internalize, I think? The SAT solvers many are likely to use today are not at all the same as the ones they would have used 20 years ago. They have made some amazing advances in how to approach those problems.

        There are also probably some very poorly conceived models that people use to adapt a problem to some of these solvers.

      2. anitil · · focus · HN ↗
        I'm new to solvers and have only used them in anger exactly once, but during my research it seemed that the received wisdom is that hand-rolled solutions were typically faster, so this is a surprise to me. I suppose in the same sense that 'you can write assembly better than the compiler if you really want', which is probably also mostly false these days.

        Do you have examples that are public or that you can talk about?

    2. shoo · · focus · HN ↗
      Would writing a recursive backtracker really be easier to reason about and implement?

      With one of these solver-based approaches, you encode the problem with decision variables in some fashion, state all the constraints & call solve. There's some art & experience in how to encode & model the problem, but the specification of the model & the problem is fairly declarative.

      What's great about general purpose solver-based approaches is that its usually faster (in terms of implementation time & effort) to start getting solutions & they're also much more robust to changes in requirements & the problem statement. That's less of a concern in this toy example, where the problem is small, well-defined & unambiguous, but in a real business/industrial application, the problem statement often changes considerably over time.

      I agree that the performance & behaviour of a black box solver may be much harder to reason about than something you custom build by hand & know inside out, but if the general purpose black box solver is 'good enough' for the distributions of problem instances it needs to process, then there's no need to custom-build anything. Throw the black box solver at it -- job's done, and you're left with something that's both quite readable (declarative modelling of the problem, particularly if someone documents the formulation - the meaning of all the decision variables, index sets, constraints, objective terms etc) & flexible to future change.

      Custom solvers & heuristics can sometimes be much, much more effective in being able to scale and solve industrial-scale problems, but usually at the expense of being much more effort to set up in the first place, and very fragile to changes in requirements -- if you learn something a few weeks into a project that perturbs the problem statement, maybe it wrecks the particular mathematical structure you were relying upon for a custom solver/heuristic, so you need to chuck out all your work & go back to the drawing board.

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.