Assignment 3 (June 19)

This task is about producing a ‘pthread’ parallel version of a model counter. The sequential version ‘decncnt’ written in C is provided in the Moodle together with a test suite and benchmarks in DIMACS format, which is the standard format for SAT solvers.

To build the sequential version use the ‘configure’ script, which has two options

• ‘-g’ to compile with assertion checking

• ‘-l’ to include and enable logging code

Then issue ‘make’ to build the binary.

The parallel version should be implemented in C (or C++) using ‘pthreads’ or ‘cilk’ / ‘lace’ and can optionally also use atomic primitives.

The main challenges are (1) how to schedule recursive calls of ‘solve’, and (2) how to split the solver state into separate parts for each thread (‘vals’, ‘clauses’, ‘next’, ‘search’, ‘level’, ‘trail’).

The permutation benchmarks like ‘perm10.cnf’ are ideal to measure speed-up. Beside those in the test-suite you can use ‘cnfs/permute.c’ to generate larger ones.