arXiv · 1304.2026
Resolution structure in HornSAT and CNFSAT
Abstract
This article describes about the difference of resolution structure and size between HornSAT and CNFSAT. We can compute HornSAT by using clauses causality. Therefore we can compute proof diagram by using Log space reduction. But we must compute CNFSAT by using clauses correlation. Therefore we cannot compute proof diagram by using Log space reduction, and reduction of CNFSAT is not P-Complete.
Explore related subjects
Keep this discovery
Koji Kobayashi. 2013-04-07. Resolution structure in HornSAT and CNFSAT. https://arxiv.org/abs/1304.2026
Cite the original work for its findings. Save a collection to share your selection of sources.