TY - JOUR
T1 - An algorithm for the class of pure implicational formulas
AU - Franco, John
AU - Goldsmith, Judy
AU - Schlipf, John
AU - Speckenmeyer, Ewald
AU - Swaminathan, R. P.
PY - 1999/10/15
Y1 - 1999/10/15
N2 - 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(nk). 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(kk n2), which is polynomial for a fixed k. Thus this problem is fixed-parameter tractable.
AB - 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(nk). 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(kk n2), which is polynomial for a fixed k. Thus this problem is fixed-parameter tractable.
KW - Boolean functions
KW - Fixed parameter tractable
KW - Implicational formulas
KW - Satisfiability
UR - https://www.scopus.com/pages/publications/17144444721
UR - https://www.scopus.com/inward/citedby.url?scp=17144444721&partnerID=8YFLogxK
U2 - 10.1016/S0166-218X(99)00038-4
DO - 10.1016/S0166-218X(99)00038-4
M3 - Article
AN - SCOPUS:17144444721
SN - 0166-218X
VL - 96-97
SP - 89
EP - 106
JO - Discrete Applied Mathematics
JF - Discrete Applied Mathematics
ER -