Poster Reception-Alef Parallel SAT Solver for HPC Hardware



Publication Source: The ACM/IEEE SC Conference on High Performance Networking and Computing, Tampa, FL, USA, 2006

Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications, including formal verification of both hardware and software, mathematics, and planning. However, solver performance, measured in terms of speed and maximum problem size, is a limiting factor to the application of SAT to real-world problems. We are developing a parallel SAT solver, Alef, to take advantage of HPC hardware.The Alef parallel SAT solver utilizes algorithms and heuristics that improve its performance over existing approaches. We are developing the solver to run well on commercially available HPC hardware. Our analysis shows that our algorithms combined with the low message latency of supercomputers are likely to produce a significant performance improvement over existing solvers in terms of speed and maximum problem size. Our poster will describe the algorithms we are using, illustrate our approach to problem partitioning, and present our performance analysis to date.
Google Scholar    Article

R-Stream: A Parametric High Level Compiler



Publication Source: High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA, 2006

This presentation describes the R-Stream compiler. The motivation of high level, source to source optimization is described. The process or raising code to the Generalized Dependence Graph (GDG) is identified, and then the techniques for optimization within the GDG.  Finally, the techniques for code generation from the GDG - polyhedral scanning, and importantly, the process of generating "human readable" C to allow the low level compiler to optimize.
Google Scholar    Article

Enabling Cognitive Architectures for UAV Mission Planning



Publication Source: The High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA, (Best papers award session), September, 2006

The operational performance desired for autonomous vehicles in the battlefield requires new approaches in algorithm design and computation. Our design, Polymorphic Cognitive Agent Architecture (PCAA), is a hardware-software system that supports the requirements for implementing a dynamic multi-unmanned aerial vehicle (UAV) mission planning application using cognitive architectures. We describe the requirements for our application, and discuss the challenges of using current “non-cognitive” algorithms to solve this problem and the reasons this motivates our experiment.
Google Scholar    Article

Runtime Verification of Cognitive Applications



Publication Source: The 10th Annual High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA

Cognitive systems have been the subject of much research, and are increasingly of interest in embedded systems. However, cognitive applications have unique characteristics that make them challenging to verify, validate, and debug. A cognitive application by definition makes intelligent decisions – if it were possible to formally and precisely express its behavior under all circumstances, the cognitive system would not need to be “cognitive.”
Google Scholar    Article

Salt & Alef: Unlocking the Power of Boolean Satisfiability



Publication Source: The 10th Annual High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA, 2006

Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications relevant to the HPEC community. These applications include formal verification, analysis of numerical precision for embedded pipelines, and cognitive reasoning. However, solver performance, measured in terms of speed and maximum problem size, is a limiting factor to the application of SAT to real-world problems. We are developing a constraint language, translation tool, and parallel SAT solver to significantly mitigate the impact of these limitations.
Google Scholar    Article

1 19 20 21 22