Paper 2022/672

CENSOR: Privacy-preserving Obfuscation for Outsourcing SAT formulas

Tassos Dimitriou, Kuwait University
Khazam Alhamdan, Kuwait University

We propose a novel obfuscation technique that can be used to outsource hard satisfiability (SAT) formulas to the cloud. Servers with large computational power are typically used to solve SAT instances that model real-life problems in task scheduling, AI planning, circuit verification and more. However, outsourcing data to the cloud may lead to privacy and information breaches since satisfying assignments may reveal considerable information about the underlying problem modeled by SAT. In this work, we develop CENSOR (privaCy prEserviNg obfuScation for Outsourcing foRmulas), a novel SAT obfuscation framework that resembles Indistinguishability Obfuscation. At the core of the framework lies a mechanism that transforms any formula to a random one with the same number of satisfying assignments. As a result, obfuscated formulas are indistinguishable from each other thus preserving the input-output privacy of the original SAT instance. Contrary to prior solutions that are rather adhoc in nature, we formally prove the security of our scheme. Additionally, we show that obfuscated formulas are within a polynomial factor of the original ones thus achieving polynomial slowdown. Finally, the whole process is efficient in practice, allowing solutions to original instances to be easily recovered from obfuscated ones. A byproduct of our method is that all NP problems can be potentially outsourced to the cloud by means of reducing to SAT.

Note: Updated the flattening and pre-processing phases with more details and examples.

Available format(s)
Publication info
SATisfiabilityObfuscationCloud computing/outsourcingVerifiabilityPrivacy preservationRandom walks/Mixing time
Contact author(s)
tassos dimitriou @ ieee org
khazam alhamdan @ grad ku edu kw
2023-10-21: revised
2022-05-30: received
See all versions
Short URL
Creative Commons Attribution


      author = {Tassos Dimitriou and Khazam Alhamdan},
      title = {CENSOR: Privacy-preserving Obfuscation for Outsourcing SAT formulas},
      howpublished = {Cryptology ePrint Archive, Paper 2022/672},
      year = {2022},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.