"An algorithm for the class of pure implicational formulas"
Article by John Franco, Judy Goldsmith, John S. Schlipf, Ewald Speckenmeyer, R. P. Swaminathan, available as BibTeX Source.
Informatik, Universität zu Köln
Preprint Key:	zpr97-270
Keywords:	Boolean functions, fixed parameter tractable, implicational formulas, satisfiability problem
This article was published in 1999 in the journal "Discrete Applied Mathematics", volume 96-97, number 270, pages 89-106.
Abstract:	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 O(n). 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 O(kn), which is polynomial for a fixed k. Thus this problem is fixed-parameter tractable.