Paper 2021/1584
ppSAT: Towards Two-Party Private SAT Solving
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).
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. USENIX Security 2022
- Keywords
- secure multiparty computation sat solving
- Contact author(s)
- samuel judson @ yale edu
- History
- 2022-08-12: revised
- 2021-12-03: received
- See all versions
- Short URL
- https://ia.cr/2021/1584
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2021/1584,
author = {Ning Luo and Samuel Judson and Timos Antonopoulos and Ruzica Piskac and Xiao Wang},
title = {ppSAT: Towards Two-Party Private SAT Solving},
howpublished = {Cryptology ePrint Archive, Paper 2021/1584},
year = {2021},
note = {\url{https://eprint.iacr.org/2021/1584}},
url = {https://eprint.iacr.org/2021/1584}
}
