Goals

1. Mathematical Description of CompSAT
2. Complexity/Efficiency Analysis of Algorithms
3. SequenceL implementation
4. Time and Space Comparison to Traditional Parallel SAT solvers.
5. Map-Reduce implementation
6. Pthreads Implementation

(Minimum Target 1-4)

Time Line

1. 03/13/14 - 1 page Proposal (team members, problem statement, motivation, and proposed research)
2. 04/29/14 - 05/01/14 - Course Project Presentation
3. 05/06/14 - Final Deliverable
   1. Technical report: 4000 – 6000 words excluding references, summarizing your findings
      1. IEEE conference paper standard format, provided on Blackboard
      2. Follow scientific publications format: abstract/introduction/related work/your findings/experiments if any/conclusion
   2. Presentation: covering your research findings, details announced later
   3. All related files including source codes, figures, slides, etc.
   4. All files need to be in the source format (such as .tex/.doc instead of .pdf), and submit only one tarball/zipped file of all files on Blackboard

Work

Technical Report

1. Abstract
2. Introduction
3. Related Work
   1. Current Work On Parallelization Via Decomposition
   2. Current Work in Parallel SAT.
4. Your Findings
5. Experiments
6. Conclusions/Future Work

Presentation

1. Slides

Performance Comparison To Other SAT Solvers

1. Find Best Parallel Solvers
2. Get Them Running on DISCL Server
3. Collect Variety of Problems
4. Create Automated Testing Scripts and Report Generation Scripts.
   1. Max Memory Usage For Each Problem in Solver
   2. Time To Solution
   3. Profile of Processor Utilization Over Time.

Mathematical Description

1. Identify Types and Functions on Types.
2. Pseudocode For Each Function and Intuitive Description of Behavior
3. Complexity Analysis (Space and Time) on the functions

SequenceL Implementation

1. Find proper data structure representation of Math
2. Write Program
3. Identify any inherent inefficiencies due the semantics/implementation of SequenceL
4. Performance Metrics

MapReduce Implementation

1. Express the problem in MapReduce