For a CNF formula F we define its 1-conflict graph as follows: Two clauses C,D ∈ F are connected by an edge if they have a nontrivial resolvent - that is, if there is a unique literal u ∈ C for which ū ∈ D. Let lc1(F) denote the maximum degree of this graph. A k-CNF formula is a CNF formula in which each clause has exactly k distinct literals. We show that (1) a k-CNF formula F with lc1(F) ≤ k - 1 is satisfiable; (2) there are unsatisfiable k-CNF formulas F with lc_1(F) = k; (3) there is a polynomial time algorithm deciding whether a k-CNF formula F with lc_1(F) = k is satisfiable; (4) satisfiability of k-CNF formulas F with lc_1(F) ≤ k + 1 is NP-hard. Furthermore, we show that if F is a k-CNF formula and lc_1(F) ≤ k, then we can find in polynomial time a satisfying assignment (if F is satisfiable) or a treelike resolution refutation with at most |F| leaves (if F is unsatisfiable). Here, |F| is the number of clauses of F.
展开▼
