The complexity of the falsifiability problem for pure implicational formulas Original Research Article

We consider Boolean formulas where logical implication (→) is the only operator and all variables, except at most one (denoted z), occur at most twice. We show that the problem of determining falsifiability for formulas of this class is NP-complete but if the number of occurrences of z is restricted to be at most k then there is an O(|F|k) algorithm for certifying falsifiability. We show this hierarchy of formulas, indexed on k, is interesting because even lower levels (e.g., k=2) are not subsumed by several well-known polynomial time solvable classes of formulas.