I need help proving that this problem is decidable in polynomial-time:

Input: a 3CNF formula with more than one clause.

Question: can the formula be divided into two satisfiable 3CNF formulas ?

Example: given the formula:

(x1 or not(x2) or x3) and (x1 or x2 or x3) and (not(x1) or not(x2) or not(x3))

the answer is "yes", as we can divide into these two satisfiable 3CNF formulas:

  1. (x1 or not(x2) or x3) and (x1 or x2 or x3)
  2. (not(x1) or not(x2) or not(x3))
  • 2
    $\begingroup$ Crossposted from SO. $\endgroup$
    – Raphael
    Jul 13 '12 at 14:21
  • 3
    $\begingroup$ Is this a homework? $\endgroup$ Jul 13 '12 at 19:20
  • 3
    $\begingroup$ Welcome to cstheory, a Q&A site for research-level questions in theoretical computer science (TCS). Your question does not appear to be a research-level question in TCS. Please see the FAQ for more information on what is meant by this and suggestions for sites that might welcome your question. Finally, if your question is closed for being out of scope, and you believe you can edit the question to make it a research-level question, please feel free to do so. Closing is not permanent and questions can be reopened, check the FAQ for more information. $\endgroup$
    – Kaveh
    Jul 14 '12 at 3:58
  • $\begingroup$ Please add some context/background/motivation for the question if you think the question is a research-level question and in Theoretical Computer Science's scope. For general level questions please consider posting on Computer Science. $\endgroup$
    – Kaveh
    Jul 14 '12 at 3:59

Take a formula $\phi$ in 3-CNF over variables $V=\{v_{i}\}$ and clauses $C=\{c_{j}\}$, and let $A:V\rightarrow \{TRUE,FALSE\}$ be an arbitrarily chosen assignment.

The clauses of $\phi$ can be divided into two categories, those that are satisfied by $A$ and those that aren't. All those that are satisfied have at least one literal that evaluates to $TRUE$, however those that aren't have no such literals. Let $C_{T} = \{c^{T}_{j}\}$ be set of clauses that evaluate to $TRUE$ under $A$, and $C_{F} = \{c^{F}_{j}\}$ be the rest.

Assuming that neither $C_{F}$ nor $C_{T}$ are empty, then $\bigwedge_{j} c^{T}_{j}$ is satisfiable under $A$, and $\bigwedge_{j} c^{F}_{j}$ is satisfiable under $\bar{A}$, the inverse assignment of $A$.

In the trivial cases (thanks to Marzio! q.v. the comments) where either $C_{F} = \emptyset$ or $C_{T} = \emptyset$ any split is valid, with $A$ being a satisfying assignment for both subformula in the first case, and $\bar{A}$ being a satisfying assignment in the second.

These two formula are in 3-CNF, and partition the clauses of $\phi$.

  • $\begingroup$ thank you for your answer, i would just like to clarify some points to better my understanding: $\endgroup$ Jul 13 '12 at 14:12
  • $\begingroup$ (sorry pressed enter by mistake...) does this mean that we can always find such a partition to satisfiable formulas (and so the answer is always "yes") ? $\endgroup$ Jul 13 '12 at 14:23
  • $\begingroup$ Yep, whatever the truth assignment, you can split the formula. $\endgroup$ Jul 13 '12 at 15:42
  • 1
    $\begingroup$ @LukeMathieson: the only trivial cases that must be handled differently is when $A$ is a satisfying assignment for $\phi$ (i.e. all clauses are true) or $A$ doesn't make true any clause at all. In the first case every split is valid, in the second case every split is valid using $\bar{A}$. $\endgroup$ Jul 13 '12 at 16:16
  • $\begingroup$ Hehe, the stupid thing is I thought of this, just failed to actually write it in... (I'll add it for smooth reading). $\endgroup$ Jul 15 '12 at 4:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.