5 ms·

Why are verified SAT solvers interesting?

Jweb_Guru 4y ago
SAT solvers often form (part of) the backbone of other proof assistants and verified software and hardware, which makes them producing correct output quite critical. At the same time, production SAT solvers (the ones people actually use on the critical path of these proof assistants) are very performance-sensitive, which means tons of optimizations that are nonobvious, subtle, and in some cases not obviously memory safe. This makes them ideal candidates for formal verification. Unfortunately, in the past, the proof effort required to produce a competitive SAT solver was so high that this was considered infeasible, so instead the industry has been focused on non-verified SAT solvers that produce efficiently verifiable certificates for their solution that can be checked by an independent verifier. This was an important improvement that has allowed SAT solvers to continue to evolve, but (as mentioned downthread) they have disadvantages compared to a solver that can be fully trusted without producing a certificate, including in "forcing" people to use techniques that produce proofs which we know how to efficiently verify. What this project promises is an order of magnitude reduction in proof effort to achieve and maintain an extensible, competitive, verified solver, which may help change the above calculus to favor verified solvers. IMO, it is quite an exciting development, even if it does not pan out!
- jhgb 4y ago
  Maybe I'm missing something blindingly obvious, but why is "trusting" a SAT solver necessary in the first place? The solution itself either satisfies the constraints or it does not. Are there situations where we can't even tell whether the solution is correct by looking at the problem instance?
  - Jweb_Guru 4y ago
    For positive solutions, you are correct--verifying the solution is incredibly easy. For negative solutions (UNSAT), however, this is not the case--UNSAT is in Co-NP, not NP. Finding an efficiently verifiable representation of the UNSAT proof can be very challenging, which is part of why solvers are given much more time to produce and verify certificates than they are to solve the problem in the first place.
    - jhgb 4y ago
      Ahh, I see now what you mean. Thanks, that makes much more sense to me now.
    - dwheeler 4y ago
      Right, unsat is the interesting case where you especially want a proof of the SAT solver. Unsat can be used, in turn, to prove other things. If you want to prove that some condition C is always true in a set of expressions, just ask the SAT solver to solve for "not C". If the answer is UNSAT, then C is always true... if the answer UNSAT is actually correct.
- andi999 4y ago
  Thanks. Do you have a link or reference to more material on the certificates. I dont understand a bit, but I want to learn more.
  - Jweb_Guru 4y ago
    I will just steal from the paper's author (Sarek) and point you to the first two talks and lecture notes by Randy Bryant at this link: https://fm.csl.sri.com/SSFT22/#splogic https://fm.csl.sri.com/SSFT22/#splogic.

SAT solvers often form (part of) the backbone of other proof assistants and verified software and hardware, which makes them producing correct output quite critical. At the same time, production SAT solvers (the ones people actually use on the critical path of these proof assistants) are very performance-sensitive, which means tons of optimizations that are nonobvious, subtle, and in some cases not obviously memory safe. This makes them ideal candidates for formal verification. Unfortunately, in the past, the proof effort required to produce a competitive SAT solver was so high that this was considered infeasible, so instead the industry has been focused on non-verified SAT solvers that produce efficiently verifiable certificates for their solution that can be checked by an independent verifier. This was an important improvement that has allowed SAT solvers to continue to evolve, but (as mentioned downthread) they have disadvantages compared to a solver that can be fully trusted without producing a certificate, including in "forcing" people to use techniques that produce proofs which we know how to efficiently verify. What this project promises is an order of magnitude reduction in proof effort to achieve and maintain an extensible, competitive, verified solver, which may help change the above calculus to favor verified solvers. IMO, it is quite an exciting development, even if it does not pan out!

jhgb 4y ago
Maybe I'm missing something blindingly obvious, but why is "trusting" a SAT solver necessary in the first place? The solution itself either satisfies the constraints or it does not. Are there situations where we can't even tell whether the solution is correct by looking at the problem instance?
- Jweb_Guru 4y ago
  For positive solutions, you are correct--verifying the solution is incredibly easy. For negative solutions (UNSAT), however, this is not the case--UNSAT is in Co-NP, not NP. Finding an efficiently verifiable representation of the UNSAT proof can be very challenging, which is part of why solvers are given much more time to produce and verify certificates than they are to solve the problem in the first place.
  - jhgb 4y ago
    Ahh, I see now what you mean. Thanks, that makes much more sense to me now.
  - dwheeler 4y ago
    Right, unsat is the interesting case where you especially want a proof of the SAT solver. Unsat can be used, in turn, to prove other things. If you want to prove that some condition C is always true in a set of expressions, just ask the SAT solver to solve for "not C". If the answer is UNSAT, then C is always true... if the answer UNSAT is actually correct.
andi999 4y ago
Thanks. Do you have a link or reference to more material on the certificates. I dont understand a bit, but I want to learn more.
- Jweb_Guru 4y ago
  I will just steal from the paper's author (Sarek) and point you to the first two talks and lecture notes by Randy Bryant at this link: https://fm.csl.sri.com/SSFT22/#splogic https://fm.csl.sri.com/SSFT22/#splogic.