Parallel failed literal preprocessor for SAT formulas in DIMACS format.

This program takes a CNF in DIMACS format and simplifies it with failed
literal probing until completion.  This is an old well-known technique
from look-ahead solvers and works as follows.

Consider this formula in DIMACS format with 2 variables and 3 clauses:

  c this is a comment line
  p cnf 2 3
  1 2 0
  -1 2 0
  1 -2 0

The header 'p cnf 2 3' gives the number of variables ('2') and clauses ('3').
The rest of the file consists of zero terminated clauses.  Note literals are
encoded as integers.  As formula you could think of this CNF as follows:

  (x1 | x2) & (!x1 | x2) & (x1 | !x2)

On this formula failed literal probing works as follows:

We assume 'x2=true' then the third clauses forces 'x1=true' and the remaining
clauses are satisfied.  Thus we did not learn anything yet and reset both
variable to be unassigned.  The same happens if we assume 'x1=true'.
No assume 'x2=false'.  Then the first clause forces 'x1=true' and we
get that the second clause and thus the whole formula is 'false'.  There fore
'x2' can not be 'false' in any solution to this formula.  It has to be 'true'.
We permanently assign 'x2' to 'true' which in turn also forces 'x1' to be
permanently set to 'true'.  Now all variables are forced to a value and the
formula is satisfiable.  Thus this is only satisfying assignment.

The result of failed literal probing returns the forced assignment as clauses
and simplifies the remaining clauses (none in the example) accordingly.

  p cnf 2 2
  1 0
  2 0

The complete algorithm is not that complicated:

For all literals L in the formula, assume L, i.e., set L to 'true' and then
propagate it.  Propagation means to deduce all implied literals. More
specifically if there is a clause in the formula which has all but one of its
literals set to 'false', then the remaining one has to be set to 'true'.

If propagation leads to a conflict (all literals of a clause are assigned to
'false'), then the assumption that the formula can be satisfiable while L is
'true' is wrong.  Then  L is called a 'failed literal' and we can permanently
set L to 'false'.  If on the other hand propagation of the assumption that L
is 'true' does not lead to a conflict then we have to backtrack and unassign
the assumption and all literals implied by it.

If a failed literal is found and set to 'false', we need to propagate this
learned fact (the unit clause which consist of the negation of 'L'). This in
turn might yield additional implied literals (and even lead to a conflict in
which case the formula is proven to be unsatisfiable).  In any case, after a
failed literal has been found, the formula becomes simpler and in principle we
need to probe all literals again.

This procedure has cubic complexity since (A) we have to repeat until no more
failed literals are found, (B) try all literals and (C) propagate each.

There is one optimization implemented in 'parfail' which avoids redundant
probing of literals (assuming and propagating a literal).  If a literal
L was assigned to 'true' and propagated and that propagation did not lead
to a conflict, then this literal does not have to be assumed to be 'true'
before another failed literal is found.  This prevents one of the linear
factors in the complexity analysis above and renders the procedure quadratic.
In order to implement this optimization we use virtual time stamps of when a
literal was propagated without conflict, measured in the number of failed
literals found so far before this propagation.

Even though the linear factor (C) is in many formulas much smaller than
the worst cases (almost all variables become assigned), there are instances
where this algorithm even with the described optimization takes too much
time and therefore it is a prefect target for parallelization.
