This is an algorithm I came up with, that seeks to solve the ‘Boolean Tautology Problem’ in polynomial time, using $ 3-DNF$ clauses. I am posting this algorithm here seeking advice, and correction, if any can be provided.

I treat boolean variables as sets. The set itself denotes the variable to be $ true$ , and complement of the set denotes the variable to be $ false$ . $ \bigcap$ of sets denotes $ \land(AND)$ of the variables, and $ \bigcup$ of sets denotes $ \lor(OR)$ of the variables.

The sets are arranged so that they perfectly intersect, and every section is a boolean expression. Here are some examples(using upto $ 4$ sets/variables, since drawing more clutters the picture) :

$ 3$ variable example :

$ 4$ variable example :

Now, each clause in $ 3-DNF$ has $ 3$ literals(using the exact $ 3-DNF$ version). So, there are only $ 4$ possible cases for the literals :

1) All $ 3$ literals are positive – $ (a\land b\land c)$

2) $ 1$ literal negative, rest positive – $ (\lnot i\land j\land k)$

3) $ 2$ literals negative, remaining positive – $ (\lnot p\land\lnot q\land r)$

4) All $ 3$ literals negative – $ (\lnot x\land\lnot y\land\lnot z)$

Any $ 3-DNF$ expression consists of $ \lor$ of these $ 4$ kinds of clauses, and each clause itself is a subset of our total set of variables. Each clause highlights a certain part of the Venn Diagram of the set of variables. So, a tautological expression will have clauses that highlight the entirety of the Venn Diagram. The important part is that using $ 3-DNF$ , the total set can be highlighted **only** using these specific sets, and not just any arbitrarily small subset.

The way the algorithm works is by highlighting all such clauses found within the expression, **and** their intersections with all such other subsets. The reasoning is that since only the $ 4$ clause cases can highlight their respective subsets in the Venn Diagram, upon highlighting one such clause, other clauses which may intersect with it also have portions that need to be highlighted. Since the possible highlighter subsets are limited to the $ 4$ kinds of clauses, we just need to check intersections between them, two at a time.

**Implementation :**

The implementation would be as follows(given a $ 3-DNF$ expression with $ n$ variables) :

1) Create a graph, starting with all possible clauses as beginning nodes.(total number of clauses $ =8\times {n\choose 3}$ )

2) Create a set of children nodes for each parent node, by adding one more literal each to the parent clause.

3) For each such child, there is a dual child which has the negation of that literal.

4) Using these children as parents, follow procedure (2).

5) Continue this process until you have exhausted your variables, or have $ 6$ literals in your last created children nodes (intersection between two $ 3-DNF$ clauses).

6) A child can have multiple parents.

An example case of graph building is shown below. The directed arrow represents parent-to-child relation. Dual children are attached to the same relation for ease of view. The graph shown is partially built, so as to not clutter.

** Solving :**

Now, on to the solving the $ 3-DNF$ expression :

1) Scan through the expression and take up each clause.

2) For each clause, mark the corresponding node as true.

3) If a parent node is true, all child nodes are marked true.

4) If both dual children are true, the parent is marked true.

5) If every node is marked true, the expression is a tautology, otherwise not.

**Remarks :**

Step (3) of the solver ensures that if a particular clause is true, then all possible intersections of it, and any other clause also gets marked true. Since the graph stops building child nodes once those nodes have $ 6$ literals, we deal only with cases of intersection of two clauses. E.g.

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

It should be obvious that if common literals exist in these clauses then it results in less than $ 6$ literals in the child clause. We do not need to check for intersections of more than two clauses, since the intersection will be contained within the intersection of two clauses each, since each true assignment is in disjunction with others.

**Time Complexity :**

Since we stop at child nodes with $ 6$ literals each, no matter the value of $ n$ , the number of variables, it is obviously polynomially bounded.

**Closing words :**

Please read through the method, and do tell me if there are any errors, or logical leaps that I made, or if the algorithm does actually work, which would be great.

EDIT : Added some subtitles for paragraphs.