Staff View
Width-parameterized SAT: time-space tradeoffs,

Descriptive

TypeOfResource
Text
TitleInfo
Title
Width-parameterized SAT: time-space tradeoffs,
Name (authority = orcid); (authorityURI = http://id.loc.gov/vocabulary/identifiers/orcid.html); (type = personal); (valueURI = http://orcid.org/0000-0002-0650-028X)
NamePart (type = family)
Allender
NamePart (type = given)
Eric
Affiliation
Computer Science (New Brunswick), Rutgers University
Role
RoleTerm (authority = marcrt); (type = text)
author
Name (type = personal)
NamePart (type = family)
Chen
NamePart (type = given)
Shiteng
Affiliation
Tsinghua University
Role
RoleTerm (authority = marcrt); (type = text)
author
Name (type = personal)
NamePart (type = family)
Lou
NamePart (type = given)
Tiancheng
Affiliation
Google
Role
RoleTerm (authority = marcrt); (type = text)
author
Name (type = personal)
NamePart (type = family)
Papakonstantinou
NamePart (type = given)
Periklis
Affiliation
Tsinghua University
Role
RoleTerm (authority = marcrt); (type = text)
author
Name (type = personal)
NamePart (type = family)
Tang
NamePart (type = given)
Bangsheng
Affiliation
Hulu
Role
RoleTerm (authority = marcrt); (type = text)
author
Name (authority = RutgersOrg-Department); (type = corporate)
NamePart
Computer Science (New Brunswick)
Name (authority = RutgersOrg-School); (type = corporate)
NamePart
School of Arts and Sciences (SAS) (New Brunswick)
Genre (authority = RULIB-FS)
Article, Refereed
Genre (authority = NISO JAV)
Version of Record (VoR)
OriginInfo
DateCreated (encoding = w3cdtf); (keyDate = yes); (qualifier = exact)
2014
Publisher
theoryofcomputing.org
Abstract (type = Abstract)
Alekhnovich and Razborov (2002) presented an algorithm that solves SAT on instances ϕ of size n and tree-width TW(ϕ), using time and space bounded by 2O(TW(ϕ))nO(1). Although several follow-up works appeared over the last decade, the first open question of Alekhnovich and Razborov remained essentially unresolved: Can one check satisfiability of formulas with small tree-width in polynomial space and time as above? We essentially resolve this question, by (1) giving a polynomial space algorithm with a slightly worse run-time, (2) providing a complexity-theoretic characterization of bounded tree-width SAT, which strongly suggests that no polynomial-space algorithm can run significantly faster, and (3) presenting a spectrum of algorithms trading off time for space, between our PSPACE algorithm and the fastest known algorithm.

First, we give a simple algorithm that runs in polynomial space and achieves run-time 3TW(ϕ)lognnO(1), which approaches the run-time of Alekhnovich and Razborov (2002), but has an additional log n factor in the exponent. Then, we conjecture that this annoying log n factor is in general unavoidable.

Our negative results show our conjecture true if one believes a well-known complexity assumption, which is the SC ≠ NC conjecture and its scaled variants. Technically, we base our result on the following lemma. For arbitrary k, SAT of tree-width logkn is complete for the class of problems computed by circuits of logarithmic depth, semi-unbounded fan-in and size 2O(logkn) (SAC1 when k=1). Problems in this class can be solved simultaneously in time-space (2O(logk+1n),O(logk+1n)), and also in (2O(logkn), 2O(logkn)). Then, we show that our conjecture (for SAT instances with poly-log tree-width) is equivalent to the question of whether the small-space simulation of semi-unbounded circuit classes can be sped up without incurring a large space penalty. This is a recasting of the conjecture that SAC1 (and even its subclass NL) is not contained in SC.

Although we cannot hope for an improvement asymptotically in the exponent of time and space, we introduce a new algorithmic technique which trades constants in the exponents: for each ε with 0<ε<1, we give an algorithm in time-space
(31.441(1−ε)TW(ϕ)log|ϕ||ϕ|O(1),22εTW(ϕ)|ϕ|O(1)).
We systematically study the limitations of our technique for trading off time and space, and we show that our bounds are the best achievable using this technique.
Language
LanguageTerm (authority = ISO 639-3:2007); (type = text)
English
PhysicalDescription
InternetMediaType
application/pdf
Extent
43 p.
Subject (authority = local)
Topic
Complexity theory
Subject (authority = LCSH)
Topic
Algorithms
Subject (authority = local)
Topic
Complexity classes
Subject (authority = local)
Topic
Circuit complexity
Subject (authority = local)
Topic
Parametrized complexity
Subject (authority = local)
Topic
Nondeterminism
Subject (authority = local)
Topic
CNF-DNF formulas
Subject (authority = local)
Topic
Boolean formulas
Subject (authority = local)
Topic
Completeness
Subject (authority = local)
Topic
Time-space tradeoff
Subject (authority = local)
Topic
Treewidth (Graph theory)
Subject (authority = local)
Topic
Pathwidth (Graph theory)
Extension
DescriptiveEvent
Type
Citation
DateTime (encoding = w3cdtf)
2014
AssociatedObject
Name
Theory of Computing
Type
Journal
Relationship
Has part
Detail
297-339
Identifier (type = volume and issue)
10(12)
Reference (type = url)
http://dx.doi.org/doi:10.4086/toc.2014.v010a012
Extension
DescriptiveEvent
Type
Grant award
AssociatedEntity
Role
Funder
Name
National Science Foundation
AssociatedEntity
Role
Originator
Name
Eric Allender
AssociatedObject
Type
Grant number
Name
CCF-1064785
Extension
DescriptiveEvent
Type
Grant award
AssociatedEntity
Role
Funder
Name
National Science Foundation
AssociatedEntity
Role
Originator
Name
Eric Allender
AssociatedObject
Type
Grant number
Name
CCF-0832787
Extension
DescriptiveEvent
Type
Grant award
AssociatedEntity
Role
Funder
Name
National Basic Research Program of China
AssociatedObject
Type
Grant number
Name
2011CBA00300
AssociatedObject
Type
Grant number
Name
2011CBA00301
Extension
DescriptiveEvent
Type
Grant award
AssociatedEntity
Role
Funder
Name
National Natural Science Foundation of China
AssociatedObject
Type
Grant number
Name
61033001
AssociatedObject
Type
Grant number
Name
61061130540
AssociatedObject
Type
Grant number
Name
61073174
AssociatedObject
Type
Grant number
Name
61250110577
Note (type = general note)
Licensed under a Creative Commons Attribution License (CC-BY) http://creativecommons.org/licenses/by/3.0/
Note (type = peerReview)
Peer reviewed
Subject (authority = LCSH)
Topic
Computational complexity
RelatedItem (type = host)
TitleInfo
Title
Allender, Eric
Identifier (type = local)
rucore30165700001
Location
PhysicalLocation (authority = marcorg); (displayLabel = Rutgers, The State University of New Jersey)
NjNbRU
Identifier (type = doi)
doi:10.7282/T3N87CM1
Genre (authority = ExL-Esploro)
Journal Article
Back to the top

Rights

RightsDeclaration (AUTHORITY = FS); (ID = rulibRdec0004)
Copyright for scholarly resources published in RUcore is retained by the copyright holder. By virtue of its appearance in this open access medium, you are free to use this resource, with proper attribution, in educational and other non-commercial settings. Other uses, such as reproduction or republication, may require the permission of the copyright holder.
Copyright
Status
Copyright protected
Availability
Status
Open
Reason
Permission or license
RightsEvent
Type
Permission or license
AssociatedObject
Type
License
Name
Multiple author license v. 1
Detail
I hereby grant to Rutgers, The State University of New Jersey (Rutgers) the non-exclusive right to retain, reproduce, and distribute the deposited work (Work) in whole or in part, in and from its electronic format, without fee. This agreement does not represent a transfer of copyright to Rutgers.Rutgers may make and keep more than one copy of the Work for purposes of security, backup, preservation, and access and may migrate the Work to any medium or format for the purpose of preservation and access in the future. Rutgers will not make any alteration, other than as allowed by this agreement, to the Work.I represent and warrant to Rutgers that the Work is my original work. I also represent that the Work does not, to the best of my knowledge, infringe or violate any rights of others.I further represent and warrant that I have obtained all necessary rights to permit Rutgers to reproduce and distribute the Work and that any third-party owned content is clearly identified and acknowledged within the Work.By granting this license, I acknowledge that I have read and agreed to the terms of this agreement and all related RUcore and Rutgers policies.
RightsHolder (type = personal)
Name
FamilyName
Allender
GivenName
Eric
Role
Copyright holder
RightsHolder (type = personal)
Name
FamilyName
Chen
GivenName
Shiteng
Role
Copyright holder
RightsHolder (type = personal)
Name
FamilyName
Lou
GivenName
Tiancheng
Role
Copyright holder
RightsHolder (type = personal)
Name
FamilyName
Papakonstantinou
GivenName
Periklis
MiddleName
A.
Role
Copyright holder
RightsHolder (type = personal)
Name
FamilyName
Tang
GivenName
Bangsheng
Role
Copyright holder
Back to the top

Technical

RULTechMD (ID = TECHNICAL1)
ContentModel
Document
Back to the top
Version 8.3.13
Rutgers University Libraries - Copyright ©2020