Two-Dimensional Indirect Binary Search for the Positive One-in-Three Satisfiability Problem

TL;DR

This paper introduces a novel 2-dimensional binary search algorithm to efficiently solve the positive one-in-three satisfiability problem, avoiding exponential complexity in assignment enumeration.

Contribution

It presents a new algorithm leveraging 2D binary search to decide satisfiability without exponential assignment enumeration.

Findings

Efficient decision of Pos1in3SAT for all formulas

Avoids exponential assignment enumeration

Uses 2D binary search method

Abstract

In this paper, we propose an algorithm for the positive one-in-three satisfiability problem (Pos1in3SAT). The proposed algorithm can efficiently decide the existence of a satisfying assignment in all assignments for a given formula by using a 2-dimensional binary search method without constructing an exponential number of assignments.