Encoding Treewidth into SAT (bibtex)
by Marko Samer, Helmut Veith
Abstract:
One of the most important structural parameters of graphs is treewidth, a measure for the ``tree-likeness'' and thus in many cases an indicator for the hardness of problem instances. The smaller the treewidth, the closer the graph is to a tree and the more efficiently the underlying instance often can be solved. However, computing the treewidth of a graph is NP-hard in general. In this paper we propose an encoding of the decision problem whether the treewidth of a given graph is at most k into the propositional satisfiability problem. The resulting SAT instance can then be fed to a SAT solver. In this way we are able to improve the known bounds on the treewidth of several benchmark graphs from the literature.
Reference:
Encoding Treewidth into SATMarko Samer, Helmut VeithProceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT'09) (Oliver Kullmann, ed.), volume 5584 of Lecture Notes in Computer Science, pages 45-50, July 2009, Springer-Verlag.
Bibtex Entry:
@inproceedings{SamVei09SAT,
  author = {Marko Samer and Helmut Veith},
  title = {Encoding Treewidth into SAT},
  month = {July},
  year = {2009},
  booktitle = {Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing (SAT'09)},
  editor = {Kullmann, Oliver},
  pages = {45--50},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  volume = {5584},
  abstract = {One of the most important structural parameters of graphs is treewidth, a measure for the ``tree-likeness'' and thus in many cases an indicator for the hardness of problem instances. The smaller the treewidth, the closer the graph is to a tree and the more efficiently the underlying instance often can be solved. However, computing the treewidth of a graph is NP-hard in general. In this paper we propose an encoding of the decision problem whether the treewidth of a given graph is at most k into the propositional satisfiability problem. The resulting SAT instance can then be fed to a SAT solver. In this way we are able to improve the known bounds on the treewidth of several benchmark graphs from the literature.},
  isbn = {978-3-642-02776-5},
  doi = {10.1007/978-3-642-02777-2_6}
}
Powered by bibtexbrowser