EXERCISE

Parallelize the sequential version using Pthreads and other methods discussed
in the last exercise.  The sequential version already gives some hints.

The actual algorithm uses only non-static data stored in a 'Worker' structure,
such as the current assignment and the trail of assigned literals for
backtracking.  There is a global result part, which contains a stack of
learned units (negated failed literals). I would suggest to use this stack to
communicate failed literals between different work threads and otherwise let
the worker threads own and probe different subsets of literals.  You have to
be careful not to add learned units to the global learned unit stack which
were already found by other threads.  A strategy could be to always import
learned units before trying to push.  The formula is shared and propagation
only changes the state of a worker.  After all workers do not find new failed
literals anymore, they should have all the same permanent assigned variables
(a super set of the learned units).  Thus all but one can be reset.  The
remaining one will be used to simplify the formula formula and export all the
'implied' literals for printing.  Note, that failed literal probing is a
confluent preprocessing technique Thus the resulting simplified formula should
always be the same.

With 'make test' you can run some simple examples.  The provided big
compressed example CNFs can be use for testing how your parallel solution
scales.  Here is the output I got of the optimized sequential version.  There
are many other interesting examples try from the last SAT competition.

$ ./parfail examples/bin1.cnf -
c [parfail] Parfail Failed Literal Preprocessor
c [parfail]
c [parfail] reading DIMACS file from 'examples/bin1.cnf'
c [parfail] found 'p cnf 2 3' header
c [parfail] found 0 original unit clauses
c [parfail] using 12 threads as determined by 'sysconf'
c [parfail] removed 3 clauses (0 remain 0%)
c [parfail] formula SATISFIABLE (all variables assigned)
c [parfail]
c [parfail] writing simplified formula to '<stdout>'
p cnf 2 2
1 0
2 0
c [parfail]
c [parfail] propagations 2 (0.01 millions per second)
c [parfail] decisions 1 (2.0 propagations per decisions)
c [parfail] conflicts 1 (1.0 decisions per conflict)
c [parfail] learned 1 (100% learned unit clauses per conflict)
c [parfail] implied 2 (2.0 per learned unit clause)
c [parfail]
c [parfail] process time 0.000 seconds
c [parfail] wall clock time 0.000 seconds
c [parfail] utilization 43% for 12 threads


$ ./parfail examples/slp-synthesis-aes-bottom18-sc2011.cnf.xz
c [parfail] Parfail Failed Literal Preprocessor
c [parfail]
c [parfail] reading DIMACS file from 'examples/slp-synthesis-aes-bottom18-sc2011.cnf.xz'
c [parfail] found 'p cnf 36410 121578' header
c [parfail] found 1 original unit clauses
c [parfail] using 12 threads as determined by 'sysconf'
c [parfail] removed 21789 clauses (99789 remain 82%)
c [parfail] formula not solved
c [parfail]
c [parfail] not writing simplified CNF (use '-' to write to '<stdout>')
c [parfail]
c [parfail] propagations 176059990 (11.38 millions per second)
c [parfail] decisions 1816700 (96.9 propagations per decisions)
c [parfail] conflicts 2026 (0.0 decisions per conflict)
c [parfail] learned 2026 (100% learned unit clauses per conflict)
c [parfail] implied 5096 (2.5 per learned unit clause)
c [parfail]
c [parfail] process time 15.465 seconds
c [parfail] wall clock time 15.465 seconds
c [parfail] utilization 8% for 12 threads


$ ./parfail examples/Mario-t-hard-2_c18.cnf.xz 
c [parfail] Parfail Failed Literal Preprocessor
c [parfail]
c [parfail] reading DIMACS file from 'examples/Mario-t-hard-2_c18.cnf.xz'
c [parfail] found 'p cnf 35945 1228400' header
c [parfail] found 27 original unit clauses
c [parfail] using 12 threads as determined by 'sysconf'
c [parfail] removed 832 clauses (1227568 remain 100%)
c [parfail] formula not solved
c [parfail]
c [parfail] not writing simplified CNF (use '-' to write to '<stdout>')
c [parfail]
c [parfail] propagations 14505730 (0.27 millions per second)
c [parfail] decisions 222217 (65.3 propagations per decisions)
c [parfail] conflicts 34 (0.0 decisions per conflict)
c [parfail] learned 34 (100% learned unit clauses per conflict)
c [parfail] implied 98 (2.9 per learned unit clause)
c [parfail]
c [parfail] process time 54.388 seconds
c [parfail] wall clock time 54.388 seconds
c [parfail] utilization 8% for 12 threads


Note that the thread part is only there for your convenience.  It does
not do anything yet, except that corresponding command line options
can be parsed (the number of threads can be set):

$ ./parfaile -h
usage: parfail [-h] [<threads>] [<input> [<output>]]
