Automatic Enumeration of Intervals of Partial Co-Clones

by Adam Shih

Institution: Linköping University
Year: 2016
Keywords: Engineering and Technology; Electrical Engineering, Electronic Engineering, Information Engineering; Other Electrical Engineering, Electronic Engineering, Information Engineering; Teknik och teknologier; Elektroteknik och elektronik; Annan elektroteknik och elektronik; Computer science; Datavetenskap
Posted: 02/05/2017
Record ID: 2134340
Full text PDF: http://urn.kb.se/resolve?urn=urn:nbn:se:liu:diva-127982


Computer scientists are curious about the complexity relationship between different kinds of NP-complete SAT problems. In order to understand the complexity relationship between SAT problems, we decided to correspond SAT problems to a kind of algebra called partial co-clones. Each SAT problem can be represented by a set of Boolean relations. Partial co-clones are Boolean relations enumerated under quantifier-free primitive positive definition. If SAT(R2) is included in SAT(R1)’s partial co-clones, SAT(R1) cannot be solved faster than SAT(R2). We used this kind of relationship to get a partial order of the worst-case time complexity of SAT problems. Partial co-clones are complicated, and we do not really understand the structure of partial co-clones. Therefore, it would have been easier to explore parts of their structures automatically with the help of current computers. We strived to develop a scalable efficient program exploiting parallel computers. We started with exploring sequential optimization methods including data structure design, Depth First Search combination, Inverse SAT, and tried to partition the searching process equally to each computing node. We proposed an easy but efficient, scalable implementation that could handle problem size less than O(280) with memory cost equal to O(n). Given enough computing nodes, we could achieve performance close to linear speedup.