On Satisfiability Problems with a Linear Structure

Authors Serge Gaspers, Christos H. Papadimitriou, Sigve Hortemo Sæther, Jan Arne Telle

Thumbnail PDF


  • Filesize: 0.6 MB
  • 14 pages

Document Identifiers

Author Details

Serge Gaspers
Christos H. Papadimitriou
Sigve Hortemo Sæther
Jan Arne Telle

Cite AsGet BibTex

Serge Gaspers, Christos H. Papadimitriou, Sigve Hortemo Sæther, and Jan Arne Telle. On Satisfiability Problems with a Linear Structure. In 11th International Symposium on Parameterized and Exact Computation (IPEC 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 63, pp. 14:1-14:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


It was recently shown [Sæther, Telle, and Vatshelle, JAIR 54, 2015] that satisfiability is polynomially solvable when the incidence graph is an interval bipartite graph (an interval graph turned into a bipartite graph by omitting all edges within each partite set). Here we relax this condition in several directions: First, we show an FPT algorithm parameterized by k for k-interval bigraphs, bipartite graphs which can be converted to interval bipartite graphs by adding to each node of one side at most k edges; the same result holds for the counting and the weighted maximization version of satisfiability. Second, given two linear orders, one for the variables and one for the clauses, we show how to find, in polynomial time, the smallest k such that there is a k-interval bigraph compatible with these two orders. On the negative side we prove that, barring complexity collapses, no such extensions are possible for CSPs more general than satisfiability. We also show NP-hardness of recognizing 1-interval bigraphs.
  • Satisfiability
  • interval graphs
  • FPT algorithms


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Amotz Bar-Noy, Reuven Bar-Yehuda, Ari Freund, Joseph (Seffi) Naor, and Baruch Schieber. A unified approach to approximating resource allocation and scheduling. In Proceedings of the Thirty-second Annual ACM Symposium on Theory of Computing, STOC'00, pages 735-744, New York, NY, USA, 2000. ACM. URL: http://dx.doi.org/10.1145/335305.335410.
  2. Andreas Brandstädt and Vadim V. Lozin. On the linear structure and clique-width of bipartite permutation graphs. Ars Comb., 67, 2003. Google Scholar
  3. Johann Brault-Baron, Florent Capelli, and Stefan Mengel. Understanding model counting for beta-acyclic CNF-formulas. In 32nd International Symposium on Theoretical Aspects of Computer Science, STACS 2015, March 4-7, 2015, Germany, volume 30 of LIPIcs, pages 143-156. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2015.143.
  4. Rodney G. Downey and Michael R. Fellows. Parameterized Complexity. Monographs in Computer Science. Springer, 1999. URL: http://dx.doi.org/10.1007/978-1-4612-0515-9.
  5. Christian Egeland. Algorithms for linearly ordered boolean formulas. Master’s thesis, University of Bergen, 2016. URL: http://hdl.handle.net/1956/12667.
  6. Eldar Fischer, Johann A. Makowsky, and Elena V. Ravve. Counting truth assignments of formulas of bounded tree-width or clique-width. Discrete Applied Mathematics, 156(4):511-529, 2008. URL: http://dx.doi.org/10.1016/j.dam.2006.06.020.
  7. M. R. Garey and David S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman, 1979. Google Scholar
  8. Serge Gaspers and Stefan Szeider. Backdoors to satisfaction. In Hans L. Bodlaender, Rod Downey, Fedor V. Fomin, and Dániel Marx, editors, The Multivariate Algorithmic Revolution and Beyond - Essays Dedicated to Mike Fellows on His 60th Birthday, volume 7370 of Lecture Notes in Computer Science, pages 287-317. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-30891-8_15.
  9. Serge Gaspers and Stefan Szeider. Strong backdoors to bounded treewidth SAT. In 54th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2013, 26-29 October, 2013, Berkeley, CA, USA, pages 489-498. IEEE Computer Society, 2013. URL: http://dx.doi.org/10.1109/FOCS.2013.59.
  10. Martin Charles Golumbic and Ron Shamir. Complexity and algorithms for reasoning about time: A graph-theoretic approach. J. ACM, 40(5):1108-1133, November 1993. URL: http://dx.doi.org/10.1145/174147.169675.
  11. Georg Gottlob and Stefan Szeider. Fixed-parameter algorithms for artificial intelligence, constraint satisfaction and database problems. Comput. J., 51(3):303-325, 2008. URL: http://dx.doi.org/10.1093/comjnl/bxm056.
  12. Frank Harary, Jerald A Kabell, and Frederick R McMorris. Bipartite intersection graphs. Commentationes Mathematicae Universitatis Carolinae, 23(4):739-745, 1982. Google Scholar
  13. Pavol Hell and Jing Huang. Interval bigraphs and circular arc graphs. Journal of Graph Theory, 46(4):313-327, 2004. URL: http://dx.doi.org/10.1002/jgt.20006.
  14. Haiko Müller. Recognizing interval digraphs and interval bigraphs in polynomial time. Discrete Applied Mathematics, 78(1-3):189-205, 1997. URL: http://dx.doi.org/10.1016/S0166-218X(97)00027-9.
  15. Christos H. Papadimitriou and Mihalis Yannakakis. On the complexity of database queries. Journal of Computer and System Sciences, 58(3):407-427, 1999. URL: http://dx.doi.org/10.1006/jcss.1999.1626.
  16. Daniël Paulusma, Friedrich Slivovsky, and Stefan Szeider. Model counting for CNF formulas of bounded modular treewidth. In STACS, volume 20 of LIPIcs, pages 55-66. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2013. URL: http://dx.doi.org/10.4230/LIPIcs.STACS.2013.55.
  17. Arash Rafiey. Recognizing interval bigraphs by forbidden patterns. CoRR, abs/1211.2662, 2012. Google Scholar
  18. Jean-Charles Régin and Jean-Francois Puget. A filtering algorithm for global sequencing constraints. In Proceedings of the 3rd International Conference on Principles and Practice of Constraint Programming (CP 1997), volume 1330 of Lecture Notes in Computer Science, pages 32-46. Springer, 1997. URL: http://dx.doi.org/10.1007/BFb0017428.
  19. Sigve Hortemo Sæther, Jan Arne Telle, and Martin Vatshelle. Solving #SAT and MAXSAT by dynamic programming. J. Artif. Intell. Res. (JAIR), 54:59-82, 2015. URL: http://dx.doi.org/10.1613/jair.4831.
  20. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. J. Discrete Algorithms, 8(1):50-64, 2010. URL: http://dx.doi.org/10.1016/j.jda.2009.06.002.
  21. Friedrich Slivovsky and Stefan Szeider. Model counting for formulas of bounded clique-width. In Leizhen Cai, Siu-Wing Cheng, and Tak Wah Lam, editors, ISAAC, volume 8283 of Lecture Notes in Computer Science, pages 677-687. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-45030-3_63.
  22. Christine Solnon, Van-Dat Cung, Alain Nguyen, and Christian Artigues. The car sequencing problem: Overview of state-of-the-art methods and industrial case-study of the ROADEF'2005 challenge problem. European Journal of Operational Research, 191(3):912-927, 2008. URL: http://dx.doi.org/10.1016/j.ejor.2007.04.033.
  23. Stefan Szeider. On fixed-parameter tractable parameterizations of SAT. In Enrico Giunchiglia and Armando Tacchella, editors, SAT 2003, volume 2919 of Lecture Notes in Computer Science, pages 188-202. Springer, 2003. URL: http://dx.doi.org/10.1007/978-3-540-24605-3_15.
  24. Ryan Williams, Carla P. Gomes, and Bart Selman. Backdoors to typical case complexity. In Georg Gottlob and Toby Walsh, editors, IJCAI-03, Proceedings of the Eighteenth International Joint Conference on Artificial Intelligence, Acapulco, Mexico, August 9-15, 2003, pages 1173-1178. Morgan Kaufmann, 2003. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail