2-satisfiability 2026-10-18
2-satisfiability restricts SAT to CNF in which each Boolean clause has at most two Boolean literals. The example in Boolean satisfiability problem is therefore a 2-SAT instance. Unlike general SAT and 3-SAT, 2-SAT has a polynomial-time algorithm; its tractability concerns finding a satisfying assignment or deciding that none exists, not merely checking a candidate. 3-SAT allows up to three Boolean literals per Boolean clause and is NP-complete, even though it includes many individually easy instances such as this one.[ref]
The key logical equivalence is
where are Boolean literals. It expresses a two-Boolean literal Boolean clause as two logical implications. Representing these logical implications as edges in a directed graph gives a route to the polynomial-time algorithm. In the example, says both and : enabling the feature requires its component, and an absent component excludes the feature.
3-SAT reduction to vertex cover Created 2026-10-07 Updated 2026-10-14
A polynomial-time many-one reduction represents each variable by an adjacent literal pair and each clause by a triangle in a graph. Connect each occurrence vertex to its corresponding literal vertex. A vertex cover of size must choose one literal vertex per variable and two vertices per clause, and its omitted clause vertex forces a true literal. Conversely a satisfying Boolean valuation supplies such a cover. This establishes NP-hardness of the vertex-cover decision problem from 3-SAT.
Boolean-pair colouring gadget Created 2026-10-06 Updated 2026-10-14
Two graph triangles sharing a vertex force their two opposite edges to use the same two colours in a graph colouring with three colours. A palette graph triangle and another graph triangle therefore force the literal pair to have opposite Boolean colours. This gadget is used in a reduction from 3-SAT to the three-colourability problem.
Conjunctive normal form Created 2026-10-06 Updated 2026-10-18
A Boolean formula is in conjunctive normal form when it is a logical conjunction of Boolean clauses. It is true precisely when every Boolean clause is true under the same Boolean valuation; an empty logical conjunction is true. For example, has two Boolean clauses with widths two and one. Width counts Boolean literal occurrences within a Boolean clause, whereas the Boolean clause count counts the conjuncts. 2-SAT bounds width by two, and 3-SAT bounds width by three. A Boolean formula with an empty Boolean clause is an unsatisfiable Boolean formula.
A decision problem is in NP if every yes-instance has a complexity certificate of length bounded by a polynomial in the input length, and a deterministic verifier can check that certificate in polynomial time. More precisely, for some polynomial and verifier ,
where runs in polynomial time. Equivalently, a nondeterministic machine decides the problem in polynomial time. A problem is NP-complete if it belongs to NP and is NP-hard: every problem in NP has a polynomial-time many-one reduction to it. Such a reduction maps instances to instances with if and only if is a yes-instance of the target problem.
For 3-SAT, the complexity certificate is one truth value for each Boolean variable. Check every Boolean literal, negate its variable's truth value when appropriate, evaluate the disjunction in each Boolean clause, and check their conjunction. This takes time linear in the encoded Boolean formula, apart from equally polynomial bookkeeping for variable names. A satisfying assignment passes; an unsatisfiable Boolean formula has no passing assignment. Thus 3-SAT belongs to NP.
For the diagram's three-colour clause gadget, name the three colours by the graph triangle . Each input is adjacent to , so each has colour or . Suppose that none has colour . Then all three have colour . Because is adjacent to and to , neither has colour . The edge forces these two colours to be and in some order. The graph triangle now forces to have colour . Since is adjacent to and , it must have colour . The graph triangle forces to have colour . But is adjacent to , which also has colour , contradicting a proper graph colouring. Therefore at least one input has colour .
To give the polynomial-time many-one reduction, use one common palette graph triangle . For each Boolean variable , create two graph vertices and join them to each other and to . This Boolean-pair colouring gadget forces them to have opposite colours . For each Boolean clause, introduce five fresh auxiliary graph vertices and the edges of the three-colour clause gadget, identifying its inputs with that clause's three Boolean literal vertices and using the common . In the notation of the diagram, its ten additional edges are the two triangles and , the bridge , and the three input edges. With variables and clauses the constructed undirected graph has vertices and at most edges. Repeated literals do not affect the argument. Its construction takes polynomial time.
A proper graph colouring defines a consistent truth assignment by declaring true precisely when its vertex has colour . The only-if result just proved makes every clause true. Conversely, a satisfying assignment colours every literal vertex consistently, and the supplied if-direction extends each satisfied clause's colours to its fresh auxiliary vertices. These extensions do not conflict, since different clauses share only already-coloured palette and literal vertices. Thus the Boolean formula is satisfiable exactly when the constructed undirected graph is three-colourable. Since 3-SAT is NP-complete, composition of reductions proves NP-hardness of the three-colourability problem.
Finally, a list of three colour labels, one for each graph vertex, is a complexity certificate for the three-colourability problem. Checking all edges takes time. Hence this problem is in NP as well, and the three-colourability problem is NP-complete.
Use the specified construction as a polynomial-time many-one reduction from 3-SAT. There are vertices and edges: one edge per variable pair, three edges per clause triangle in a graph, and three occurrence edges per clause. Any vertex cover must take at least one vertex from every variable pair and at least two from every clause triangle. Therefore every cover has at least vertices.
Given a satisfying Boolean valuation, include the vertex corresponding to the true Boolean literal in each variable pair. In each clause choose a true occurrence and omit its clause vertex, including the other two. Every variable edge and triangle edge is covered. An occurrence edge with an included clause endpoint is covered automatically; the only omitted occurrence vertex is joined to the included true-literal vertex. This is a vertex cover with exactly vertices.
Conversely, a cover of that size must use exactly one vertex in each variable pair and exactly two in each triangle. Declare a variable true precisely when its positive-literal vertex is included. Each clause has one omitted vertex. Its occurrence edge forces the corresponding literal vertex into the cover, so that literal is true. Every clause is therefore satisfied. Thus
The construction and target size are polynomial in the input length. Since 3-SAT is NP-complete, the decision problem is NP-hard. The usual “at most ” version has the same equivalence here because is an unavoidable lower bound. More generally, a cover with fewer than vertices can be padded to exactly . Verifying a proposed cover is polynomial, so the usual vertex-cover decision problem is also in NP and hence NP-complete.
The decision problem is in NP: an assignment is a certificate, and counting its satisfied clause occurrences is polynomial in the input size.
Reduce 3-SAT to it. For each of the original clauses, use the seven-clause gadget for MAX-2SAT with its three literals in place of and with a fresh auxiliary variable. Keep all ten clause occurrences per gadget, including any repeated occurrences across gadgets. Set the target to .
If the original formula is satisfiable, choose each auxiliary value as in part (a), giving seven satisfied clauses per gadget. Conversely, no gadget can exceed seven. If an assignment satisfies at least clauses in total, every gadget must reach seven, so every original clause is satisfied by the original-variable assignment. The construction has clauses and auxiliary variables, so is polynomial. Consequently the decision version of MAX-2SAT is NP-complete.
The three-colourability problem belongs to NP: a colour assignment is a polynomial-length complexity certificate, and all edges can be checked in time.
For NP-hardness, reduce 3-SAT to the three-colourability problem. Start with a palette graph triangle with vertices . Its colours are necessarily distinct, and name them by these vertices. For each Boolean variable , add vertices , join them to each other, and join each to . The graph triangle is the forcing component of the Boolean-pair colouring gadget, so the two literal vertices receive opposite colours .
For each Boolean clause, attach a fresh copy of the three-colour clause gadget, identify its with the palette vertex , and identify its three input vertices with the Boolean clause's Boolean literal vertices. Copies share only palette or literal vertices. A Boolean clause with one or two Boolean literals is padded to three by repeating a literal; an empty Boolean clause can be mapped immediately to the uncolourable graph .
Any graph colouring with three colours gives a truth assignment by reading colour as true. The three-colour clause gadget forbids three false inputs, so every Boolean clause is satisfied. Conversely, any satisfying truth assignment colours the literal pairs, and the extension property proved above independently colours the fresh auxiliary vertices of each clause. Thus the entire graph is three-colourable exactly when the formula is satisfiable.
There are vertices for variables and nonempty padded clauses, and edges. The construction is a polynomial-time many-one reduction. Using the permitted NP-completeness of 3-SAT, we obtain
A three-literal disjunction can be represented by ten unit or two-literal clause occurrences with one fresh auxiliary variable. If the number of true input literals is zero, the best auxiliary choice satisfies six; for , the best count is seven. Applying separate gadgets to all clauses of a 3-SAT instance gives target seven times the original clause count, proving NP-completeness of the decision form of MAX-2SAT. The local counting argument is essential: no gadget may exceed seven and compensate for an unsatisfied input clause.
Three-colourability problem Created 2026-10-06 Updated 2026-10-14
This decision problem asks whether a finite undirected graph has a graph colouring with three colours. It is NP-complete: a colouring certifies membership in NP, while 3-SAT reduces using Boolean-pair colouring gadgets and three-colour clause gadgets.