Cryptology ePrint Archive: Report 2021/1584

ppSAT: Towards Two-Party Private SAT Solving

Ning Luo and Samuel Judson and Timos Antonopoulos and Ruzica Piskac and Xiao Wang

Abstract: We design and implement a privacy-preserving Boolean satisfiability (ppSAT) solver, which allows mutually distrustful parties to evaluate the conjunction of their input formulas while maintaining privacy. We first define a family of security guarantees reconcilable with the (known) exponential complexity of SAT solving, and then construct an oblivious variant of the classic DPLL algorithm which can be integrated with existing secure two-party computation (2PC) techniques. We further observe that most known SAT solving heuristics are unsuitable for 2PC, as they are highly data-dependent in order to minimize the number of exploration steps. Faced with how best to trade off between the number of steps and the cost of obliviously executing each one, we design three efficient oblivious heuristics, one deterministic and two randomized. As a result of this effort we are able to evaluate our ppSAT solver on small but practical instances arising from the haplotype inference problem in bioinformatics. We conclude by looking towards future directions for making ppSAT solving more practical, most especially the integration of conflict-driven clause learning (CDCL).

Category / Keywords: cryptographic protocols / secure multiparty computation, sat solving

Original Publication (in the same form): USENIX Security 2022

Date: received 3 Dec 2021

Contact author: samuel judson at yale edu

Available format(s): PDF | BibTeX Citation

Version: 20211203:080011 (All versions of this report)

Short URL: ia.cr/2021/1584


[ Cryptology ePrint archive ]