Paper 2021/1584

ppSAT: Towards Two-Party Private SAT Solving

Ning Luo
Samuel Judson
Timos Antonopoulos
Ruzica Piskac
Xiao Wang

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).

Available format(s)
Cryptographic protocols
Publication info
Published elsewhere. USENIX Security 2022
secure multiparty computation sat solving
Contact author(s)
samuel judson @ yale edu
2022-08-12: revised
2021-12-03: received
See all versions
Short URL
Creative Commons Attribution


      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{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.