Ozdemir, A., Wu, H., & Barrett, C. (2021). SAT Solving in the Serverless Cloud. In Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021 (pp. 241–245). TU Wien Academic Press. https://doi.org/10.34727/2021/isbn.978-3-85448-046-4_33
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
Series:
Conference Series: Formal Methods in Computer-Aided Design
-
Published in:
Proceedings of the 21st Conference on Formal Methods in Computer-Aided Design – FMCAD 2021
-
Date (published):
Oct-2021
-
Number of Pages:
5
-
Publisher:
TU Wien Academic Press, Wien
-
Peer reviewed:
Yes
-
Keywords:
parallel SAT; serverless computing; divide and conquer
en
Abstract:
In recent years, cloud service providers have sold
computation in increasingly granular units. Most recently,
“serverless” executors run a single executable with restricted
network access and for a limited time. The benefit of these
restrictions is scale: thousand-way parallelism can be allocated in
seconds, and CPU time is billed with sub-second granularity. To
exploit these executors, we introduce gg-SAT: an implementation
of divide-and-conquer SAT solving. Infrastructurally, gg-SAT
departs substantially from previous implementations: rather than
handling process or server management itself, gg-SAT builds
on the gg framework, allowing computations to be executed on
a configurable backend, including serverless offerings such as
AWS Lambda. Our experiments suggest that when run on the
same hardware, gg-SAT performs competitively with other D&C
solvers, and that the 1000-way parallelism it offers (through AWS
Lambda) is useful for some challenging SAT instances.