On non-canonical solving the Satisfiability problem

TL;DR

This paper explores a non-canonical approach to solving the SAT problem by counting false clauses, identifying conditions for efficient solutions, and analyzing the complexity based on clause structure.

Contribution

It introduces a counting-based method for SAT solving and characterizes problem instances where the method is efficient or exponential.

Findings

Efficient solution when clauses have pairwise contrary literals.

Exponential complexity with long chains of non-contrary literals.

Provides conditions for the method's applicability.

Abstract

We study the non-canonical method for solving the Satisfiability problem which given by a formula in the form of the conjunctive normal form. The essence of this method consists in counting the number of tuples of Boolean variables, on which at least one clause of the given formula is false. On this basis the solution of the problem obtains in the form YES or NO without constructing tuple, when the answer is YES. It is found that if the clause in the given formula has pairwise contrary literals, then the problem can be solved efficiently. However, when in the formula there are a long chain of clauses with pairwise non-contrary literals, the solution leads to an exponential calculations.