0
$\begingroup$

The algorithm works as follows:

For each clause, the algorithm turns the middle disjunction into conjunction, i.e. if an arbitrary clause is of the form:

(l1 ∨ l2) ∨ (l3 ∨ l4)

Then after turning the middle disjunction into conjunction the 4CNF clause becomes conjunction of two 2CNF clauses:

(l1 ∨ l2) ∧ (l3 ∨ l4)

After doing this for all clauses in the input 4CNF formula, the input 4CNF formula becomes 2CNF formula and the algorithm builds the first implications directed graph from the result 2CNF formula, which has 2n vertices, where n is the number of atomic variables in the input formula given as input and each vertex in the implications directed graph is for each other and different literal, and the disjunction of each clause (in the result 2CNF formula) is two directed edges in the implications directed graph.

If an arbitrary clause from the result 2CNF formula is l1 ∨ l2 then the implications directed graph has the following edges:

(¬l1,l2) and (¬l2,l1), because of the fact that:

l1 ∨ l2 ≡ ¬l1→l2 ≡ ¬l2→l1

Once the first implications directed graph is ready, the algorithm tries to find contradictions in this implications directed graph.

Note that every contradiction is a cycle in the implications directed graph, which is two paths in the implications directed graph: a path from x to ¬ x and a path from ¬x to x, where x is one of the variables given in the input of the algorithm, and a path in the implications directed graph is conjunction of implications, so is cycle.

If no contradiction was found then the algorithm returns the answer that "The given 4CNF formula is satisfiable" as output.

But if contradiction was found, then the algorithm does the following:

If a cycle in the first implications directed graph is contradiction, then the negation of the conjunction of all implications in that cycle must be true in the satisfying truth assignment/interpretation/model.

So the algorithm counts the number of contradictions found in the first implications directed graph and then it creates a jagged array, which is an array of arrays and whose length is the number of contradictions found in the first implications directed graph.

Then for each contradiction in the first implications directed graph, compute the length of the cycle, which is to count the number of directed edges in that cycle, which is the number of implications, that their conjunction is contradiction.

Once the algorithm finished to compute the length of the cycle of the contradiction the algorithm creates a new array, whose length is the computed length of the cycle of the contradiction and the new array is member of / element of the jagged array.

Then in that array, the algorithm writes down all the directed edges of the cycle, which are all implications, that their conjunction is contradiction.

First contradiction is always at index 0 of the jagged array, second contradiction is always at index 1 of the jagged array, third contradiction is always at index 2 of the jagged array and so on.

Now the algorithm needs to find a satisfying assignment/interpretation/model so not all the implications in any of the arrays of the jagged array are true.

To do so, the algorithm builds another implications directed graph.

Back to the original 4CNF formula, in each clause, interpret the first two literals as they were four vertices in the second implications graph, and interpret the third and fourth literals as they were another four vertices in the second implications graph, and the middle disjunction is eight directed edges in the second implications graph.

It's known fact that:

(l1 ∨ l2) ∨ (l3 ∨ l4) ≡ ((¬l1→l2) ∧ (¬l2→l1)) ∨ ((¬l3→l4) ∧ (¬l4→l3))

So in the second implications directed graph, ¬l1→l2, ¬l2→l1, ¬l3→l4, ¬l4→l3, ¬(¬l1→l2), ¬(¬l2→l1), ¬(¬l3→l4), ¬(¬l4→l3) are all vertices, but not directed edges!

So what are the directed edges in the second implications directed graph then?

The middle disjunction of the clause in the 4CNF formula determines this.

In general:

(¬(¬l1→l2),¬l3→l4), (¬(¬l1→l2),¬l4→l3), (¬(¬l2→l1),¬l3→l4), (¬(¬l2→l1),¬l4→l3), (¬(¬l3→l4),¬l1→l2),(¬(¬l3→l4),¬l2→l1), (¬(¬l4→l3),¬l1→l2) and (¬(¬l4→l3),¬l2→l1) are directed edges in the second implications directed graph for that clause.

Once the second implications directed graph is ready the algorithm firstly tries to find contradiction in the second implications directed graph, the same way as in the first implications directed graph.

If contradiction was found, then the algorithm returns and the output of the algorithm is "the given 4CNF formula is unsatisfiable", because even though it was assumed that disjunction of two literals was a free independent atomic variable there is still contradiction in the formula, so there is contradiction without the assumption as well.

If no contradiction was found in the second implications directed graph then the algorithm uses it to tell if it is possible to find an truth assignment/interpretation/model so not all the implications in any of the arrays of the jagged array are true.

For each array in the jagged array, iterate through all the implications.

Each implication in the array of the jagged array is an directed edge in the first implications directed graph, but a vertex in the second implications directed graph.

Mark that vertex in the second implications directed graph.

Take two arbitrary vertices from the second implications directed graph:

¬li→lj and ¬lj→li

If there exist paths, from ¬li→lj to all marked vertices in the second implications directed graph, so also there exist paths, from ¬lj→li to all these marked vertices.

That means that in the original 4CNF formula, there is no satisfying assignment/interpretation/model where li ∨ lj is true, because li ∨ lj implies contradiction because of the both first and second implications directed graphs.

So ¬(li ∨ lj) must be true in all satisfying assignments/interpretations/models.

Now take vertices ¬(¬li→lj) and ¬(¬lj→li) from the second implications directed graph and check if there exist paths from these two vertices to the all marked vertices.

If such paths exist, then the output of the algorithm is "The given 4CNF formula is unsatisfiable", because it has reached a contradiction.

The conclusion is that both (li ∨ lj) and ¬(li ∨ lj) must be false in order to not be in a contradiction, because of the both implications directed graphs, but this is impossible, so this is a contradiction that cannot be resolved.

Thus the 4CNF formula is really unsatisfiable.

If for each four vertices ¬li→lj, ¬lj→li, ¬(¬li→lj) and ¬(¬lj→li), it was not possible to find paths to all marked vertices from each array of the jagged array, then the 4CNF formula is satisfiable, because no contradiction is detected.

The algorithm can call Floyd Wars-hall's algorithm to know for each two vertices, if there exist a path or not.

If the distance is finite, then there is a path, but if the distance is infinite, then there is no path.

Define that the weight of each directed edge (in the second implications directed graph) to be equal to 1 in order to the algorithm to work.

Now finally my question is:

Does this algorithm correct?

What is the time complexity of this algorithm?

What is the space complexity of this algorithm?

How do I analysis it?

Building both the first and second implications directed graphs should take polynomial both time and space, and Floyd War-shall's algorithm is known to be polynomial time algorithm Θ(V3), where V is the number of vertices in the given graph.

So I think that this algorithm, in total, should be polynomial both in time and space, but I want to make sure that this is really true.

Also it is possible that in each array of the jagged array, the algorithm can save the disjunction of two literals, rather than implication, so in the second implications directed graph, each vertex is either disjunction of two literals or the negation of disjunction of two literals, rather than implication.

Also I don't think that this is necessary to find contradiction in the second implications directed graph, because all literals in the assumption are positive and they aren't repeating in the formula, so the 2CNF that the 4CNF resembles is always satisfiable, so the algorithm will never find contradiction in the second implications directed graph.

$\endgroup$
  • $\begingroup$ And now this seems to be linked to my conjecture. $\endgroup$ – rus9384 Jul 20 '17 at 23:50
  • $\begingroup$ What do you mean? What is your conjecture? $\endgroup$ – Farewell Stack Exchange Jul 21 '17 at 1:06
  • $\begingroup$ Here it is: cs.stackexchange.com/questions/77818/… . It strongly relies on 2-variable implications. $\endgroup$ – rus9384 Jul 21 '17 at 2:01
  • $\begingroup$ Very nice question you asked there! Did you find the answer to your question since then? $\endgroup$ – Farewell Stack Exchange Jul 21 '17 at 3:37

Your Answer

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

Browse other questions tagged or ask your own question.