A novel algorithm for solving the Decision Boolean Satisfiability Problem without algebra

TL;DR

This paper introduces a new algorithm for the Decision Boolean Satisfiability Problem that avoids algebraic methods, utilizing binary properties, parallel execution, and object-oriented design to improve efficiency.

Contribution

It presents a novel algebra-free algorithm leveraging binary properties and parallel execution, with proven upper complexity bounds for solving SAT problems.

Findings

Complexity upper bound of 2^{n-1} for the proposed algorithm

Uses expansion and simplification operations to avoid algebraic growth

Demonstrates efficiency improvements over algebra-based methods

Abstract

This paper depicts an algorithm for solving the Decision Boolean Satisfiability Problem using the binary numerical properties of a Special Decision Satisfiability Problem, parallel execution, object oriented, and short termination. The two operations: expansion and simplification are used to explains why using algebra grows the resolution steps. It is proved that its complexity has an upper bound of $2^{n-1}$ where $n$ is the number of logical variables of the given problem.