This article describes the solvability of HornSAT and CNFSAT. Unsatisfiable HornCNF have partially ordered set that is made by causation of each clauses. In this partially ordered set, Truth value assignment that is false in each clauses become simply connected space. Therefore, if we reduce CNFSAT to HornSAT, we must make such partially ordered set in HornSAT. But CNFSAT have correlations of each clauses, the partially ordered set is not in polynomial size. Therefore, we cannot reduce CNFSAT to HornSAT in polynomial size.
Download