Consider a formula of propositional logic consisting of aconjunction of clauses of the form (±p⊕±q), where p and q arepropositional variables (not necessarily distinct) and ±p standsfor either p or ¬p. Consider the graph in which the verticesinclude p and ¬p for all propositional variables p appearing in theformula, and in which there is an edge (1) connecting p and ¬p foreach variable p, and (2) connecting two literals if theirexclusive-or is a clause of the formula. Prove that the formula issatisfiable if and only if the graph is 2-colorable.
