A Fast Algorithm for SAT in Terms of Formula Length
- Speaker
- Junqiang Peng
- Affiliation
- University of Electronic and Science Technology of China
- Date
- Time
- – Asia/Shanghai
- 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.
Schedule
- 10:00-12:00 (Time in Beijing)
- 14:00-16:00 (Time in Auckland)
- June 4, 2021 (Friday)
Online Meeting
Link: https://meeting.tencent.com/s/2p05iZpS1RvT
ID: 973 577 922 Password: 1949