Ruiwen Chen (SFU)
15/11/13 12:30 Talks
An improved deterministic #SAT algorithm for small De Morgan formulas
Speaker:
Ruiwen Chen (Simon Fraser University, Computing Science)
Abstract:
We give a deterministic #SAT algorithm for de Morgan formulas of size up to $n^{2.63}$, which runs in time $2^{n-n^{\Omega(1)}}$. This improves upon the deterministic #SAT algorithm of Chen, Kabanets, and Kolokolova, which has similar running time but works only for formulas of size less than $n^{2.5}$.
Our new algorithm is based on the shrinkage of de Morgan formulas under random restrictions, shown by Paterson and Zwick. We prove a concentrated and constructive version of their shrinkage result. Namely, we give a deterministic polynomial-time algorithm that selects variables in a given de Morgan formula so that, with high probability over the random assignments to the chosen variables, the original formula shrinks in size, when simplified using a deterministic polynomial-time formula-simplification algorithm.
This is a joint work with Valentine Kabanets and Nitin Saurabh.
Date:
Friday, November 15, 2013
Time:
12:30 pm - 1:30 pm
Location:
TASC1 Building, Room No. 9204, Simon Fraser University, Burnaby
Ruiwen Chen (Simon Fraser University, Computing Science)
Abstract:
We give a deterministic #SAT algorithm for de Morgan formulas of size up to $n^{2.63}$, which runs in time $2^{n-n^{\Omega(1)}}$. This improves upon the deterministic #SAT algorithm of Chen, Kabanets, and Kolokolova, which has similar running time but works only for formulas of size less than $n^{2.5}$.
Our new algorithm is based on the shrinkage of de Morgan formulas under random restrictions, shown by Paterson and Zwick. We prove a concentrated and constructive version of their shrinkage result. Namely, we give a deterministic polynomial-time algorithm that selects variables in a given de Morgan formula so that, with high probability over the random assignments to the chosen variables, the original formula shrinks in size, when simplified using a deterministic polynomial-time formula-simplification algorithm.
This is a joint work with Valentine Kabanets and Nitin Saurabh.
Date:
Friday, November 15, 2013
Time:
12:30 pm - 1:30 pm
Location:
TASC1 Building, Room No. 9204, Simon Fraser University, Burnaby