3 ms·

Generating a proof and checking it is definitely a step up, but it does have a few issues. - SAT is in NP, and UNSAT is in CoNP. This means that proofs take a

by Sarek 4y ago

Generating a proof and checking it is definitely a step up, but it does have a few issues. - SAT is in NP, and UNSAT is in CoNP. This means that proofs take a lot of space to store and a lot of time to check. Proofs are usually run with 5x the time limit of the initial solve, and still end up timing out. - Proofs are (currently) based on resolution, which means that research on efficient solving techniques which can not be efficiently modelled as resolution is not being prioritised. This is touched on briefly in the first 2 talks of Randy Bryant on: https://fm.csl.sri.com/SSFT22/#splogic https://fm.csl.sri.com/SSFT22/#splogic. I think the talks in general are among the better for understanding a SAT solver like CreuSAT.

fjdh 4y ago
>Proofs are (currently) based on resolution Proofs are actually based on a practical version of extended resolution [1] called DRAT. Extended resolution is an extremely strong proof system, and research on techniques that are not efficiently modelled by resolution are in fact being prioritised (see for instance [2]). This is not to say that CreuSAT is not very impressive, but just a correction on the current state of the things. [1]: https://en.wikipedia.org/wiki/Frege_system#Extended_Frege_system https://en.wikipedia.org/wiki/Frege_system#Extended_Frege_sy... [2]: https://link.springer.com/chapter/10.1007/978-3-642-31365-3_28 https://link.springer.com/chapter/10.1007/978-3-642-31365-3_...