Anzeige
Erschienen in:
2014 | OriginalPaper | Buchkapitel
Cloud-Oriented SAT Solver Based on Obfuscating CNF Formula
verfasst von : Ying Qin, Shengyu Shen, Jingzhu Kong, Huadong Dai
Erschienen in: Web Technologies and Applications
Verlag: Springer International Publishing
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Propositional satisfiability (SAT) has been widely used in hardware and software verification. Outsourcing complex SAT problem to Cloud can leverage the huge computation capability and flexibility of Cloud. But some confidential information encoded in CNF formula, such as circuit structure, may be leaked to unauthorized third party.
In this paper, we propose a novel Cloud-oriented SAT solving algorithm to preserve privacy.
First
, an obfuscated CNF formula is generated by embedding a Husk formula into the original formula with proper rules.
Second
, the obfuscated formula is solved by a state-of-the-art SAT solver deployed in Cloud.
Third
, a simple mapping algorithm is used to map the solution of the obfuscated formula back to that of the original CNF formula.
Theoretical analysis and experimental result show that our algorithms can significantly improve security of the SAT solver with linear complexity while keeping its solution space unchanged.