How to test CNF for satisfiability?

Question

If we have a conjunctive linked expression where only the following clauses are allowed: $A_i, \quad \neg A_i, \quad A_i \vee \neg A_j, \quad \neg A_i \vee A_j$

Example: $A_1 \wedge (A_2 \vee \neg A_3) \wedge \neg A_3 \wedge (\neg A_2 \vee A_4) $ What's the easiest way to check for satisfiability or non-satitsfiability?

Answer 1

1. Remove all clauses that are always true, that is if it contains both the negated and non-negated litteral.
2. Remove super-clauses, that is a clause containing already stated litterals as another clause, for example $(A\vee B\vee \neg C)\wedge(\neg C\vee B) \equiv (B\vee \neg C)$.
   
3. Assign the litterals in singelton clauses the value $\top$.
4. Assign the litterals that are only occurring as either negated or non-negated the value $\top$.
5. Use a semantic tableau on the remaining clauses by using the rules for and and or.

As for your example: $$ A_1\wedge(A_2\vee\neg A_3)\wedge\neg A_3\wedge(\neg A_2\vee A_4)\\ \equiv A_1\wedge \neg A_3\wedge(\neg A_2\vee A_4)\\ \cong \top\wedge\top\wedge(\top\vee\top)\\ \equiv \top\,\text{is satisfiable} $$

No tableau is needed in most examples, keep in mind that you may want to do step 4 more than one time (by removing clauses that contains $\top$ in between).

EDIT: This is a general solution to CNF-form.

Answer 2

Because of the very restricted sort of clauses that you allow, there is an efficient algorithm for deciding satisfiability. Make a list of all the propositional variables $A_i$ that are used in your formula. The algorithm will gradually determine that certain variables must be assigned the value T (i.e., true) in any satisfying truth assignment and that certain variables must be assigned F. The process begins by assigning T to any variable $A_i$ that occurs as one of the clauses in your formula, and assigning F to any $A_i$ such that $\neg A_i$ occurs as one of the clauses. After that, repeatedly carry out the following steps for each clause of the form $A_i\lor\neg A_j$ (or the equivalent form $(\neg A_j)\lor A_i$). If $A_j$ has already been assigned T, then also assign T to $A_i$; and if $A_i$ has already been assigned F, then also assign F to $A_j$. Repeat this process as long as any new assignments are produced. At the end, if some variable has been assigned both T and F, then your formula is not satisfiable; otherwise it is satisfiable. In fact, in the latter case, you can obtain a satisfying truth assignment by starting with the values that the algorithm has assigned to variables and then assigning T to any variable that didn't already get a value assigned.

Note that this algorithm depends very strongly on the very restricted sort of clauses that you allow. In the first place, if you allowed clauses with three disjuncts rather than only two, then, as Arthur wrote in the comments, the problem becomes NP-complete, so no such efficient algorithm is known (or is likely to exist). Furthermore, if you had allowed clauses of the form $A_i\lor A_j$ or $(\neg A_i)\lor(\neg A_j)$, then there is still an efficient algorithm for deciding satisfiability, but it requires steps for handling the new sorts of clauses, and the method for obtaining a satisfying truth assignment is not as simple as assigning T to all the variables that didn't get truth values earlier.