Fault Tolerant Boolean Satisfiability

A -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 -models was introduced by Ginsberg, Parkes, and Roy (1998), where it was proved that finding -models for general Boolean formulas is NP-complete. In this paper, we extend that result by studying the complexity of finding -models for classes of Boolean formulas which are known to have polynomial time satisfiability solvers. In particular, we examine 2-SAT, Horn-SAT, AffineSAT, dual-Horn-SAT, 0-valid and 1-valid SAT. We see a wide variation in the complexity of finding -models, e.g., while 2-SAT and Affine-SAT have polynomial time tests for -models, testing whether a H...

• Type: Journal
• Year: 2006
• Where: JAIR
• Authors: Amitabha Roy
• Keywords: Boolean Formulas, General Boolean Formulas, JAIR 2006, Satisfying Assignments