SAT Solving in the Serverless Cloud

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:

   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 = {}

(This webpage was created with bibtex2web.)