News for hackers. Stuff that matters.

A comment on Modern SAT solvers: fast, neat and underused (2018). Parent comment

Re:Modern SAT solvers: fast, neat and underused (2018) by xavxav on Friday May 26, 2023 @03:34PM (#36088618)
Wait, this is very relevant to some work I’ve been doing recently, how do you conclude that Horn clauses should be preferred from Schaefer’s theorem?
[ Parent | on HN ]
Re:Modern SAT solvers: fast, neat and underused (2018) by thomasahle on Friday May 26, 2023 @03:54PM (#36088795)
Isn't it just that Horn clauses are easy to understand, and they are guaranteed to be fast.
[ Parent | on HN ]
Re:Modern SAT solvers: fast, neat and underused (2018) by Karrot_Kream on Friday May 26, 2023 @04:02PM (#36088881)
Take a look at https://en.wikipedia.org/wiki/Boolean_satisfiability_problem... (based on Schaefer's "The complexity of satisfiability problems"). Horn clause satisfiability problems (HORN SAT) fall in P-c.
[ Parent | on HN ]
Re:Modern SAT solvers: fast, neat and underused (2018) by xavxav on Saturday May 27, 2023 @04:37AM (#36093047)
Oh right this is just Horn clauses, not CHCs
[ Parent | on HN ]