Lecture 09: Large-Scale SAT Solving
This lecture was a talk by Dominik Schreiber. For the content, we refer to the video on our NextCloud called sat-solving-230619-parallel-portfolio-clause-sharing-mallob.mp4.
Check Your Knowledge
- Explain the analogy of the “antisocial nerds.”
- What approaches do you know for parallel SAT solving?
- Explain the idea of clause sharing. What are crucial design choices we have to consider?
- Why do we need communication protocols when using massively parallel hardware? How does that affect parallel SAT solving?
- Explain how clause exchange works in Mallob.
- Why do we need clause filtering?
- What challenge do LBD values impose?
- Sharing clauses appear to simulate diversification techniques. Why could that be?