4 ms·

I thought proof checking tools mostly negated the need for verified sat solvers.

Jweb_Guru 4y ago
Producing the proofs (especially for UNSAT) is often very time consuming, and verifying them can be subtle (and if an incorrect proof is produced, you still have to deal with that case somehow...). It's not so much that they negate the need for verified SAT solvers as that creating and maintaining a verified SAT solver was considered much too difficult to justify the proof effort required. If the goal can be accomplished with an order of magnitude less effort, that calculus changes somewhat.
- zozbot234 4y ago
  SAT solving is the subtle and time consuming part. A valid SAT proof certificate can be verified efficiently.
  - Jweb_Guru 4y ago
    I'm referring to producing the certificate as the time-consuming part, not the verification time (I disagree that verification is not subtle, but I suppose that doesn't matter as there are verified verifiers). For example, many SAT solvers no longer attempt to provide "pure" resolution proofs because they are too expensive to produce, which restricts the kinds of techniques you see used in competition. In fact, producing certificates efficiently is an active research area, which wouldn't be the case if certificate production had negligible cost, e.g. see https://lmcs.episciences.org/9357/pdf https://lmcs.episciences.org/9357/pdf.
  - xavxav 4y ago
    SAT comp gives you 5x the solving time to check your proof, which is indicative that checking isn’t so simple (though it is on paper)
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_...
k0k0r0 4y ago
A former coworker of mine was in the process of publishing a really nice paper about a framework that allows concurrent resp. simultaneous verification of proofs generated by most state-of-the-art SAT Solvers, which drastically reduced the time needed to construct and then resp. simultaneously verify UNSAT proofs. Unfortunately, he left before publishing the paper. (Among other reasons he was unhappy with the academic world, which I do understand perfectly.) Unfortunately, I have trouble reaching him. I believe his basically finished paper would be of so much use to some people. It's really sad. I believe his paper really should be published in a journal or at least put online somewhere. It's not totally groundbreaking or something, but like hard work nobody had the determination to, yet. At least not publicly. I feel so bad that I can not share his work without his permission.

Producing the proofs (especially for UNSAT) is often very time consuming, and verifying them can be subtle (and if an incorrect proof is produced, you still have to deal with that case somehow...). It's not so much that they negate the need for verified SAT solvers as that creating and maintaining a verified SAT solver was considered much too difficult to justify the proof effort required. If the goal can be accomplished with an order of magnitude less effort, that calculus changes somewhat.

zozbot234 4y ago
SAT solving is the subtle and time consuming part. A valid SAT proof certificate can be verified efficiently.
- Jweb_Guru 4y ago
  I'm referring to producing the certificate as the time-consuming part, not the verification time (I disagree that verification is not subtle, but I suppose that doesn't matter as there are verified verifiers). For example, many SAT solvers no longer attempt to provide "pure" resolution proofs because they are too expensive to produce, which restricts the kinds of techniques you see used in competition. In fact, producing certificates efficiently is an active research area, which wouldn't be the case if certificate production had negligible cost, e.g. see https://lmcs.episciences.org/9357/pdf https://lmcs.episciences.org/9357/pdf.
- xavxav 4y ago
  SAT comp gives you 5x the solving time to check your proof, which is indicative that checking isn’t so simple (though it is on paper)

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_...

k0k0r0 4y ago

A former coworker of mine was in the process of publishing a really nice paper about a framework that allows concurrent resp. simultaneous verification of proofs generated by most state-of-the-art SAT Solvers, which drastically reduced the time needed to construct and then resp. simultaneously verify UNSAT proofs. Unfortunately, he left before publishing the paper. (Among other reasons he was unhappy with the academic world, which I do understand perfectly.) Unfortunately, I have trouble reaching him. I believe his basically finished paper would be of so much use to some people. It's really sad. I believe his paper really should be published in a journal or at least put online somewhere. It's not totally groundbreaking or something, but like hard work nobody had the determination to, yet. At least not publicly. I feel so bad that I can not share his work without his permission.