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.
- 5. Juni 2018, 08:19
- 5. Juni 2018, 12:01