Description
The algorithm ppSAT as introduced by Luo et al. can solve the SAT
problem ϕ = ϕ1 ∧ ϕ2 where the formulas ϕ1 and ϕ2 (stemming from party 1
and 2) remain private to their respective counterparties. This is a so-called
multi-party computation implemented with Garbled Circuits.
From a game theory perspective, this has substantial potential for problems
that can be modeled and then computed efficiently as a SAT instance.
Applications exist in biomedical applications where sharing private bio-
metric information conflicts with research goals: Often sensitive genetic
properties are associated in databases with personalized phenotypes such
as body height or diseases. Not blindly sharing these datasets is imperative
for protecting the trust and privacy of patients. Currently, ppSAT does
not leverage the full potential of modern SAT solvers because the current
solution consists of only a naive DPLL solver without an abort function.
This solution will run, under certain conditions, in the worst case runtime.
In this work, we pave the way for more refined solutions that do not run
for an exponential runtime. Our contributions are
• Formalizing the dynamic skipping where computation blocks can be
skipped by the evaluator
• Implementing a Garbled Circuit engine from scratch with dynamic
skipping
|
