<p>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.</p>

<p>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.</p>

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

<p>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.</p>

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

CC BY-SA 3.0
2012-07-13T14:12:38.723Z
thank you for your answer, i would just like to clarify some points to better my understanding:
user1521539
CC BY-SA 3.0
2012-07-13T14:23:08.883Z
(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") ?
user1521539
CC BY-SA 3.0
2012-07-13T15:42:34.290Z
Yep, whatever the truth assignment, you can split the formula.
Luke Mathieson
CC BY-SA 3.0
2012-07-13T16:16:33.587Z
@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}$.
Marzio De Biasi
CC BY-SA 3.0
2012-07-15T04:28:14.837Z
Hehe, the stupid thing is I thought of this, just failed to actually write it in... (I'll add it for smooth reading).
Luke Mathieson
CC BY-SA 3.0
2012-07-13T13:47:44.043Z
2012-07-15T04:32:01.510Z
2012-07-15T04:32:01.510Z
Luke Mathieson
<p>I need help proving that this problem is decidable in polynomial-time:</p>

<p><strong>Input:</strong> a 3CNF formula with more than one clause.</p>

<p><strong>Question:</strong> can the formula be divided into two satisfiable 3CNF formulas ?</p>

<p><strong>Example:</strong> given the formula: </p>

<p>(x1 or not(x2) or x3) and (x1 or x2 or x3) and (not(x1) or not(x2) or not(x3))</p>

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

<ol>
<li>(x1 or not(x2) or x3) and (x1 or x2 or x3)</li>
<li>(not(x1) or not(x2) or not(x3))</li>
</ol>

CC BY-SA 3.0
2012-07-13T14:21:25.157Z
Crossposted from [SO](http://stackoverflow.com/q/11470352/539599).
Raphael
CC BY-SA 3.0
2012-07-13T19:20:07.927Z
Is this a homework?
Mahdi Cheraghchi
CC BY-SA 3.0
2012-07-14T03:58:49.680Z
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.
Kaveh
CC BY-SA 3.0
2012-07-14T03:59:06.077Z
Please add some context/background/motivation for the question if you think the question is a research-level question and in [cstheory.se]'s scope. For general level questions please consider posting on [cs.se].
Kaveh
<cc.complexity-theory><complexity-classes><computability><sat><polynomial-time>
Help proving a 3CNF related prob. is in P
user1521539
# Help proving a 3CNF related prob. is in P

(Asked by: username_0 on 2012-07-13)

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))

**Tags:** cc.complexity-theory, complexity-classes, computability, sat, polynomial-time
> **Comments:**
> **username_1**: Crossposted from [SO](http://stackoverflow.com/q/11470352/539599).  
> **username_2**: Is this a homework?  
> **username_3**: 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.  
> **username_3**: Please add some context/background/motivation for the question if you think the question is a research-level question and in [cstheory.se]'s scope. For general level questions please consider posting on [cs.se].  

---

## 1 answers

### Answer by username_4 on 2012-07-13. Score: 12 | Accepted answer

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

> **Comments:**
> **username_0**: thank you for your answer, i would just like to clarify some points to better my understanding:  
> **username_0**: (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") ?  
> **username_4**: Yep, whatever the truth assignment, you can split the formula.  
> **username_5**: @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}$.  
> **username_4**: Hehe, the stupid thing is I thought of this, just failed to actually write it in... (I'll add it for smooth reading).  

---

