Parallel algorithm for 3-Satisfiability Problem (Jianan Hao)

The included source code implements a parallel solution to an input instance of the 3-Satisfiability problem, as described in the included problem description text file. The input form of the Boolean expression is conjunctive normal form. 

The included write-up describes a depth-first search algorithm to find a solution. As variables are given either a TRUE or FALSE assignment, an attempt is made to reduce the number of variables in clauses based on current settings of variables already examined along the current search path. Windows Threads is used to implement the parallelism; Intel Threading Building Blocks (TBB) and OpenMP were considered but discarded for cited reasons. The code was intended for Windows OS and includes Microsoft Visual Studio solution and project files to build the application.
DISCLAIMER: This code is provided by the author as a submitted contest entry, and is intended for educational use only. The code is not guaranteed to solve all instances of the input data sets and may require modifications to work in your own specific environment.

There are downloads available under the Creative Commons License license. Download Now
For more complete information about compiler optimizations, see our Optimization Notice.