An Algorithm for the Class of Pure Implicational Formulas,
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 exp(k)). 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((k exp(k))(n-sq)), which is polynomial for a fixed k. Thus this problem is fixed parameter tractable.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1996
- Accession Number
- ADA325899
Entities
People
- Ewald Speckenmeyer
- John Franco
- John Schlipf
- Judy Goldsmith
- R. P. Swaminathan
Organizations
- University of Cincinnati