News for hackers. Stuff that matters.

A comment on CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot. Parent comment

Re:CreuSAT: Formally verified SAT solver written in Rust and... by Zee2 on Friday June 17, 2022 @09:35PM (#31786570)
Isn't the traveling salesman optimization problem non-polynomially-verifiable? https://www.nomachetejuggling.com/2012/09/14/traveling-sales...
[ Parent | on HN ]
Re:CreuSAT: Formally verified SAT solver written in Rust and... by Jweb_Guru on Friday June 17, 2022 @09:37PM (#31786586)
The optimization problem isn't, but neither are the optimization problems for a bunch of other NP-complete problems. The decision problem (where you specify an upper bound cost) is indeed NP-complete.
[ Parent | on HN ]