Secure Outsourcing Scheme for Boolean Formulas Truth Assignment Problem

The Boolean formula satisfiability problem (SAT) plays a fundamental role in many practical applications, but is computationally challenging due to its NP-hard nature. Leveraging cloud computing has become an effective way to address larger-scale instances. This article proposes a secure outsourcing framework for solving Boolean formula SAT, with a focus on preserving the confidentiality of both the Boolean formulas and their solutions. The core innovation of our scheme lies in its robust obfuscation technique, which prevents the original formula from being exposed during outsourcing. This is an essential property when formulas encode sensitive designs, such as advanced digital circuits. Our approach transforms Boolean formulas into systems of equations over the finite field <inline-formula xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink"><tex-math notation="LaTeX">$\mathbf {GF}(2)$</tex-math></inline-formula>, which are then modified through arithmetic operations to generate an obfuscated equivalent. These transformed systems can be solved either by applying linearization techniques in the cloud or by reverting to Boolean form for processing by specialized SAT solvers. Compared to existing methods, our scheme offers enhanced protection by generating obfuscated instances that are indistinguishable from any formula with the same solution space. Moreover, the transformation incurs only linear growth in problem size, ensuring practical efficiency is maintained.