Satisfiability Problem · Theory Problems

Lesson 1

Nikolai Chukhin · Alexander S. Kulikov

Basic Problems.

  1. (5 points) What are the shortest sets of clauses with the following properties?
    1. (2 points) Satisfiable.
    2. (3 points) Unsatisfiable.
  2. (10 points) Recall the pigeonhole principle for \(n + 1\) pigeons and \(n\) holes. Let the variable \(x_{ph}\), where \(1 \le p \le n+1\) and \(1 \le h \le n\), be equal to one if and only if the \(p\)-th pigeon occupies the \(h\)-th hole. The formula consists of the following clauses:
    • Every pigeon occupies some hole: for all \(1 \le p \le n+1\), \[(x_{p1}\lor x_{p2}\lor \dotsb \lor x_{pn}) \ .\]

    • Each hole contains at most one pigeon: for all \(1 \le h \le n\) and all \(1 \le p < p' \le n+1\), \[(\overline{x_{ph}}\lor \overline{x_{p'h}}) \ .\]

    Although this formula is clearly unsatisfiable, prove that if one removes an arbitrary single clause, the resulting formula becomes satisfiable.
  3. (10 points) Consider the simplest modification of the backtracking algorithm: after assigning a value to the next variable, we shall immediately assign values to variables from unit clauses (i.e. clauses with only one literal). Prove that such an algorithm solves the 2-satisfiability problem in polynomial time.
  4. (10 points) For a Boolean function \(f \colon \{0, 1\}^{n}\to \{0, 1\}\), take the DNF \(F\), which is a disjunction of conjunctions corresponding to the rows where \(f(x) = 1\). Then, we say that \(F'\) is a prime DNF of a monotone function \(f\), constructed from \(F\) by the following procedure:
    • Remove all literals with negations.

    • Delete all clauses that are a superset of some other clause. I.e., leave only minimal by inclusion clauses.

    Prove that the prime DNF of any monotone function is the shortest possible DNF.
  5. (15 points) For a given graph with \(n\) vertices, construct a CNF formula with \(n^{2}\) variables that is satisfiable if and only if the graph has a Hamiltonian cycle.
    Hint:
    Let the variables be \(x_{i,j}\) for \(i, j \in \{1, …, n\}\), where \(x_{i,j}\) is true if vertex \(j\) is the \(i\)-th vertex in the cycle. The formula must enforce the properties of a Hamiltonian cycle:
    1. Every vertex must appear exactly once in the cycle.
    2. Every position in the cycle must be filled by exactly one vertex.
    3. If two vertices are adjacent in the cycle, they must be connected by an edge in the graph.
    Express each of these conditions as a conjunction of clauses.
  6. (15 points) Prove that the resolution algorithm decides the satisfiability of any \(2\)-CNF formula in polynomial time. Assume the resolution algorithm works as follows: it repeatedly finds any two resolvable clauses in the current set and adds their resolvent to the set (if it is not already present). No clauses are ever deleted. The process continues as long as new resolvents can be generated.
    Hint:
    Consider the total number of possible clauses that can be generated during the resolution process. How many literals can a clause obtained by resolving two \(2\)-clauses contain?
  7. (15 points) Consider a formula \(C_{1}\land C_{2}\land \dotsb \land C_{m}\), where each \(C_{i}\) is an \(\mathrm{XOR}\) of certain variables. That is, we start with a CNF and replace each \(\lor\) by \(\oplus\). Prove that the satisfiability of this formula can be determined in polynomial time.
    Hint:
    Observe that the formula represents a system of linear equations over \(\mathbb{F}_{2}\).
  8. (15 points) Provide an algorithm that takes as input a formula \(F\) in CNF and, in time linear in the size of \(F\) (i.e., the total length of all clauses in \(F\)), constructs a formula \(F'\) in 3-CNF that is equisatisfiable with \(F\).

    This means, in particular, that if there is a polynomial algorithm for the satisfiability problem of formulas in \(3\)-CNF, then there is also a polynomial algorithm for the satisfiability problem of formulas in CNF.

  9. (15 points) Unique SAT (\(\mathrm{USAT}\)) is the problem of deciding whether a given Boolean formula has exactly one satisfying assignment. Prove that if \(\mathrm{SAT}\) can be solved in polynomial time, then \(\mathrm{USAT}\) can also be solved in polynomial time.
  10. (15 points) Prove that the resolution proof system is complete: from any unsatisfiable formula in CNF, it is possible to derive the empty clause.

    The resolution proof system works as follows. Start with the original clauses. Then, in one step, one takes two clauses \((A \lor x)\) and \((B \lor \overline{x})\) (where \(A\) and \(B\) are disjunctions of literals) and adds a clause \((A \lor B)\). Hence, the original two clauses are not removed and can be used in the later steps.

  11. (15 points) Show that every satisfiability problem with \(m\) clauses and \(n\) variables can be transformed into an equivalent formula with \(m+n\) clauses and \(2n\) variables, in which the first \(m\) clauses contain only negative literals, and the last \(n\) clauses are binary with two positive literals.

    I.e., the problem of checking the satisfiability of a formula remains hard even if each clause contains either only positive literals or only negative literals.