Dealing With Uncertainty Between Peers and Having the Best of Times With Distributed Systems
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
Parallel and Distributed Automated Reasoning 2022
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
Diminishing increases in CPU frequency over the last years lead to increasing demands in SAT & QBF solvers to use multiple cores at once for solving formulas. Multiple solving paradigms exist to parallelize these solvers, each suited for different problem families. One of them is Cube and Conquer, which tries to split formulas into sub-problems by applying assumptions. This lends itself well to parallel solving, as many sub-problems may be solved at the same time. Distributing such a solver is conceptionally easy, but requires significant implementation effort that is mostly identical for different solvers. For this we created Paracooba 2, a framework for solvers based on splitting their (sub-) problems. Paracooba 2 provides the multithreading and distribution over multiple hosts, letting a solving module be implemented in an easier and abstracted environment. In this talk, we share details about this implementation, some networking-related and conceptual challenges that arose during development, and how we have overcome them.
Sprache der Kurzfassung:
Englisch
Englischer Vortragstitel:
Dealing With Uncertainty Between Peers and Having the Best of Times With Distributed Systems
Englischer Tagungstitel:
Parallel and Distributed Automated Reasoning 2022
Englische Kurzfassung:
Diminishing increases in CPU frequency over the last years lead to increasing demands in SAT & QBF solvers to use multiple cores at once for solving formulas. Multiple solving paradigms exist to parallelize these solvers, each suited for different problem families. One of them is Cube and Conquer, which tries to split formulas into sub-problems by applying assumptions. This lends itself well to parallel solving, as many sub-problems may be solved at the same time. Distributing such a solver is conceptionally easy, but requires significant implementation effort that is mostly identical for different solvers. For this we created Paracooba 2, a framework for solvers based on splitting their (sub-) problems. Paracooba 2 provides the multithreading and distribution over multiple hosts, letting a solving module be implemented in an easier and abstracted environment. In this talk, we share details about this implementation, some networking-related and conceptual challenges that arose during development, and how we have overcome them.
Vortragstyp:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung
Forschungs-