Abstract
We investigate the computational complexity of some prominent variants of the propositional satisfiability problem (SAT), namely not-all-equal SAT (NAE-SAT) and exact SAT (XSAT) restricted to the class of linear conjunctive normal form (CNF) formulas. Clauses of a linear formula pairwise have at most one variable in common. We prove that NAE-SAT and XSAT both remain NP-complete when restricted to linear formulas. Since the corresponding reduction is not valid when input formulas are not allowed to have 2-clauses, we also prove that NAE-SAT and XSAT still behave NP-complete on formulas only containing clauses of length at least k, for each fixed integer k ≥ 3. Moreover, NP-completeness proofs for NAE-SAT and XSAT restricted to monotone linear formulas are presented. We also discuss the length restricted monotone linear formula classes regarding NP-completeness where a difficulty arises for NAE-SAT, when all clauses are k-uniform, for k ≥ 4. Finally, we show that NAE-SAT is polynomial-time decidable on exact linear formulas, where each pair of distinct clauses has exactly one variable in common. And, we give some hints regarding the complexity of XSAT on the exact linear class.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Berge, C.: Hypergraphs. North-Holland, Amsterdam (1989)
Byskov, J.M., Ammitzboll Madsen, B., Skjernaa, B.: New Algorithms for Exact Satisfiability. Theoretical Comp. Sci. 332, 515–541 (2005)
Eiter, T.: Open Problems in Satisfiability, http://www.ece.uc.edu/~franco/Sat-workshop/sat-workshop-open-problems.html
Garey, M.R., Johnson, D.S.: Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, San Francisco (1979)
Knuth, D.E.: Axioms and Hulls. LNCS, vol. 606. Springer, Heidelberg (1992)
Lam, C.W.H., Thiel, L., Swiercz, S.: The Non-existence of Finite Projective Planes of Order 10, article dedicated to the memory of H. J. Ryser (1989), http://citeseerx.ist.psu.edu/viewdoc/summary/doi=10.1.1.39.8684
Monien, B., Speckenmeyer, E., Vornberger, O.: Upper Bounds for Covering Problems. Methods of Operations Research 43, 419–431 (1981)
Palisse, R.: A short proof of Fisher’s inequality. Discrete Math. 111, 421–422 (1993)
Porschen, S., Speckenmeyer, E.: A CNF class generalizing Exact Linear Formulas. In: Kleine Büning, H., Zhao, X. (eds.) SAT 2008. LNCS, vol. 4996, pp. 231–245. Springer, Heidelberg (2008)
Porschen, S., Speckenmeyer, E., Zhao, X.: Linear CNF formulas and satisfiability. Discrete Appl. Math. (2008) doi:10.1016/j.dam, 03.031
Ryser, H.J.: Combinatorial Mathematics, Carus Mathematical Monographs 14, Mathematical Association of America (1963)
Schaefer, T.J.: The complexity of satisfiability problems. In: Proc. STOC, pp. 216–226. ACM, New York (1978)
Scheder, D.: Unsatisfiable Linear k-CNFs Exist, for every k (preprint, 2007) arXiv:math cs.DM/0708.2336 v1
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Porschen, S., Schmidt, T. (2009). On Some SAT-Variants over Linear Formulas. In: Nielsen, M., Kučera, A., Miltersen, P.B., Palamidessi, C., Tůma, P., Valencia, F. (eds) SOFSEM 2009: Theory and Practice of Computer Science. SOFSEM 2009. Lecture Notes in Computer Science, vol 5404. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-95891-8_41
Download citation
DOI: https://doi.org/10.1007/978-3-540-95891-8_41
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-95890-1
Online ISBN: 978-3-540-95891-8
eBook Packages: Computer ScienceComputer Science (R0)