Hiding multiple solutions in a hard 3-SAT formula

摘要

Hiding solutions in 3-SAT formulas can be used in privacy protection and data security. Although the typical q-hidden algorithm could cancel the attraction to the unique predefined solution, and generate deceptive 3-SAT formulas with unique predefined solution, few works have mentioned that with multiple predefined solutions. Therefore, the objective of this paper is to propose algorithms which could cancel the attraction to the multiple predefined solutions simultaneously. The core element of these proposed algorithms is misguiding the SAT solvers with local search strategy to the reverse direction of the centre solution of the multiple predefined solutions, so that the attraction to the multiple predefined solutions can be cancelled simultaneously. Experimental results verify the behaviour of the two classical SAT solvers: the SAT solvers with local search strategy (such as WalkSAT) and that with DPLL strategy (such as zChaff). And a real-world application is introduced based on the proposed algorithm.