Solvability of HornSAT and CNFSAT

TL;DR

This paper investigates the structural differences between HornSAT and CNFSAT, demonstrating that CNFSAT cannot be polynomially reduced to HornSAT due to the complexity of their clause correlations.

Contribution

It introduces a novel approach using partially ordered sets to analyze the solvability and reduction limitations between HornSAT and CNFSAT.

Findings

CNFSAT has clause correlations that prevent polynomial reduction to HornSAT.

Unsatisfiable HornCNF can be represented by a simple connected space.

Polynomial size reduction from CNFSAT to HornSAT is impossible.

Abstract

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.