A Fast Algorithm for SAT in Terms of Formula Length

Speaker:

Junqiang Peng (University of Electronic and Science Technology of China)

Time:

10:00-12:00 (Time in Beijing)
14:00-16:00 (Time in Auckland)
June 4, 2021 (Friday)

VooVmeeting:

Link: https://meeting.tencent.com/s/2p05iZpS1RvT

ID: 973 577 922 Password: 1949

Venue:

Main Building

Abstract:

The CNF satisfiability problem is defined as follows: given a CNF formula $F$ , decide if there exists a truth-value assignment to variables such that the formula evaluates to true. In this talk, I will introduce an algorithm that solves the general CNF satisfiability problem in $O^*(1.0646^L)$ time, where $L$ is the length of the input CNF-formula (i.e., the total number of literals in the formula). This algorithm is a standard branch-and-search algorithm analyzed by using the measure-and-conquer method. It improves the running time bound $O^*(1.0652^L)$ given by Chen and Liu in 2009.