Satisfiability of co-nested formulas |
| |
Authors: | Jan Kratochvíl Mirko K?ivánek |
| |
Affiliation: | (1) KA MFF UK, Charles University, Sokolovská 83, 18600 Praha 8, Czech Republic;(2) KI MFF UK, Charles University, Malostranské nám. 25, 11000 Praha 1, Czech Republic |
| |
Abstract: | As a notion dual to Knuth's nested formulas 4], we call a boolean formula
in conjunctive normal formco-nested if its clauses can be linearly ordered (sayC={c
i
;i=1,2, ...,n})so that the graphG
cl
=(XC, {xc
i
;xc
i
or ¬xc
i
} {c
i
c
i+1;i=1, 2, ...,n}) allows a noncrossing drawing in the plane so that the circlec
1,c
2, ...,c
n
bounds the outerface. Our main result is that maximum satisfiability of co-nested formulas can be decided in linear time.Both authors acknowledge a partial support of Ec Cooperative Action IC-1000 (project ALTEC:Algorithms for Future Technologies). |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|