Fault Tolerant Boolean Satisfiability
  A delta-model is a satisfying assignment of a Boolean formula for which any
small alteration, such as a single bit flip, can be repaired by flips to some
small number of other bits, yielding a new satisfying assignment. These
satisfying assignments represent robust solutions to optimization problems
(e.g., scheduling) where it is possible to recover from unforeseen events
(e.g., a resource becoming unavailable). The concept of delta-models was
introduced by Ginsberg, Parkes and Roy (AAAI 1998), where it was proved that
finding delta-models for general Boolean formulas is NP-complete. In this
paper, we extend that result by studying the complexity of finding delta-models
for classes of Boolean formulas which are known to have polynomial time
satisfiability solvers. In particular, we examine 2-SAT, Horn-SAT, Affine-SAT,
dual-Horn-SAT, 0-valid and 1-valid SAT. We see a wide variation in the
complexity of finding delta-models, e.g., while 2-SAT and Affine-SAT have
polynomial time tests for delta-models, testing whether a Horn-SAT formula has
one is NP-complete.
