Solution space adjustable CNF obfuscation for privacy-preserving SAT solving

In this paper, we study the problem of privacy-preserving SAT solving in the cloud computing paradigm. We present a novel Husk formula based CNF obfuscation algorithm and its corresponding solution recovery algorithm, to prevent unauthorized third party in cloud obtaining sensitive information. By obfuscation, the CNF formula is transformed into another formula with over-approximated solution space. Solution of the original CNF can be extracted from the solution of obfuscated CNF by projection based solution recovery algorithm. By customizing the Husk formula, we make solution space of obfuscated CNF adjustable to control the ratio of false solution introduced by Obfuscation, to satisfying performance requiments. Theoretical analysis demonstrates that, with the aid of Cubic Husks formula, obfuscation algorithm can not only change the structure of CNF formula with polynomial time complexity, but also construct an adjustable over-approximated solution space. 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.