I posted an algorithm yesterday, that purported to solve the co-NP Complete 'Boolean Tautology Problem' in polynomial time.
Link to the algorithm : polynomial time algorithm

In that post, I presented the algorithm's motivation, and implementation, but not proof of validity. Herein I present said proof :

Recap :

The algorithm accepts Exact $3-DNF$ expressions as input, and checks whether they are tautologies. The job of the algorithm is to derive, and mark clauses as true. Given some $n$ variable expression, the number of possible clauses are $8\times{n\choose 3}$ If all of them are derived, and marked true, then the algorithm claims that the expression is a tautology.

Given a $n$ variable expression, the algorithm first creates a graph in the following manner :

  1. Start with all possible clauses in $n$ variables, as initial nodes.
  2. Create children nodes for each parent by adding one more literal to the parent clause. Such child clauses can have multiple parents.
  3. For each such child, there is a dual child which has the negation of that one extra literal.
  4. Repeat this process with the children as parent nodes, until you either exhaust your variables, or end up with children with $6$ literals in their clauses.
  5. All nodes are initially marked false.

For reference, a child is the $\land$ of the parent clause, and another literal. E.g. Parent : $(a\land b\land c)$, possible children : $(a\land b\land c\land d)$, $(a\land b\land c\land\lnot e)$, etc.
Dual children of a parent have opposite literals, e.g. $(a\land b\land c\land d)$, and $(a\land b\land c\land\lnot d)$ are dual children of $(a\land b\land c)$. So are $(a\land b\land c\land e)$, and $(a\land b\land c\land\lnot e)$, etc.

Then, the algorithm scans the input boolean expression to extract the clauses present, and works in the following manner :

  1. Upon finding a clause in the expression, the corresponding clause node in the graph is marked true.
  2. If a parent node is true, all children nodes are marked true.
  3. If some dual couple children of a parent are true, then the parent is marked true.
  4. If every node is marked true, the original expression is a tautology, otherwise not.

This is a brief summary of the algorithm. I did not go into the reasoning behind these steps, as I've linked the original post. Now on to the proof of validity.

Rationale :

So, the question is, 'Why is the algorithm doing any of this?', and here's the answer :
We are given some $3-DNF$ boolean expression, and we can derive the presence of $3-DNF$ clauses from it. If the expression is a tautology, we can say that all possible clauses are present. Either they are directly present in the expression, or are a logical consequence of clauses within the expression. The job of the algorithm is to see if it can derive the presence of all possible clauses from the expression.

Obviously, the clauses present in the given expression are already present. The tricky part is to derive the remaining clauses. Each clause present in the expression carries with it some parts of the clauses not present directly. Each clause provides particular intersecting pieces of the missing, yet derivable clauses.

This is the reason why the algorithm stops making child nodes in the graph after they contain $6$ literals. This is because $6$ literals is the maximum number of possible literals in an intersection $(AND)$ of any two $3-DNF$ clauses.

Proof of Validity :

Herein, I go through the algorithm steps(after the graph is created) one by one, and justify them.

1) We find clauses in the input $3-DNF$ expression, by scanning through it. Every time we find a clause, we mark the corresponding node on the graph $true$. This implies that the particular clause is present , or has been derived to be present.

2) Any node on the graph represents a $\land$ of some literals. The propositional logic implication is that any assignment of variables that matches those of the literals present in the clause will result in the expression evaluating true. For example, if we consider the clause $(a\land b\land\lnot c)$ in $5$ variables, $\{a, b, c, d, e\}$, then any assignment of variables to the expression will result in the expression evaluating true, as long as we put $a=true$, $b=true$, $c=false$.

Therefore, if any parent node is true, any child node of the parent must also be true, since it is just a $\land$ of the parent, and another literal, i.e. it falls within variable assignments of the parent. For example, if $(a\land b\land\lnot c)$ is true, then any child, like $(a\land b\land\lnot c\land y)$ must also be true.

3) To prove : Some dual couple children are true $\Rightarrow$ Parent is true

Let us start with a parent $(x_1\land x_2\land\ldots\land x_k)$
If some dual couple children of this clause, with some variable $y$, are marked true, we get :
$(x_1\land x_2\land\ldots\land x_k\land y)\lor (x_1\land x_2\land\ldots\land x_k\land\lnot y)$
$=(x_1\land x_2\land\ldots\land x_k)\land (y\lor\lnot y)$
$=(x_1\land x_2\land\ldots\land x_k)$
This proves :
Some dual couple children are true $\Rightarrow$ Parent is true

4) To prove : All nodes on graph marked true $\equiv$ Input $3-DNF$ expression is a tautology

Let us first prove : All nodes on graph marked true $\Rightarrow$ Input $3-DNF$ expression is a tautology

We assume that we have a case where all nodes are marked true, but the expression is not a tautology, and show it is impossible.
Firstly, any $3-DNF$ clauses present in the expression must have been marked true in the graph; same is true of all the children, and sub-children of those clauses.

Since the expression is known to not be a tautology, there must be some error in how we mark nodes true, i.e. we must be marking nodes true when they should not be marked. But the marking is done in only two ways.

The first way is directly marking from parent-to-child which happens if some parent is marked true. The second is marking a parent true if some dual couple children of its are true. Both methods are logically sound, as we have shown earlier. Hence there is no error in marking methods. So, it is impossible for all nodes to be marked true, if the expression is not a tautology.
Hence, All nodes on graph marked true $\Rightarrow$ Input $3-DNF$ expression is a tautology

Now we prove : All nodes on graph marked true $\Leftarrow$ Input $3-DNF$ expression is a tautology.

We assume we have a case where we have a tautological expression, but some nodes on the graph are marked false. This implies that we have some error in our marking method such that we fail to mark some nodes as true, even when they are. Obviously this cannot be the case when we are marking top-to-bottom, as is the case when some parent node is marked true. So, the error must exist with the dual-couple-child method.

The claim now is that the dual-couple-child method sometimes fails to mark true nodes.
We know that the dual-couple-child method marks nodes true only when such nodes have some dual couple children both marked true.

If this fails to mark some true nodes, then there must be certain cases where a node is true, without any of its dual couple children being true(at most one of the dual couple may be true, not both). But this is trivially impossible since we can take the true children, in a disjunction to see if they add up to the parent. This is trivial for dual couple children, but impossible if they're not both true. For example, let us take our parent node to be $(a\land b\land c)$ in an expression of $6$ variables, $\{a,b,c,d,e,f\}$
So, possible duals of $(a\land b\land c)$ are :
$(a\land b\land c\land d)true$, $(a\land b\land c\land\lnot d)false$
$(a\land b\land c\land e)false$, $(a\land b\land c\land\lnot e)false$
$(a\land b\land c\land f)false$, $(a\land b\land c\land\lnot f)true$

the $true/false$ next to them signifies their value. Take the disjunction of the true children :
$(a\land b\land c\land d)\lor(a\land b\land c\land\lnot f)$
$=(a\land b\land c)\land(d\lor\lnot f)$
Which trivially tells us that the true children have not added up to the parent, and that it is only possible when opposing literals are present, i.e. some dual couple children have to be true.
Therefore, our dual-couple-child method is correctly assigning truth values to the nodes. Hence it is impossible to have a tautological expression, which results in some nodes on the graph marked false.
Hence : All nodes on graph marked true $\Leftarrow$ Input $3-DNF$ expression is a tautology

Since we have proved both the left, and right implications, therefore :
All nodes on graph marked true $\equiv$ Input $3-DNF$ expression is a tautology

Clarifications :

a) Why is stopping at $6$ literals sufficient?

Ans : We start with a $3-DNF$ boolean expression, in $n$ variables. Each clause in our expression is a $\land$ of $3$ literals, and the expression is a $\lor$ of the clauses. Let our expression have $m$ clauses ($m\leq8\times{n\choose3}$). The topmost nodes of the graph my algorithm creates are all possible clauses with $3$ literals.

It is trivially noted that given a tautological expression, we can check that every possible clause is present(truth table verification), and given a non-tautological expression, we cannot mark every possible clause as present.

The algorithm's job is to derive clauses from the given expression. The clauses present in the expression are trivially present, and marked $true$ on the graph.
Now, every such trivially present clause is basically a set of assignments to the variables of the expression, such that the clause is true. For example, if our expression is of $5$ variables, $\{a,b,c,d,e\}$, and contains the clause $(b\land\lnot d\land\lnot e)$, then it is equivalent to the following assignments being true :

$(\lnot a\land b\land\lnot c\land\lnot d\land\lnot e)$
$(\lnot a\land b\land c\land\lnot d\land\lnot e)$
$(a\land b\land\lnot c\land\lnot d\land\lnot e)$
$(a\land b\land c\land\lnot d\land\lnot e)$

Now, every such clause (set of assignments) contains a subset that is valid for other clauses. For example, let us take the clause $(a\land b\land c)$. The subset, of the above assignments, that is valid for this clause is :

$(a\land b\land c\land\lnot d\land\lnot e)$
which is equal to : $(b\land\lnot d\land\lnot e)\land(a\land b\land c)$

Any trivially present clause carries a subset of assignments that are valid for other clauses, which can be accessed by intersecting (taking $\land$ of) the trivially present clause, and the clause whose assignments we seek.
The algorithm does that, by marking all children of true nodes also true. Since the nodes are simply $\land$ of some literals, we're actually marking subsets of assignments true.

Now, the reason why we stop at $6$ literals is this :
Each trivially present clause carries pieces of clauses which may be true, but are absent from the expression. These pieces can be accessed by taking $\land$ of the present clauses(one at a time), and any missing clause, whose pieces we are seeking. If the missing clause is true, then the pieces will add up to it, and vice versa.

One can think of it this way - since the intersections are a subset of valid assignments to variables, then an intersection of $3$ clauses, say $(a\land b\land c)\land(b\land c\land\lnot d)\land(b\land\lnot d\land e)$ which is equal to $(a\land b\land c\land\lnot d\land e)$, will be contained in the intersection $(a\land b\land c)\land(b\land c\land\lnot d)$, or of $(b\land c\land\lnot d)\land(b\land\lnot d\land e)$, or $(a\land b\land c)\land(b\land\lnot d\land e)$
So, the intersection of more than $2$ clauses is automatically marked true within intersection of $2$ clauses, and we need not go seek intersections of arbitrary number of clauses.

We can do this efficiently because our expression is a $\lor$ of clauses, and each subset of assignments of missing clauses are also in a disjunction, so smaller subsets of assignments(gotten from $\land$ of more than $2$ clauses) maybe be marked true more than once(theoretically), for each intersection of $2$ clauses they belong to, but that is not a botheration, as they are invisible to the algorithm(practically).

Then the algorithm joins these subsets together to form any missing clauses, using the dual-couple-child method. The way we build missing clauses is by patching together the intersections of the $2$ clauses each, and checking to see if their respective (overlapping) sets of assignments to variables sum up to some missing clause. Summing is possible because they're in a disjunction, and overlapping, or redundant/repeated assignments are simply reduced (idempotence).

A simple example - say we are given this expression :
$(a\land b\land d)\lor(\lnot a\land b\land c)$

$(a\land b\land d)$ has a child $(a\land b\land c\land d)$
$(\lnot a\land b\land c)$ has a child $(\lnot a\land b\land c\land d)$
Those two children are dual couple children of $(b\land c\land d)$
Hence we have derived a missing clause from intersections of it, with other clauses. All in all, we stop at $6$ literals because that is the maximum number of literals that can be found in a $\land$ of $2$ clauses.

Conclusion :

I have proved every step of the algorithm's verification process to be valid. Since the algorithm scans only up to clauses with $6$ variables each, no matter the number of variables in the expression, it scans over $8\times{n\choose3}+16\times{n\choose4}+32\times{n\choose5}+64\times{n\choose6}$ possible cases, which is in polynomial time.

  • 2
    $\begingroup$ If I'm reading your algorithm correctly, and I think I am, then I agree it is polynomial time, and that if the algorithm affirms then the statement is a tautology. What I can't work out or figure out from your writing yet is, why you think the converse, that if the input is a tautology then the algorithm affirms. And there should be a point where you say why stopping at 6 literals is sufficient (that is really the entire crux of the algorithm anyway). Anyway, that's the only non trivial reasoning of the algorithm, so some clarity there would be helpful. $\endgroup$ – DanielV Mar 13 at 10:47
  • $\begingroup$ @DanielV , I have added a 'Clarifications' sub-header, that addresses your question about why we stop at 6 literals. I think that the clarification, combined with the implication proof in step (4) under 'Proof of Validity' sub-header will answer both your questions, but I'm happy to specifically answer the other question if it doesn't. $\endgroup$ – Sohan Biswas Mar 13 at 13:39
  • 1
    $\begingroup$ "It is trivially noted that we can derive every possible 3 literal clause from a tautological expression, " What does "derive" mean here? It certainly isn't the case that a tautology implies an arbitrary clause. The converse is the case. And it isn't trivial that from a tautological input the algorithm marks every clause, if it even does. $\endgroup$ – DanielV Mar 14 at 10:03
  • $\begingroup$ @DanielV , what I mean 'derive' is that we can simply look up the truth table, and see that for a tautological expression, every clause will be marked true, since every output is true. I realize that in logic jargon the word 'derive' has a specific connotation. And, I wasn't talking about the algorithm at that point. If I was, I would have mentioned "It is trivially noted that the algorithm can derive.." This is an oversight, and I am editing the post, to use correct terminology. But yes, the algorithm does derive clauses, from the clauses present in the expression. $\endgroup$ – Sohan Biswas Mar 14 at 12:30

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.