Does Treewidth Help in Modal Satisfiability?

Details Does Treewidth Help in Modal Satisfiability? Does Treewidth Help in Modal Satisfiability?

2010-06-12

arxiv.org/abs/1006.2461v2

Computer Science

Logic in Computer Science

Full version of the paper appearing in MFCS 2010. Change from v1: improved section 5 to avoid exponential blow-up in formula s

Scientific paper

Many tractable algorithms for solving the Constraint Satisfaction Problem (CSP) have been developed using the notion of the treewidth of some graph derived from the input CSP instance. In particular, the incidence graph of the CSP instance is one such graph. We introduce the notion of an incidence graph for modal logic formulae in a certain normal form. We investigate the parameterized complexity of modal satisfiability with the modal depth of the formula and the treewidth of the incidence graph as parameters. For various combinations of Euclidean, reflexive, symmetric and transitive models, we show either that modal satisfiability is FPT, or that it is W[1]-hard. In particular, modal satisfiability in general models is FPT, while it is W[1]-hard in transitive models. As might be expected, modal satisfiability in transitive and Euclidean models is FPT.

Affiliated with

Also associated with

No associations

Rating

Does Treewidth Help in Modal Satisfiability? does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Does Treewidth Help in Modal Satisfiability?, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Does Treewidth Help in Modal Satisfiability? will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-644998