I work a lot with sat solvers, but with using in a proper language. Either cbmc ... | Hacker News

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

login

rurban on Aug 4, 2018 | parent | context | favorite | on: Modern SAT solvers: fast, neat and underused

I work a lot with sat solvers, but with using in a proper language. Either cbmc for C (not Klee, not Z3 as these require extensive translations to obscure languages), or picat for a proper functional language with support for normal non-functional coding styles.

The sudoku sample is a few lines there, and it used to win many CSP contests. http://www.hakank.org/picat/sudoku_pi.pi

cbmc is esp. nice to autocreate proper test cases.

rurban on Aug 8, 2018 [–]

Have to add to obvious ones: prolog. Almost every prolog comes now with a sat solver.

With prolog it's usually easiest to formulate a problem. Efficient solutions are a bit of a black art though: https://www.metalevel.at/prolog/horror

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