“SAT Solving in the Serverless Cloud” by Alex Ozdemir, Haoze Wu, and Clark Barrett. In Proceedings of the 21^st International Conference on Formal Methods In Computer-Aided Design (FMCAD '21), (Ruzica Piskac and Michael W. Whalen, eds.), Oct. 2021, pp. 241-245.
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 beneft 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 confgurable 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.
BibTeX entry:
@inproceedings{OWB21,
author = {Alex Ozdemir and Haoze Wu and Clark Barrett},
editor = {Ruzica Piskac and Michael W. Whalen},
title = {{SAT} Solving in the Serverless Cloud},
booktitle = {Proceedings of the {\it 21^{st}} International Conference
on Formal Methods In Computer-Aided Design (FMCAD '21)},
pages = {241--245},
publisher = {TU Wien Academic Press},
month = oct,
year = {2021},
doi = {10.34727/2021/isbn.978-3-85448-046-4_33},
url = {http://theory.stanford.edu/~barrett/pubs/OWB21.pdf}
}
(This webpage was created with bibtex2web.)