Universität zu Köln

Computational Complexity of SAT, XSAT and NAE-SAT for linear and mixed Horn CNF formulas

Schmidt, Tatjana (2010) Computational Complexity of SAT, XSAT and NAE-SAT for linear and mixed Horn CNF formulas. PhD thesis, Universität zu Köln.

[img]
Preview
PDF
Download (8Kb) | Preview
    [img]
    Preview
    PDF
    Download (899Kb) | Preview

      Abstract

      The Boolean conjunctive normal form (CNF) satisfiability problem, called SAT for short, gets as input a CNF formula and has to decide whether this formula admits a satisfying truth assignment. As is well known, the remarkable result by S. Cook in 1971 established SAT as the first and genuine complete problem for the complexity class NP. In this thesis we consider SAT for a subclass of CNF, the so called Mixed Horn formula class (MHF). A formula F in MHF consists of a 2-CNF part P and a Horn part H. We propose that MHF has a central relevance in CNF because many prominent NP-complete problems, e.g. Feedback Vertex Set, Vertex Cover, Dominating Set and Hitting Set, can easily be encoded as MHF. Furthermore, we show that SAT remains NP-complete for some interesting subclasses of MHF. We also provide algorithms for some of these subclasses solving SAT in a better running time than O(2^0.5284n) which is the best bound for MHF so far. One of these subclasses consists of formulas, where the Horn part is negative monotone and the variable graph corresponding to the positive 2-CNF part P consists of disjoint triangles only. Regarding the other subclass consisting of certain k-uniform linear mixed Horn formulas, we provide an algorithm solving SAT in time O(k^(n/k)), for k>=4. Additionally, we consider mixed Horn formulas F in MHF for which holds: H is negative monotone, c<=3, for all c in H, and P consists of positive monotone 2-clauses. We solve SAT in running time O(1.325^n) for this formula class by using the autarky principle, that means we can provide a better running time than the so far best one of O(p(n)\cdotp 1.427^n) by S. Kottler, M. Kaufmann and C. Sinz for this class of mixed Horn formulas. Afterwards we consider mixed Horn formulas F for which holds: G_P consists of disjoint triangles, edges and isolated vertices and H consists of Horn clauses which have at most three literals, but are not necessarily negative monotone and V(P)=V(H). We can solve SAT in running time O(1.41^n) for this formula class by applying the autarky principle. Thereafter we consider some interesting subclasses of MHF for which SAT can be solved in polynomial-time. Furthermore, we present an algorithm which solves SAT for mixed Horn formulas with a linear, negative monotone and k-uniform Horn part and a P part which consists of positive monotone and disjoint 2-clauses only. Experimental results lead to the strong conjecture that its running time is better than O(3^(n/3)), where n is the number of variables. In addition, we investigate the computational complexity of some prominent variants of SAT, namely not-all-equal SAT (NAESAT) and exact SAT (XSAT) restricted to the class of linear CNF formulas. Clauses of a linear formula pairwise have at most one variable in common. We show that NAESAT and XSAT are NP-complete for monotone and linear formulas where clauses have length greater or equal k, k>=3. We also prove the NP-completeness of XSAT for CNF formulas which are l-regular meaning that every variable occurs exactly l times, where l>=3 is a fixed integer. On that basis, we can provide the NP-completeness of XSAT for the subclass of linear and l-regular formulas. This result is transferable to the monotone case. Moreover, we provide an algorithm solving XSAT for the subclass of monotone, linear and l-regular formulas faster than the so far best algorithm from J. M. Byskov et al. for CNF-XSAT with a running time of O(2^0.2325n). Using some connections to finite projective planes, we can also show that XSAT remains NP-complete for linear and l-regular formulas that in addition are l-uniform whenever l=q+1, where q is a prime power. Thus XSAT most likely is NP-complete for the other values of l>= 3, too. Apart from that, we are interested in exact linear formulas: Here each pair of distinct clauses has exactly one variable in common. We show that NAESAT is polynomial-time decidable restricted to exact linear formulas. Reinterpreting this result enables us to give a partial answer to a long-standing open question mentioned by T. Eiter: Classify the computational complexity of the symmetrical intersecting unsatisfiability problem (SIM-UNSAT). Then we show the NP-completeness of XSAT for monotone and exact linear formulas, which we can also establish for the subclass of formulas whose clauses have length at least k, k>=3. This is somehow surprising since both SAT and not-all-equal SAT are polynomial-time solvable for exact linear formulas. However, for k=3,4,5,6 we can show that XSAT is polynomial-time solvable for the k-uniform, monotone and exact linear formula class.

      Item Type: Thesis (PhD thesis)
      Translated abstract:
      AbstractLanguage
      Bei dem Boole�schen Erfüllbarkeitsproblem für Formeln in konjunktiver Normalform (KNF), kurz SAT genannt, ist eine KNF Formel gegeben und man muss entscheiden, ob diese Formel eine erfüllende Belegung besitzt. Wie bereits bekannt ist, hat S. Cook in seinem bemerkenswerten Ergebnis von 1971 SAT als das erste authentische Problem für die Klasse NP herauskristallisiert. In dieser Arbeit betrachten wir SAT für eine Teilklasse von KNF, die sogenannten Mixed-Horn-Formeln (MHF). Eine Formel F in MHF besteht aus einem 2-KNF Teil P und einem Horn Teil H. Wir zeigen, dass MHF eine zentrale Rolle in KNF spielt, weil viele prominente Probleme, wie z.B. Feedback Vertex Set, Vertex Cover, Dominating Set und Hitting Set leicht als MHF kodiert werden können. Des Weiteren zeigen wir, dass SAT für einige interessante Teilklassen von MHF NP-vollständig bleibt. Sodann stellen wir Algorithmen für zwei solcher Teilklassen vor, die SAT in einer besseren Laufzeit als O(2^0.5284n) lösen, was soweit die beste Schranke für MHF ist. Eine dieser Teilklassen besteht aus Formeln, bei denen der Horn Teil negativ monoton ist und der zugehörige Variablengraph des entsprechenden positiv monotonen 2-KNF-Teils P nur aus disjunkten Dreiecken besteht. Für die zweite Teilklasse, die aus gewissen k-uniformen, linearen Mixed-Horn-Formeln besteht, geben wir einen Algorithmus an, der SAT in Zeit O(k^(n/ k)) für k>= 4 löst. Zusätzlich betrachten wir Mixed-Horn-Formeln F, für die gilt: H ist negativ monoton, c<=3, für alle c aus H, und P besteht nur aus positiven 2-Klauseln. Wir können SAT in der Laufzeit O(1.325^n) für diese Formelklasse lösen, indem wir das Autarkie-Prinzip benutzen. Das bedeutet, wir erzielen eine bessere Laufzeit als die bisher beste Laufzeit O(p(n)1.427^n) von S.Kottler, M.Kaufmann und C.Sinz für diese Klasse von Mixed-Horn-Formeln. Danach widmen wir uns denjenigen Mixed-Horn-Formeln F in MHF, für die gilt: G_P besteht aus disjunkten Dreiecken, Kanten und isolierten Knoten und H besteht aus Horn Klauseln, die höchstens 3 Literale besitzen, aber nicht notwendigerweise negativ monoton sind. Ferner soll gelten V(P)=V(H). Wir können SAT in der Laufzeit O(1.41^n) für diese Formelklasse lösen, indem wir ebenfalls das Autarkie-Prinzip benutzen. Danach betrachten wir noch einige interessante Teilklassen von MHF, für die wir SAT in Polynomzeit lösen können. Dann präsentieren wir einen Algorithmus, der SAT für Mixed-Horn-Formeln mit einem linearen, negativ monotonen und k-uniformen Horn-Teil und einem P-Teil, bestehend nur aus positiv monotonen und disjunkten 2-Klauseln, löst. Experimentelle Ergebnisse führen zu der starken Vermutung, dass dessen Laufzeit besser ist als O(3^(n/3), wobei n die Anzahl der Variablen einer solchen Formel bezeichnet. Als Nächstes erforschen wir die Komplexität einiger prominenter Varianten von SAT, nämlich NAESAT und XSAT, eingeschränkt auf die Klasse der linearen Formeln. Je zwei Klauseln einer linearen Formel haben höchstens eine Variable gemeinsam. Wir zeigen, dass NAESAT und XSAT für monotone und lineare Formeln, deren Klauseln länger oder gleich k sind, k>= 3, NP-vollständig sind. Ferner beweisen wir, dass XSAT für KNF-Formeln, die l-regulär sind, d.h. in denen jede Variable genau l Mal vorkommt, wobei l>=3 eine feste ganze Zahl ist, NP-vollständig ist. Darauf aufbauend können wir auch die NP-Vollständigkeit von XSAT für die Teilklasse der linearen und l-regulären Formeln zeigen. Dieses Ergebnis ist auch auf den monotonen Fall übertragbar. Ein weiteres Resultat dieser Arbeit ist ein Algorithmus, der XSAT für die Klasse der monotonen, linearen und l-regulären Formeln schneller löst als der bis dato schnellste Algorithmus von J. M. Byskov für KNF-XSAT mit einer Laufzeit von O(2^0.2325n). Indem wir einige Verbindungen zu den projektiven Ebenen nutzen, können wir auch zeigen, dass XSAT NP-vollständig bleibt für die Klasse der linearen und l-regulären Formeln, die zusätzlich l-uniform sind, wobei l=q+1 und q eine Primzahlpotenz ist. Daher ist es sehr wahrscheinlich, dass XSAT auch NP-vollständig ist für alle anderen Werte von l>=3. Wir interessieren uns im Weiteren für die exakt linearen Formeln: Je zwei Klauseln haben hier genau eine Variable gemeinsam. Wir zeigen, dass NAESAT für die Klasse der exakt linearen Formeln in Polynomzeit gelöst werden kann. Wenn wir dieses Ergebnis neu deuten, dann ermöglicht es uns eine teilweise Antwort auf eine lange offen stehende Frage, die von T.Eiter gestellt worden ist: Klassifizieren der Berechnungskomplexität des SIM-UNSAT-Problems. Als Nächstes zeigen wir die NP-Vollständigkeit von XSAT für monotone und exakt lineare Formeln, deren Klauseln mindestens Länge k, k>=3, haben. Dies ist überraschend, da sowohl SAT als auch NAESAT beide in Polynomzeit für exakt lineare Formeln gelöst werden können. Für k=3,4,5,6 können wir jedoch zeigen, dass XSAT für die k-uniformen, monotonen und exakt linearen Formeln in Polynomzeit gelöst werden kann.German
      Creators:
      CreatorsEmail
      Schmidt, Tatjanatatjana_schmidt83@yahoo.de
      URN: urn:nbn:de:hbz:38-31293
      Subjects: Data processing Computer science
      Uncontrolled Keywords:
      KeywordsLanguage
      Erfüllbarkeit , KNF, lineare Formeln , KomplexitätGerman
      satisfiability , complexity , mixed Horn formulasEnglish
      Faculty: Mathematisch-Naturwissenschaftliche Fakultät
      Divisions: Mathematisch-Naturwissenschaftliche Fakultät > Institut für Informatik
      Language: English
      Date: 2010
      Date Type: Completion
      Date of oral exam: 27 June 2010
      Full Text Status: Public
      Date Deposited: 09 Aug 2010 09:04:22
      Referee
      NameAcademic Title
      Speckenmeyer, EwaldProf. Dr.
      URI: http://kups.ub.uni-koeln.de/id/eprint/3129

      Actions (login required)

      View Item