An algorithm for the class of pure implicational formulas
Heusch introduced the notion of pure implicational formulas. He showed that the falsifiability problem for pure implicational formulas with k negations is solvable in time . Such falsifiability results are easily transformed to satisfiability results on CNF formulas. We show that the falsifiability problem for pure implicational formulas is solvable in time , which is polynomial for a fixed k. Thus this problem is fixed-parameter tractable.
implicational formulas satisfiability fixed parameter tractable boolean functions