‹ BackHN Continuity

Thread

Solving a corn puzzle with CP-SAT

37 points · 20 comments · luu

  1. csense · · focus · HN ↗
    Reinventing the wheel is not always to be avoided. Finding an interesting wheel and trying to build your own equivalent can be an excellent way to improve your skills as a programmer [1].

    "Feed it to SAT solver" is a super useful technique every seasoned programmer should have in their toolbelt.

    If you want to improve your programming skill, I suggest implementing your own version of these two interesting, satisfying algorithms:

    - DPLL, the classic general-purpose SAT solving algorithm [3].

    - Algorithm X (aka Dancing Links), Knuth's super elegant search algorithm for solving exact cover problems [4] [5].

    You're not going to build something that beats CaDiCaL [6] in an afternoon, but writing your own implementation of these algorithms will teach you a lot, and a reasonable time investment will get you to a pretty satisfying endpoint of having a practical solver for your favorite application (Sudoku, polyomino packing, etc.)

    [1] Reinventing wheels is not a bad way to spend your days at a retreat focusing on one's personal growth as a programmer. "I think I'll learn a lot and get some good practice at programming and algorithmic thinking" is an easy bar to meet.

    In a professional context, telling your company or client they should commit scarce, expensive engineering resources (e.g. your time) to creating and maintaining their own wheel design requires justification [2].

    [2] "Don't reinvent wheels" is good general advice for junior developers. Senior developers know that sometimes there are specific situations where this general advice doesn't apply. For example, if no existing wheels meet your application's requirements, or if you have ideas for proprietary features that give you a competitive advantage. Even in a professional setting, reinventing the wheel isn't always a bad idea; you just need to meet a much higher bar to justify the commitment of resources.

    [3] <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;DPLL_algorithm" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;DPLL_algorithm

    [4] <a href="https:&#x2F;&#x2F;arxiv.org&#x2F;abs&#x2F;cs&#x2F;0011047" rel="nofollow">https:&#x2F;&#x2F;arxiv.org&#x2F;abs&#x2F;cs&#x2F;0011047

    [5] <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Knuth%27s_Algorithm_X" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Knuth%27s_Algorithm_X

    [6] <a href="https:&#x2F;&#x2F;github.com&#x2F;arminbiere&#x2F;cadical" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;arminbiere&#x2F;cadical

    1. cchianel · · focus · HN ↗
      Agreed; another useful technique is &quot;Feed it to a heuristic solver&quot;. Heuristic solvers tend to be easier to program and reason about than a SAT solver, since you can use your existing domain model. Moreover, your scoring function look like a typical function that can call third party libraries (as heuristic solvers see the function as a black box usually). Heuristic solvers beat SAT solvers in cases like VRP, whereas SAT solvers are usually better at bin packing.

      If you want to try to implement one yourself, a simple one is Simulated Annealing [1]. The core algorithm shouldn&#x27;t be more than 30 lines of code; it is simple to implement. If you want to try an existing library, you can try Timefold Solver [2] (disclosure: I work for Timefold).

      [1] <a href="https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Simulated_annealing" rel="nofollow">https:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Simulated_annealing

      [2] <a href="https:&#x2F;&#x2F;timefold.ai&#x2F;solver" rel="nofollow">https:&#x2F;&#x2F;timefold.ai&#x2F;solver

Open on Hacker News to reply ↗

Unofficial Hacker News client; not affiliated with Y Combinator.