Structure-aware CNF obfuscation for privacy-preserving SAT solving

In this paper, we study the problem of solving hard propositional satisfiability problem in Cloud or computing grid, which is honest-but-curious. We propose an approach to preserve input and output privacy based on CNF obfuscation, and present obfuscation algorithm and its corresponding solution recovery algorithm. By obfuscation, the CNF formula is transformed into another formula, with different circuit structure and over-approximated solution space. Solution of the original CNF can be extracted from the solution of obfuscated CNF by solution recovery. Theoretical analysis demonstrates that, obfuscation algorithm can significantly change the structure of CNF formula with polynomial time complexity, while solution recovery algorithm can filter out solution with linear time complexity. Experimental results on ISCAS89 benchmark show that obfuscation incurs acceptable negative impact on the performance of SAT solving.