| Boolean satisfiability (SAT) is a foundational problem with major impact on hardware and software verification, scheduling, planning, constraint satisfaction and knowledge representation. Cloud computing enables outsourcing the heavy computation SAT often requires, overcoming local resource constraints and enabling large-scale or real-time solving. However, delegating SAT instances to the cloud can expose sensitive formulas or intermediate data. Practical adoption, therefore, demands outsourcing methods that preserve confidentiality and produce verifiable results while still leveraging cloud-scale computations. In this work, we present a method for obfuscating SAT instances that yields compact, outsource-friendly formulas with a distinctive two-part structure: a CNF core interleaved with XOR disjunctions, followed by an extra layer of XOR constraints. Empirical and theoretical analysis shows that leading SAT solvers exhibit exponential scaling on these instances, emphasizing the need for new techniques combining SAT solving with XOR support. Further investigation uncovers surprising insights regarding the shattering of the solution space. Specifically, obfuscated instances exhibit a uniform distribution of satisfying assignments, a development that can be used to produce more accurate estimators for model sampling and counting, thus improving approximate #SAT solvers and probabilistic inference methods central to many AI applications. |
*** Title, author list and abstract as submitted during Camera-Ready version delivery. Small changes that may have occurred during processing by Springer may not appear in this window.