  In the maximum satisfiability problem (MAX-SAT) we are given a propositional
formula in conjunctive normal form and have to find an assignment that
satisfies as many clauses as possible. We study the parallel parameterized
complexity of various versions of MAX-SAT and provide the first constant-time
algorithms parameterized either by the solution size or by the allowed excess
relative to some guarantee ("above guarantee" versions). For the dual
parameterized version where the parameter is the number of clauses we are
allowed to leave unsatisfied, we present the first parallel algorithm for
MAX-2SAT (known as ALMOST-2SAT). The difficulty in solving ALMOST-2SAT in
parallel comes from the fact that the iterative compression method, originally
developed to prove that the problem is fixed-parameter tractable at all, is
inherently sequential. We observe that a graph flow whose value is a parameter
can be computed in parallel and use this fact to develop a parallel algorithm
for the vertex cover problem parameterized above the size of a given matching.
Finally, we study the parallel complexity of MAX-SAT parameterized by the
vertex cover number, the treedepth, the feedback vertex set number, and the
treewidth of the input's incidence graph. While MAX-SAT is fixed-parameter
tractable for all of these parameters, we show that they allow different
degrees of possible parallelization. For all four we develop dedicated parallel
algorithms that are constructive, meaning that they output an optimal
assignment - in contrast to results that can be obtained by parallel
meta-theorems, which often only solve the decision version.
