Worst-Case Upper Bound for (1, 2)-QSAT

TL;DR

This paper introduces an exact algorithm for (1, 2)-QSAT and establishes a worst-case upper bound of O(1.4142^m), advancing theoretical understanding of this subclass of QSAT.

Contribution

The paper provides the first known worst-case upper bound for (1, 2)-QSAT by developing an exact algorithm and analyzing its complexity.

Findings

Established a worst-case upper bound of O(1.4142^m) for (1, 2)-QSAT

Developed an exact algorithm for solving (1, 2)-QSAT

Contributed to the theoretical analysis of a subclass of QSAT

Abstract

The rigorous theoretical analysis of the algorithm for a subclass of QSAT, i.e. (1, 2)-QSAT, has been proposed in the literature. (1, 2)-QSAT, first introduced in SAT'08, can be seen as quantified extended 2-CNF formulas. Until now, within our knowledge, there exists no algorithm presenting the worst upper bound for (1, 2)-QSAT. Therefore in this paper, we present an exact algorithm to solve (1, 2)-QSAT. By analyzing the algorithms, we obtain a worst-case upper bound O(1.4142m), where m is the number of clauses.