Paper 2026/1918
Towards Practical Privacy-Preserving SAT Solving
Abstract
Privacy-preserving Boolean satisfiability (SAT) solvers allow multiple distrustful parties to solve the conjunction of their private formulas without revealing their inputs. Prior work on privacy-preserving SAT solvers, i.e., ppSAT (USENIX Security 2022), fails to solve formulas of practical size and complexity because it supports only the most basic SAT-solving algorithm. We bring privacy-preserving SAT solving closer to practicality by introducing ppCDCL. Through carefully orchestrated oblivious data structures and solver architecture, our new solver enables conflict-driven clause learning (CDCL) and efficient propagation, the two most important features of modern plaintext SAT solvers. Evaluation results show that ppCDCL outperforms ppSAT in both capability and efficiency. It solves significantly more instances: 98% vs. 65% on the Haplotype benchmarks and 84% vs. 28% on the larger, more diverse SATLIB benchmarks. Furthermore, it solves 36% of SATLIB instances within 1,000 seconds compared to only 4% for ppSAT.
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Major revision. ACM CCS 2026
- Keywords
- Secure ComputationSAT Solver
- Contact author(s)
-
gefeitan @ u northwestern edu
wenhao zhang @ northwestern edu
timos antonopoulos @ yale edu
ruzica piskac @ yale edu
wangxiao1254 @ gmail com
nl27 @ illinois edu - History
- 2026-09-10: approved
- 2026-09-08: received
- See all versions
- Short URL
- https://ia.cr/2026/1918
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2026/1918,
author = {Gefei Tan and Wenhao Zhang and Timos Antonopoulos and Ruzica Piskac and Xiao Wang and Ning Luo},
title = {Towards Practical Privacy-Preserving {SAT} Solving},
howpublished = {Cryptology {ePrint} Archive, Paper 2026/1918},
year = {2026},
url = {https://eprint.iacr.org/2026/1918}
}
