Unit Resolution (UNIT)
Category: Logic
Input
A Boolean formula $F$ in conjunctive normal form.
Problem
Can the empty clause $\square$ be deduced from $F$ by unit resolution?
Definitions
A unit is a clause with only one term. For example, the unit resolvent of $A \vee B_1 \vee \cdots \vee B_m$ and the unit $\neg A$ is $B_1 \vee \cdots \vee B_m$.
Status
$\P$-complete (Jones and Laaser [1]).
Remarks
Jones and Laaser provide a polynomial time algorithm for unit resolution [1]. The reduction to show hardness is from CVP.
See Chang and Lee [2] for an introduction to mechanical theorem proving. Under the appropriate definitions, it is known that approximating this problem is also $\P$-complete (Serna and Spirakis [3]).
References
- N. D. Jones and W. T. Laaser (1976). Complete problems for deterministic polynomial time.
- C. L. Chang and R. C. T. Lee (1973). Symbolic Logic and Mechanical Theorem Proving.
- M. J. Serna and P. G. Spirakis (1989). The approximability of problems complete for P.
- S. Kasif (1986). On the parallel complexity of discrete relaxation in constraint satisfaction networks.
- D. A. Plaisted (1984). Complete problems in the first-order predicate calculus.
- Greenlaw, R., Hoover, H. J., and Ruzzo, W. L. (1995). Limits to Parallel Computation: P-Completeness Theory. Oxford University Press. Problem A.6.1.