-3
$\begingroup$

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))
Improve this question
$\endgroup$
4
  • 2
    $\begingroup$ Crossposted from SO. $\endgroup$
    – Raphael
    Jul 13, 2012 at 14:21
  • 3
    $\begingroup$ Is this a homework? $\endgroup$
    – Mahdi Cheraghchi
    Jul 13, 2012 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, 2012 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, 2012 at 3:59

1 Answer 1

Reset to default
12
$\begingroup$

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$.

Improve this answer
$\endgroup$
5
  • $\begingroup$ thank you for your answer, i would just like to clarify some points to better my understanding: $\endgroup$
    – user1521539
    Jul 13, 2012 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$
    – user1521539
    Jul 13, 2012 at 14:23
  • $\begingroup$ Yep, whatever the truth assignment, you can split the formula. $\endgroup$
    – Luke Mathieson
    Jul 13, 2012 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$
    – Marzio De Biasi
    Jul 13, 2012 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$
    – Luke Mathieson
    Jul 15, 2012 at 4:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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