Abstracts Engineering

Automatic Enumeration of Intervals of Partial Co-Clones

by Adam Shih

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.