mts: a light framework for parallelizing tree search codes
David Avisa and Charles JordanbaSchool of Informatics, Kyoto University, Kyoto, Japan and School of Computer Science,
McGill University, Montréal, Québec, Canada; b Graduate School of Information Science andTechnology, Hokkaido University, Japan
ARTICLE HISTORY
Compiled October 29, 2019
ABSTRACTWe describe mts, a generic framework for parallelizing certain types of tree search
programs including reverse search, backtracking, branch and bound and satisfiability
testing. It abstracts and generalizes the ideas used in parallelizing lrs, a reverse searchcode for vertex enumeration. mts supports sharing information between processes
which is important for applications such as satisfiability testing and branch-andbound. No parallelization is implemented in the legacy single processor programs
minimizing the changes needed and simplifying debugging. mts is written in C, uses
MPI for parallelization and can be used on a network of computers. We give four examples of reverse search codes parallelized by using mts: topological sorts, spanning
trees, triangulations and Galton-Watson trees. We also give a parallelization of twocodes for satisfiability testing. We give experimental results comparing the parallelcodes with other codes for the same problems.
KEYWORDS
reverse search; parallel processing; topological sorts; spanning trees; triangulations;satisfiability testing
AMS CLASSIFICATION
90C05

1. Introduction
Parallel programming is a vast area and there is a great amount of literature on it (see,e.g., Mattson et al. [36]). Topics include architecture, communication, data sharing,interrupts, deadlocks, load balancing, and the distinction between shared memory anddistributed computing. This is all essential for building an efficient parallel algorithm
from scratch.
Our starting point was different. We had a large complex code, lrs, developed overabout 20 years and tested extensively, which solved vertex/facet enumeration problems. These problems are notoriously hard and running times often take weeks orlonger. The underlying algorithm, reverse search, was clearly suitable for parallelization. Nevertheless, the mathematical intricacy of the underlying problem rendered
the algorithmic engineering of direct parallelization daunting. This led us to consider
building all of the parallelization into a wrapper, making only minor changes to the
CONTACT C. Jordan. Email: skip@ist.hokudai.ac.jp

underlying lrs code. There followed a series of implementations resulting ultimately inthe authors’ mplrs code [8]. The key features of mplrs are: (a) there is no parallel code
inside lrs, (b) parallel threads execute lrs on non-overlapping subproblems, (c) there isno communication between threads except at the beginning and end of a subproblem
execution, (d) the computation can be distributed over a cluster of computers, and(e) the wrapper is directly inserted into the lrs library. Most of the topics in parallel computation mentioned above are not major issues in this restricted framework.
The exception is load balancing for which we use a particularly simple method which
consists of budgeting the number of nodes evaluated in a subproblem.
It seemed likely that similar results could be obtained for other algorithms basedon reverse search1 or similar easily parallelizable tree search methods. Many suchsequential codes exist, so designing custom wrappers for each is not desirable. Our goal
was to build a single generic wrapper that could be used, with little if any modification,
to do the required parallelization while maintaining features (a)–(e) described above.
This resulted in mts, presented here. The current implementation2 uses MPI andworks on clusters of machines. The mts framework is more general than mplrs in thatit allows the sharing of data obtained by subproblems, but still maintains the absenceof communication between threads. This widens its application to more general tree
search problems such as satisfiablility testing and branch and bound.
In Section 2 we survey the literature on parallelizing reverse search codes. We thendescribe our general approach in Section 3 and apply it to reverse search in Section 4.
We give four examples: generating topological sorts, spanning trees of a graph, highdimensional triangulations and Galton-Watson trees. This latter problem was chosen
as the trees generated are unbalanced, which is a challenge for parallelization. They
allow an analysis of the major source of overhead in mts and its dependence on the
crucial budgeting parameter which will be described in Section 3.
Tree search has wide uses, of which enumeration is just one example. In fact it isa very specific example as all nodes in the enumeration tree are visited. Two otherimportant uses of tree search are satisfiability testing and branch and bound. Herethe goal is not to search the entire tree but to prune subtrees when possible. The
tree generated in these cases will normally differ depending on the choices made atearly stages and the sharing of information learned during the computation. The mts
framework includes support for sharing data between processes and can be applied tothese types of problems. As an example we present a parallelization for satisfiability
testing in Section 5, demonstrating how little of the original code needs to be changed.
In Section 6 we give computational results for parallelized reverse search and satisfiability codes. This is followed in Section 7 by a discussion of how to evaluate theexperimental results, the situation being quite different for enumeration problems andfor those problems where pruning is used. For the enumeration problems we get nearlinear speedup using several hundred cores. For the satisfiability problem we show asubstantial improvement in the number of SAT instances that can be solved in a given
fixed time period. Finally we give some conclusions and areas for future research in
Section 8.
1 In 2008, John White made a list of 130 different applications and implementations, see link at [6].
2 Version used here available at https://www-alg.ist.hokudai.ac.jp/

2~skip/mts/

2. Survey of previous work
The reverse search method, initially developed for vertex enumeration, was extended
to a wide variety of enumeration problems [5]. From the outset it was realized that
it was eminently suitable for parallelization. In 1998, Marzetta announced his ZRAM
parallelization platform [14, 35] which can be used for reverse search, backtracking
and branch and bound codes. He successfully used it to parallelize several reverse
search and branch and bound codes, including lrs from which he derived the prs code.
Load balancing is performed using a variant of what is now known as job stealing.
Application codes, such as lrs, were embedded into ZRAM itself leading to problems
of maintenance as the underlying codes evolved. Although prs is no longer distributed
and was based on a now obsolete version of lrs, it clearly showed the potential for large
speedups of reverse search algorithms.
The reverse search framework in ZRAM was also used to implement a parallel codefor certain quadratic maximization problems [21]. In a separate project, Weibel [45]developed a parallel reverse search code to compute Minkowski sums. This C++ implementation runs on shared memory machines and he obtains linear speedups withup to 8 processors, the largest number reported.
ZRAM is a general-purpose framework that is able to handle a number of otherapplications, such as branch and bound and backtracking, for which there are by now
a large number of competing frameworks. This is a very large area and an extensive
survey of those methods relevant to the present study was given in [8]. We give a brief
overview here. Recent papers by Crainic et al. [17], McCreesh et al. [37] and Herrera etal. [25] describe over a dozen such systems. While branch and bound may seem similar
to reverse search enumeration, there are fundamental differences. In enumeration it isrequired to explore the entire tree whereas in branch and bound the goal is to explore
as little of the tree as possible until a desired node is found. The bounding step removes
subtrees from consideration and this step depends critically on what has already been
discovered. Hence the order of traversal is crucial and the number of nodes evaluatedvaries dramatically depending on this order. Sharing of information is critical to thesuccess of parallelization. These issues do not occur in reverse search enumeration, andso a much lighter wrapper is possible.
Relevant to the heaviness of the wrapper and amount of programming effort required, a comparison of three frameworks is given in [25]. The first, Bob++ [19],is a high level abstract framework, similar in nature to ZRAM, on top of which theapplication sits. This framework provides parallelization with relatively little programming effort on the application side and can run on a distributed network. The second,Threading Building Blocks (TBB) [42], is a lower level interface providing more control
but also considerably more programming effort. It runs on a shared memory machine.
The third framework is the Pthread model [15] in which parallelization is deep in theapplication layer and migration of threads is done by the operating system. It also
runs on a shared memory machine. All of these methods use job stealing for loadbalancing [13]. In [25] these three approaches are applied to a global optimization
algorithm. They are compared on a rather small setup of 16 processors, perhaps dueto the shared memory limitation of the last two approaches. The authors found that
Bob++ achieved a disappointing speedup of about 3 times, considerably slower thanthe other two approaches which achieved near linear speedup.
A more sophisticated framework for parallelizing application codes over large net-3

works of computers is MW that works with the distributed environment of HTCondor3 .
MW is a set of C++ abstract base classes that allow parallelization of existing applications based on the master-worker paradigm [23]. We employ the same paradigm in
mts although our load balancing methods are different. MW has been used successfully
to parallelize combinatorial optimization problems such as the Quadratic Assignment
Problem, see the MW home page for references. Although MW could be used to parallelize reverse search algorithms, we are not aware of any such applications.

3. The mts framework
The goal of mts is to parallelize existing tree search codes with minimal internal
modification of these codes. The tree search codes should satisfy certain conditions,specified below. The mts implementation starts a user-specified number of processes
on a cluster of computers. One process becomes the master, another becomes theconsumer, and the remaining are workers which essentially run the original tree searchcode on specified subtrees. Communication is limited; workers are not interrupted anddo not communicate between themselves.
The master sends the input data and parametrized subproblems to workers, informs
the other processes to exit when appropriate, and handles checkpointing. The consumer
receives and synchronizes output. Workers get subproblems from the master, run thelegacy code, send output to the consumer, and return unfinished subproblems to themaster.
Generating subproblems can be done in many ways. One way would be to report
nodes at some initial fixed depth. This works well for balanced trees but many trees
encountered in practice are highly unbalanced and the vast majority of subtrees contain
few nodes. Increasing the initial search depth does not solve this problem. Ideally wewould only break up the large subtrees and in the development of mplrs we triedvarious ways to estimate the size of a given subtree. Experimentally this did not work
well due to the high variance of the estimator and the wasted cost of doing many
estimates.
The idea that worked best, and is implemented in mts, was also the simplest: aheuristic to determine large subtrees called budgeting. This general approach is similar
to but simpler than the well-known work-stealing approach [13]. When assigning work
the master specifies that a worker should terminate after completing a certain amountof work, called a budget, and then return a list of unexplored subtrees. The precise
budget may depend on the application. For enumeration problems it could be thenumber of nodes visited by the worker. Some advantages of budgeting are:• small subtrees are explored without being broken up• large subtrees will be broken up repeatedly• each worker returns periodically for reassignment, can give information to bepassed on to other workers and receive such information• it is implemented on-the-fly and avoids the duplication of work done in estimation• it can be varied dynamically during execution to control the job list size
• when used statically and without pruning, the overall job list produced is deterministic and independent of the number of workers
This last item is useful for debugging purposes and also enables a theoretical analysis
3 Available at https://research.cs.wisc.edu/htcondor/mw/

4

of the job list size under certain random tree models, see [4]. In particular, methods
that limit work based on time (such as “begetting” in MW) do not have this property.
Implementing budgeting does not require interrupting workers or communication
between workers. The master uses dynamic budgets to control the job list: small budgets break up more subtrees and lengthen the joblist while large budgets have thereverse effect.
Additional features of mts include checkpointing and restarts, allowing the user tomove jobs or free computing resources without losing work. mts can produce various histograms to help tune performance. Histograms and their uses are described in
Section 7.
3.1. Sequential tree search code
To be suitable for parallelization with mts the underlying tree search code, which wewill call search, must satisfy a few properties. First, when given a positive budget, searchshould either finish the given job or return a list of unexplored nodes. Any unexplored
node should represent a smaller portion of the unfinished work, i.e. running search(with positive budgets) on the unexplored nodes and any resulting unexplored nodes
will eventually result in finishing the original job. The code should also interpret thebudget in some suitable way where larger budgets correspond to doing more workthan smaller budgets. This may require some modification of the legacy code. Our
applications usually interpret the budget as number of traversed nodes and depth, but
this is not required (see conflict budgeting in Section 5.1).
Any given worker must be able to work on any given unexplored node that mts
has seen. It is helpful for the unexplored nodes to represent non-overlapping jobs. mts
supports sharing data between workers, but it is helpful for shared data to be small.
Implementing a shared memory version of mts could help performance when large
amounts of data are shared. Shared data is not used in our enumeration applications.
It is used for satisfiability and similar applications to prune the search tree.
3.2. Master process
The master process begins with initialization, including obtaining an applicationprovided initial start vertex . It places this initial subproblem in a (new) job list L, andthen enters the main loop. In this main loop, the master assigns budgeted subproblems
to workers, collects unfinished subproblems to add to L, and collects/sends updated
shared data from/to the workers. Assigning shared data updates to the master is notessential: it simplifies checkpointing but can increase load on the master and interconnect. Each worker either finishes its subproblem or reaches its budget limitation(max depth and max nodes) and returns unfinished subproblems to the master for
insertion into L. This continues until no workers are running and the master has no
unfinished subproblems. Once the main loop ends, the master informs all processes tofinish. The main loop performs the following tasks:• subproblems and relevant shared data updates are sent to free workers whenavailable;• check if any workers are done, mark them as free and receive their unfinishedsubproblems;• check and receive shared data updates.

5

Pseudocode is given as Algorithm 3 in the Appendix. Communication is non-blocking
and work proceeds when required information is available.
Using reasonable parameters is critical to performance. This is done dynamically byobserving |L|. We use parameters lmin, lmax and scale which depend on the type oftree search problem being handled. The following default values are used in this paper.
Initially, to create a reasonable size list L, we set max depth = 2 and max nodes =5000. Therefore the initial worker will generate subtrees at depth 2 until 5000 nodes
have been visited and then terminates sending roots of unvisited subtrees back to
the master. Additional workers are given the same aggressive parameters until |L|
grows larger than lmin times the number of processors, at which point max depth isremoved. Once |L| is larger than lmax times the number of processors, we multiply
the budget by scale. With scale = 40 workers will not generate any new subproblems
unless their tree has at least 200,000 nodes. If |L| drops below these bounds we returnto the smaller budgets. The default is lmin = 1, lmax = 3. In Section 7 we show an
example of how |L| typically behaves with these settings.
3.3. Workers
The worker processes are simpler – they receive the problem at startup, and thenrepeat their main loop: receive a parametrized subproblem and possible shared data
updates from the master, work on the subproblem subject to the parameters, send theoutput to the consumer, and send updated shared data and unfinished subproblems
to the master if the budget is exhausted. Pseudocode is given as Algorithm 4 in the
Appendix.
3.4. Consumer process
The consumer process in mts is the simplest. The workers send output to the consumer
in exactly the format it should be output (i.e., this formatting is done in parallel).
The consumer simply outputs it. By synchronizing output to a single destination, theconsumer delivers a continuous output stream to the user in the same way as searchdoes. Pseudocode is given as Algorithm 5 in the Appendix.

4. Applying mts to reverse search
Reverse search is a technique for generating large relatively unstructured sets of discrete objects [5]. In its most basic form, reverse search can be viewed as the traversalof a spanning tree, called the reverse search tree T , of a graph G = (V, E) whose nodes
are the objects to be generated. Edges in the graph are specified by an adjacency oracle, and the subset of edges of the reverse search tree are determined by an auxiliary
function, which can be thought of as a local search function f for an optimization
problem defined on the set of objects to be generated. One vertex, v ∗ , is designatedas the target vertex. For every other vertex v ∈ V repeated application of f must
generate a path in G from v to v ∗ . The set of these paths defines the reverse searchtree T , which has root v ∗ .
A reverse search is initiated at v ∗ , and only edges of the reverse search tree aretraversed. When a node is visited, the corresponding object is output. Since there isno possibility of visiting a node by different paths, the visited nodes do not need to6

be stored. Backtracking can be performed in the standard way using a stack, but thisis not required as the local search function can be used for this purpose.
In the basic setting described here a few properties are required. Firstly, the underlying graph G must be connected and an upper bound on the maximum vertex degree,∆, must be known. The performance of the method depends on G having ∆ as low
as possible. An adjacency oracle Adj(v, j) must be capable of generating the adjacentvertices of any given vertex v in G. For each vertex v 6= v ∗ the local search function
f (v) returns the tuple (u, j) where v = Adj(u, j) which defines the parent u of v in
T . Pseudocode is given in Algorithm 1 and is invoked by setting start vertex = v ∗ . C
implementations for several simple enumeration problems are given at [6]. For convenience later, we do not output the start vertex in the pseudocode shown. Note thatthe vertices are output as a continuous stream. Also note that Algorithm 1 does not
require the parameter start vertex to be the root v ∗ of the entire search tree. If an
arbitrary node in the tree is given, the algorithm reports the subtree rooted at thisnode and terminates.
We need to implement budgeting in order to parallelize Algorithm 1 with mts.
We do this in two ways that may be combined. Firstly we introduce the parametermax depth which terminates the tree search at that depth returning any unvisited
subtrees. Secondly we introduce a parameter max nodes which terminates the tree
search after this many nodes have been visited and again returns the roots of allunvisited subtrees. This entails backtracking to the root and returning the unvisited
siblings of each node in the backtrack path. These modifications are straightforward
and given in Algorithm 2, which reduces to Algorithm 1 by deleting the items in red.
To output all nodes in the subtree of T rooted at v we set start vertex = v,
max nodes = +∞ and max depth = +∞. To break up T into subtrees we have
two options that can be combined. Firstly we can set the max depth parameter resulting in all nodes at that depth to be flagged as unexplored. Secondly we can set thebudget parameter max nodes. In this case, once this many nodes have been exploredthe current node and all unexplored siblings on the backtrack path to the root are
output and flagged as unexplored.
4.1. Example 1: Topological sorts
A C implementation (per.c) of the reverse search algorithm for generating permutations is given in the tutorial [6]. A small modification of this code generates all topological sorts of a partially ordered set that is given by a directed acyclic graph (DAG).
Such topological sorts are also called linear extensions or topological orderings. The
code modification is given as Exercise 5.1 and a solution to the exercise (topsorts.c) is
at [6]. Here we describe how to modify this code to allow parallelization via the mts
interface to produce the program mtopsorts. The details and code are available at [6].
It is convenient to describe the procedure as two phases. Phase 1 implements budgeting and organizes the internal data in a suitable way. This involves modifying animplementation of Algorithm 1 to an implementation of Algorithm 2 that can be independently tested. We need to prepare a global data structure bts data which contains
problem data obtained from the input. In Phase 2 we build a node structure for use
by the mts wrapper and add necessary routines to allow initialization and I/O in aparallel setting. In practice this involves using a header file from mts. The resulting
program btopsorts.c can be compiled as a sequential code or with mts as a parallelcode with no change in the source files.

7

Algorithm 1 Reverse Search
1: procedure rs(start vertex )Algorithm 2 Budgeted Reverse Search
1: procedurebrs(start vertex , max depth,
max nodes)
2:v ← start vertex
2:v ← start vertex
3:j ← 0 depth ← 03:
j ← 0 depth ← 0 count ← 0
4:repeat4:
repeat5:
unexplored ← false
5:
while j < ∆ do6:
while j < ∆ and7:
unexplored = false do6:j ←j+18:j ←j+1
7:
if f (Adj(v, j)) = v 9:
if f (Adj(v, j)) = v thenthen8:v ← Adj(v, j)
10:v ← Adj(v, j)
9:
j←0
11:
j←0
12:
count ← count + 1
10:
depth ← depth + 1 13:
depth ← depth + 1
14:
if count ≥ max nodes or
depth = max depth then15:
unexplored ← true16:
end if17:
output (v, unexplored )11:
output (v)18:
end if12:
end if19:
end while
13:
end while20:
if depth > 0 then. backtrack step14:
if depth > 0 then21:(v, j) ← f (v)15:(v, j) ← f (v)22:depth ← depth − 116:depth ← depth − 1
23:
end if17:
end ifuntil depth = 0 and j = ∆18:
until depth = 0 and j = ∆ 24:
25: end procedure
19: end procedure

In the second phase we add the ‘hooks’ that allow communication with mts. This
involves defining a Node structure which holds all necessary information about a nodein the search tree. The roots of unexplored subtrees are maintained by mts for parallel processing. Therefore whenever a search terminates due to the max nodes ormax depth restrictions, the Node structure of each unexplored tree node is returned
to mts. As we do not wish to customize mts for each application, we use a very genericnode structure. The user should pack and unpack the necessary data into this structure
as required. The Node structure is defined in the mts header.
The efficiency of mts depends on keeping the job list non-empty until the end of thecomputation, without letting it get too large. Depending on the application, there may
be a substantial restart cost for each unexplored subtree. Surely there is no need toreturn a leaf as an unexplored node, and the prune=0 option checks for this. Further,
if an unexplored node has only one child it may be advantageous to explore further,terminating either at a leaf or at a node with two or more children, which is returned
as unexplored. The prune=1 option handles this condition, meaning that no isolated
nodes or paths are returned as unexplored. Note that pruning is not a built-in mts
option; it is an example of options that applications may wish to include and was
implemented in mtopsorts.
8

4.2. Example 2: Spanning trees
In the tutorial [6] a C implementation (tree.c) is given for the reverse search algorithm
for all spanning trees of the complete graph. An extension of this to generate all
spanning trees of a given graph is stated as Exercise 6.3. Applying Phase 1 and 2 as
described above results in the code btree.c. Again this may be compiled as a sequential
code or with the mts wrapper to provide the parallel implementation mtree. All of thesecodes are given at the URL [6].
4.3. Example 3: Triangulations
The previous examples are from the tutorial on reverse search; a more substantial
application of mts is the parallel enumeration of triangulations implemented in mptopcom [29]. This was the first parallel code for the problem, and has already foundapplications [30, 43]. Here we give a brief summary, see [29] for details of mptopcom
and [18] for background on triangulations.
Enumerating triangulations in the plane is one of the early applications of reverse
search [5]. Imai et al. [28] later gave a reverse search algorithm for enumerating triangulations in general dimensions, including techniques for restricting to regular triangulations and enumerating up to symmetry. However, the standard tool used for thisis TOPCOM [41], which essentially performs a breadth-first search of the flip graph.
mptopcom is an implementation of the algorithm by Imai et al. [28] with some
improvements, parallelized using mts. It uses TOPCOM for triangulations and flips
and polymake [22] for basic data types. The single-threaded version is competitive
with other codes for this problem, while the parallel version allows one to enumerate
triangulations that are (in practice) beyond reach of the other codes; see [29] fordetailed experimental results.
4.4. Example 4: Galton Watson trees
The previous examples give reverse search trees that are rather well balanced. By
that we mean that the height of the tree is either logarithmic or polylogarithmic in
its size, i.e. the number of nodes in the tree. Balanced trees are especially suited toparallelization and this is indeed the case for mts as we will see in the experimental
results in Section 6. To see how well budgeting works for non-balanced trees Avis andDevroye [4] studied its behaviour on a family of random trees with depth roughly thesquare root of their size. They also studied how the job list size L depends on thebudget parameter b. We review the main result.
A Galton-Watson (or Galton-Watson-Bienaymé) tree is a rooted random ordered
tree that is a classical statistical model of a birth and death process. Each node
independently generates a random number of children drawn from a fixed offspring
distribution ξ. The distribution of ξ defines the distribution of T , a random GaltonWatson tree. They consider critical Galton-Watson trees which are those having E{ξ =1}, and P{ξ = 1} < 1. In addition, they assume that the variance of ξ is finite (andhence, nonzero).
Moon [39] and Meir and Moon [38] defined the simply generated trees as orderedlabelled trees of size n that are all equally likely given a certain pattern of labelingfor each node of a given degree. The most important examples include the Catalan
trees (equiprobable binary trees), the equiprobable k-ary trees, equiprobable unarybinary trees (ordered trees with up to two children), random Motzkin trees, ran9dom planted plane trees (equiprobable ordered trees of unlimited degrees) and Cayley
trees (equiprobable unordered rooted trees). It turns out that all these trees can be
represented as critical Galton-Watson trees conditional on their size, n, a fact firstpointed out by Kennedy [32] and further developed by others. For example, when ξ
is 0 or 2 with probability 1/4, and 1 with probability 1/2, we obtain the uniform
binary (Catalan) tree. Uniformly random full binary trees are obtained by settingP{ξ = 0} = P{ξ = 2} = 1/2. A uniformly random k-ary tree has its offspring distributed as a binomial (k, 1/k) random variable. A uniform planted plane tree is obtained for the geometric law P{ξ = i} = 1/2i+1 , i ≥ 0. When ξ is Poisson of parameter
1, one obtains (the shape of) a random rooted labeled (or Cayley) tree. For ξ uniformon {0, 1, 2, . . . , k}, Tn is like a uniform ordered tree with maximal degree of k. All suchtrees can be dealt with at once in the Galton-Watson framework.
In [4] an analysis is performed on the expected size of the job list as a functionof the budget parameter b. They prove that if Tn is a Galton-Watson tree of size ndetermined by ξ, where E{ξ} = 1 variance 0 < σ 2 < ∞, then
Ln
→
n

r

πσ 2
8b

(1)

in probability as n → ∞, where b is the budget and Ln is the job list size. For example,
for thepCatalan trees we have σ 2 = 3/2 and so the constant on the right hand side of(1) is 3π/16b. With a budget b = 5000 this indicates that about 1% of the nodes
are returned unexplored to the job list. Jobs returned to Ln are the main source ofoverhead in mts, so a value of about 1% is very satisfactory in practice.
Experimental results are given in [4] for various Galton-Watson trees to show thatthe estimate in (1) is quite accurate.

5. Applying mts to satisfiability
Boolean satisfiability (SAT) asks us to determine the existence of (or find) satisfying
assignments for propositional formulas, see [12] for more background. SAT solvers havemade tremendous progress over the years, and are now widely used as general NP
solvers. While most application problems seem to result in easy SAT instances [10],there has long been interest in parallel SAT solvers for hard instances. Despite themany challenges [24, 31] in parallel SAT, there are recent successes [26].
There are two major approaches to parallel SAT solvers. Either one somehow partitions the space of possible assignments and uses divide-and-conquer (e.g., [1] for a
recent example) or one uses the portfolio approach and runs many sequential solvers on
the original problem (e.g., plingeling [11]). In either case, a major issue is determining
which learnt clauses4 to share between workers [3]. While sharing these clauses helps
prune the search space, additional clauses slow the solver and enormous numbers ofclauses are learned.
Another question for divide-and-conquer solvers is the question of how to divide
the search space. Many approaches have been tried, often setting initial variables
and using a common feature of sequential solvers to “solve under assumptions”. Some
recent solvers (e.g., [1] and treengeling [11]) work on these subproblems subject to somebudget, and hard subproblems can be split again. Cube-and-conquer [27] is another
4 CDCL solvers learn clauses during the search, pruning the search space. See, e.g., Chapter 4 of [12].

10recent approach that uses look-ahead solvers to divide the search space for CDCL
solvers.
5.1. mtsat: parallelizing Minisat with mts
We used mts to implement a divide-and-conquer solver mtsat, using Minisat 2.2.0 as
sequential solver. Our goal was to demonstrate the use of shared data and show thatmts can be used in settings other than enumeration. mtsat is still experimental andmuch work remains to reach the level of state-of-the-art dedicated parallel SAT solvers,
but it allows for experimentation with, e.g., budgeting and restart strategies in parallel
SAT.
Minisat [20] supports solving under assumptions, i.e. solving subject to some partial
assignment. It also supports solving subject to a budget, given in propagations or
conflicts, returning unknown if the given subproblem could not be solved within thebudget.
The major modification required is to report unexplored partial assignments when
the budget is exhausted. At any point in the search, SAT solvers distinguish between
decision variables and propagated variables. Decision variables are those where thesolver chose an assignment, while propagated variables are those where the solver wasable to determine (because of a unit clause) that only one option need be explored.
It suffices to return unexplored nodes corresponding to the current partial assignment
and to those formed by taking the unexplored options for decision variables (including
the last one) along the backtrack path.
Regarding learnt clauses, we implemented a simple scheme sharing only learnt unit
clauses. The idea is that short clauses cut the search tree more than longer clauses; anearly version of plingeling also shared only units [11]. We avoided more sophisticatedapproaches to sharing clauses [1, 3], using conflicts to prune the job list L and similarideas for simplicity.
mtsat includes additional options. For example, while the parallel solvers most similar to our approach [1, 11] budget using conflicts – we added the option to budget
using decisions. Conflict budgets correspond to hitting a leaf in the search tree, while
decision budgets correspond to nodes in the search space (omitting propagated variables since those are forced). Conflict budgets are attractive, but decision budgets
correspond more closely to the budgets used in Section 4 and allow us to experimentwith different budgeting techniques.
Modern solvers generally perform random restarts, abandoning the current search
to start over (cf. Chapter 4 of [12]) and hopefully avoid getting stuck in hard partsof the search space. We split problems along the backtrack path and schedule theseabandoned portions of the search space for later exploration – possibly resulting inmuch duplicated work. We therefore added an option to disable restarts, in order toexperiment with their impact on performance in mtsat, and formula preprocessing, toexperiment with the idea that avoiding preprocessing can be beneficial to divide-andconquer parallel SAT solvers [24].
The total is 50 lines of changes to legacy Minisat (including support to parse inputs
from strings) of the original 4803 lines, plus a few hundred lines of generic code interfacing the Minisat API and mts that can be re-used. Essentially identical changes
suffice to parallelize Glucose (since it is based on Minisat) and others, and so we also
parallelize Glucose 3.0. One could easily support workers using a mix of solvers, ahybrid of the divide-and-conquer and portfolio approaches to parallel SAT.

11

6. Experimental results
The tests were performed at Kyoto University on mai32, a cluster of 5 nodes with a
total of 192 identical processor cores, consisting of:• mai32abcd: 4 nodes, each containing: 2x Opteron 6376 (16-core 2.3GHz), 32GB
memory, 500GB hard drive (128 cores in total);• mai32ef: 4x Opteron 6376 (16-core 2.3GHz), 64 cores, 256GB memory, 4TB hard
drive.
A complete description of the problems solved below is given in [7] and the input files
are available by following the link to tutorial2 at [6].
6.1. Topological sorts: mtopsorts
The tests were performed using the following codes:• VR: obtained from [16], generates topological sorts in lexicographic order via the
Varol-Rotem algorithm [44] (Algorithm V in Section 7.2.1.2 of [34]);• Genle: also obtained from [16], generates topological sorts in Gray code orderusing the algorithm of Pruesse and Rotem [40];• btopsorts: derived from the reverse search code topsorts.c [6] as described in
Section 4.1;
• mtopsorts: mts parallelization of btopsorts.
For the tests all codes were used in count-only mode due to the enormous output thatwould otherwise be generated. All codes were used with default parameters5 :max depth = 2 max nodes = 5000 scale = 40 lmin = 1 lmax = 3(2)

The following graphs were chosen, listed in order of increasing edge density: pm22 ,cat42 , K8,9 . The constructions for the first two partial orders are well known (see, e.g.,
Section 7.2.1.2 of [34]) and the third is a complete bipartite graph.
Table 1.: Topological sorts: mai32, times in secs
Graph
pm22
cat42
K8,9

m
nodes
22
42
17

n
edges
21
61
72

No. of perms
13,749,310,575
24,466,267,020
14,631,321,600

VR
179
654
159

Genle
14
171
5

btopsorts
12723
45674
8957

12
1172
4731
859

mtopsorts
24
48
96
595
360 206
2699 1293 724
445
249 137

192
125
408
85

Results are in Table 1. The reverse search code btopsorts is very slow, over 900 times
slower than Genle and over 70 times slower than VR on pm22 . However the parallel
mts code obtains excellent speedups and is faster than VR on all problems when 192
cores are used.
6.2. Spanning trees: mtree
The tests were performed using the following codes:
5 Performance for budgeted reverse search seems quite stable for a range of reasonable parameters. See
Section 7 below, or Section 6.4 of [8], for experimental results and [4] for analysis.

12• grayspan: Knuth’s implementation [33] of an algorithm that generates all spanning trees of a given graph, changing only one edge at a time, as described in
Malcolm Smith’s M.S. thesis, Generating spanning trees (University of Victoria,
1997);• grayspspan: Knuth’s improved implementation of grayspan: “This program combines the ideas of grayspan and spspan, resulting in a glorious routine that generates all spanning trees of a given graph, changing only one edge at a time, with‘guaranteed efficiency’—in the sense that the total running time is O(m + n + t)
when there are m edges, n vertices, and t spanning trees.” [33];• btree: derived from the reverse search code tree.c [6] as described in Section 4.2;
• mtree: mts parallelization of btree.
Both grayspan and grayspspan are described in detail in Knuth [34]. Again all codes
were used in count-only mode and with the default parameters (2). The problems
chosen were the following graphs which are listed in order of increasing edge density:
8-cage, P5 C5 , C5 C5 , K7,7 , K12 . The latter 4 graphs were motivated by Table 5 in [34]:P5 C5 appears therein and the other graphs are larger versions of examples in thattable.
Table 2.: Spanning tree generation: mai32, times in secs
Graph8-cageP 5 C5
C5 C5
K7,7
K12

m
nodes
30
25
25
14
12

n
edges
45
45
50
49
66

No. of trees
23,066,015,625
38,720,000,000
1,562,500,000,000
13,841,287,201
61,917,364,224

grayspan
3166
3962
131092699
2394

grayspspan
730
1212
41568
460
1978

btree
10008
8918
230077
2708
3179

12
1061
851
26790
259
310

24
459
455
13280
142
172

mtree
48
238
221
7459
68
84

96
137
137
4960
51
97

192
92
122
4244
61
148

The computational results are given in Table 2. This time the reverse search code isa bit more competitive: about 3 times slower than grayspan and about 14 times slower
than grayspspan on 8-cage for example. The parallel mts code runs about as fast asgrayspspan on all problems when 12 cores are used and is significantly faster after that.
Near linear speedups are obtained up to 48-cores but then tail off. For the two densegraphs K7,7 and K12 the performance of mts is actually worse with 192 cores thanwith 96.
6.3. Satisfiability
The tests were performed using the following codes:• Minisat: version 2.2.0, classic sequential solver [20];• Glucose: version 3.0, sequential solver [2] derived from Minisat;• mtsat: parallel solver using mts and Minisat 2.2.0;• mtsat-glucose: parallel solver using mts and Glucose 3.0;
• Glucose-Syrup: version 4.0, parallel (shared memory) solver;• lingeling, treengeling: version bbc, sequential and (shared memory) parallel
solvers [11].
Benchmarking parallel SAT solvers is challenging [24] and any particular instance
may give superlinear speedups or timeouts. We use a standard set of hard instancesfrom applications, and count the number of problems that each solver can solve withina given time. We re-use the setup of [1], i.e. the 100 instances in the parallel track13

of SAT Race 2015 [9] and a timeout of 20 minutes. Results are in Figure 1. Due todifferent computers used, our results are not directly comparable to those in [1]. As
noted by [10], solvers like mtsat can use substantial memory on very large instances,
limiting the number of processes that can execute in a given amount of memory. The
computers we used had sufficient memory for the instances used.
1200

Solver
Minisat
mtsat (16)mtsat (32)mtsat (64)mtsat (128)mtsat (192)lingeling
treengeling (32)time (s)

1000
800
600

Minisat
mtsat (16)mtsat (32)mtsat (64)mtsat (128)mtsat (192)

400
200
0
10

20

30

40

50

60

70

problems solved (out of 100)

SAT
18
17
22
23
29
35
17
38

UNSAT
1
1
2
4
7
10
10
21

Total
19
18
24
27
36
45
27
59

(b) Instances solved within 1200s(a) Instances solved vs time

Figure 1.: mtsat performance (decision budgeting, default parameters (2))
The results in Figure 1 show improvement from additional cores using default parameters and decision budgeting with no attempt at tuning. Performance with conflictbudgeting is shown in Figure 2, using an initial budget of 10000 conflicts (i.e. the corresponding value in [1]).
1200

time (s)1000

Solver
Minisat
mtsat (16)mtsat (32)mtsat (64)mtsat (128)mtsat (192)

800
600

Minisat
mtsat (16)mtsat (32)mtsat (64)mtsat (128)mtsat (192)

400
200
0
10

20

30

40

50

60

70

SAT
18
18
23
27
30
34

UNSAT
1
2
3
7
10
11

Total
19
20
26
34
40
45

(b) Instances solved within 1200s

problems solved (out of 100)(a) Instances solved vs time

Figure 2.: mtsat performance (conflict budgeting, max nodes = 10000, scale = 10)
All non-timeout outputs are correct, and the 32-core run with conflict budgeting
solves problem 62bits 10.dimacs.cnf (reported as unsolved in the SAT Race 2015
results) giving a correct satisfying assignment. It is likely that experimenting withparameter values can improve performance, and using a newer sequential solver on
the workers may be another source of improvement given the performance treengelingachieves starting from the higher baseline performance of lingeling.
Along these lines, we also report results applying mts to parallelize Glucose. Figures
3 and 4 show results using the default decision budgeting and also conflict budgeting.
Note that like in mtsat, only unit clauses are shared in mtsat-glucose. A more sophisticated approach to sharing learnt clauses, e.g. sharing glue clauses, would likely help
14

1200

1200

1000

1000

800

800

time (s)time (s)performance.

600
400
200

600
400
200

0

0
10

20

30

40

50

60

70

10

problems solved (out of 100)
Glucosemtsat-glucose (16)mtsat-glucose (32)mtsat-glucose (64)mtsat-glucose (128)mtsat-glucose (192)

20

30

40

50

60

70

problems solved (out of 100)
Glucosemtsat-glucose (16)mtsat-glucose (32)mtsat-glucose (64)mtsat-glucose (128)mtsat-glucose (192)(a) Decision budgeting withdefault parameters (2)(b) Conflict budgeting with
max nodes = 10000, scale = 10

Figure 3.: mtsat-glucose performance: Instances solved vs time

SolverGlucosemtsat-glucose (16)mtsat-glucose (32)mtsat-glucose (64)mtsat-glucose (128)mtsat-glucose (192)
Glucose-Syrup (32)
Glucose-Syrup (64)

SAT
6
26
26
31
32
35
32
31

(a) Decision budgeting withdefault parameters (2)

UNSAT
5
5
5
6
9
10
18
18

Total
11
31
31
37
41
45
50
49

SolverGlucosemtsat-glucose (16)mtsat-glucose (32)mtsat-glucose (64)mtsat-glucose (128)mtsat-glucose (192)

SAT
6
23
27
30
34
38

UNSAT
5
7
7
10
13
13

Total
11
30
34
40
47
51

(b) Conflict budgeting with
max nodes = 10000, scale = 10

Figure 4.: mtsat-glucose performance: Instances solved within 1200s
In all cases, we see that additional cores allow one to solve more problems given a
fixed amount of time. While it is likely that performance can be improved by tuning
and a better approach to sharing clauses, these results suffice for our purpose: to showthat one can easily parallelize a legacy code with mts.
As mentioned earlier, conflict budgeting is most common in this kind of parallel
solver. This is because generating a conflict clause guarantees at least some progress has
been made and instances can have very different and enormous numbers of variables.
Conflict budgeting usually slightly outperformed decision budgeting in the runs here,
however this was not universal. Given the minimal tuning for both budget types, ourresults do not show a clear difference regarding how to budget.

157. Evaluating and improving performance
Our main measures of performance for the enumeration problems are the elapsed time
taken and the efficiency defined as:
efficiency =single core running timenumber of cores ∗ multicore running time(3)

Multiplying efficiency by the number of cores gives the speedup. Speedups that scalelinearly with the number of cores give constant efficiency. External factors can affectperformance as the load on the machine increases. One example is dynamic overclocking, where the speed of working cores may be increased by 25%–30% when other cores
are idle. This limits the maximum efficiency achievable when all cores are used, since
the single core running times are measured on otherwise idle machines. In Figure 5 weplot the efficiencies obtained by mtopsorts and mtree for the runs shown in Tables 1
and 2 respectively.
Efficiency vs number of cores (mtree)
1

0.8

0.8
efficiency

efficiency

Efficiency vs number of cores (mtopsorts)
1

0.6
0.4
pm22
cat42
K8,9

0.2
0
16

0.6
8-cageP 5 C5
C5 C5
K7,7
K12

0.4
0.2
0

32

64

128

16

32

cores

64

128

cores

(a) Efficiency with mtopsorts(b) Efficiency with mtree

Figure 5.: Efficiency vs number of cores (data from Tables 1 and 2)
The amount of work contained in a subproblem can vary dramatically. mts can
produce histograms to help understand and tune performance. We discuss three here:
processor usage, job list size and distribution of subproblem sizes. Figure 6 shows thefirst two histograms for the mtopsorts run on K8,9 with default parameters (2).

Number of cores vs timeSize of job list L vs time

125

2200
’histk89-default’ using 1:3

120

2000

115

1800

110

1600

105

1400

100

1200

L

cores

’histk89-default’ using 1:2

95

1000

90

800

85

600

80

400

75

200
0

20

40

60
time (secs)

80

100

120

0

20

40

60
time (secs)

80

100

120

Figure 6.: Histograms for mtopsorts on K8,9 : busy workers (left) job list size (right)

16

We see the master struggling to keep workers busy despite having jobs available.
This suggests that we can improve performance with better parameters. Here, a larger-scale or -maxnodes value may help, since it will allow workers to do more work
(assuming a sufficiently large subproblem) before contacting the master.

Number of cores vs timeSize of job list L vs time

130

1400
’histk89-scale200maxnodes10000’ using 1:2’histk89-scale200maxnodes10000’ using 1:3
1200

110

1000

100

800
L

cores

120

90

600

80

400

70

200

60

0
0

20

40

60
time (secs)

80

100

120

0

20

40

60
time (secs)

80

100

120

Figure 7.: Histograms with -scale 200 -maxnodes 10000 on K8,9 : busy workers (l),joblist size (r)Figure 7 shows the result of using 200 for -scale and 10000 for -maxnodes. These
parameters produce less than half the number of total number of jobs compared tothe default parameters, and increase performance by about five percent on this input.
In addition to the performance histograms, mts can generate a frequency file containing a list of values returned by each worker on the completion of each job. For theenumeration applications this is normally the number of nodes visited by the worker
during the job. Such a list provides statistical information about the tree that is helpfulwhen tuning the parameters for better performance. For example, it may be helpful
to implement and use pruning if many jobs correspond to leaves. Likewise, increasing
the budget will have limited effect if only few jobs use the full budget.

Frequency distribution of subtree sizes

Frequency distribution of subtree sizes up to 100 nodes

70000

70000
’freq’ using (rounded($1)):(1)

60000

60000

50000

50000

40000

40000

Frequency

Frequency’freq’ using (rounded($1)):(1)

30000

30000

20000

20000

10000

10000

0

0
0

50000

100000150000Size of subtree

200000250000

0

20

40

60

80

100

Size of subtree

Figure 8.: Subproblem sizes for K8,9 : all (left) small subproblems only (right)
Figure 8 shows the distribution of subproblem sizes that was produced in a runof mtopsorts on K8,9 with default parameters (2). L is usually large so the scaled
budget constraint of 200000 is normally in use. The left figure shows this constraint
was invoked about 15000 times. The right figure shows that most subproblems have17

less than 40 nodes and so are not broken up. The three spikes in the middle of the left
figure are interesting and show there are large numbers of subtrees with these specificsizes. This is probably due to the high symmetry of the graph K8,9 .
8. Conclusions
We have presented a generic framework for parallelizing certain tree search codes
requiring only minimal changes to the legacy codes. Two features of our approach arethat the parallelizing wrapper does not need to be user modified and the modified
legacy code can be tested in standalone single processor mode. There is no separate
library to install and just a few routines need to be inserted in a user’s existing library.
Applying mts to four reverse search codes we obtained comparable results to that
previously obtained by the customized mplrs wrapper applied to the the lrs code [8].
We expect that many other reverse search applications and will obtain similar speedups
when parallelized with mts.
The application to SAT demonstrates the use of shared data, and the ease withwhich a widely-used existing legacy code can be parallelized using mts. While mtsat
remains work in progress, it shows some promise and further experimentation can likely
improve performance. Other ongoing work involves using mts to parallelize existing
integer programming solvers that use the branch-and-bound approach.

Funding
This work was partially supported by JSPS Kakenhi Grants 16H02785, 18K18027,
23700019 and 15H00847, Grant-in-Aid for Scientific Research on Innovative Areas,‘Exploring the Limits of Computation (ELC)’.

References[1] G. Audemard, J.M. Lagniez, N. Szczepanski, and S. Tabary, An Adaptive Parallel SAT
Solver, in CP, LNCS Vol. 9892. 2016, pp. 30–48.
[2] G. Audemard and L. Simon, Predicting Learnt Clauses Quality in Modern SAT Solvers,
in IJCAI. 2009, pp. 399–404.
[3] G. Audemard and L. Simon, Lazy Clause Exchange Policy for Parallel SAT Solvers, in
SAT, LNCS Vol. 8561. 2014, pp. 197–205.
[4] D. Avis and L. Devroye, An analysis of budgeted parallel search on conditional GaltonWatson trees, arXiv:1703.10731 (2017).
[5] D. Avis and K. Fukuda, Reverse search for enumeration, Discrete Applied Mathematics
65 (1993), pp. 21–46.
[6] D. Avis and C. Jordan, Reverse search: tutorials (2000,2016). http://cgm.cs.mcgill.
ca/~avis/doc/tutorial.
[7] D. Avis and C. Jordan, A parallel framework for reverse search using mts,
arXiv:1610.07735 (2016).
[8] D. Avis and C. Jordan, mplrs: A scalable parallel vertex/facet enumeration code, Math.
Program. Comput. 10 (2018), pp. 267–302.
[9] T. Balyo, A. Biere, M. Iser, and C. Sinz, SAT Race 2015, Artificial Intelligence 241 (2016),
pp. 45–65.
[10] T. Balyo, M.J. Heule, and M. Järvisalo, SAT Competition 2016: Recent Developments, in
AAAI. 2017.

18

[11] A. Biere, Lingeling and Friends Entering the SAT Challenge 2012, in Proc. SAT Challenge
2012, Department of Computer Science Series of Publications B, University of HelsinkiVol. B-2012-2. 2012, pp. 33–34.
[12] A. Biere, M.J. Heule, H. van Maaren, and T. Walsh (eds.), Handbook of Satisfiability, IOS
Press, 2009.
[13] R.D. Blumofe and C.E. Leiserson, Scheduling multithreaded computations by work stealing,
Journal of the ACM 46 (1999), pp. 720–748.
[14] A. Brüngger, A. Marzetta, K. Fukuda, and J. Nievergelt, The parallel search bench ZRAM
and its applications., Ann. Oper. Res. 90 (1999), pp. 45–63.
[15] L.G. Casado, J.A. Martı́nez, I. Garcı́a, and E.M.T. Hendrix, Branch-and-bound interval
global optimization on shared memory multiprocessors, Optimization Methods and Software 23 (2008), pp. 689–701.
[16] Combinatorial Object Server : Linear extensions. http://theory.cs.uvic.ca/inf/
pose/LinearExt.html.
[17] T.G. Crainic, B. Le Cun, and C. Roucairol, Parallel Branch-and-Bound Algorithms, inParallel Combinatorial Optimization, John Wiley & Sons, Inc. (2006), pp. 1–28.
[18] J.A. De Loera, J. Rambau, and F. Santos, Triangulations, Algorithms and Computationin Mathematics Vol. 25, Springer-Verlag, 2010.
[19] A. Djerrah, B. Le Cun, V.D. Cung, and C. Roucairol, Bob++: Framework for Solving
Optimization Problems with Branch-and-Bound methods, in 2006 15th IEEE International
Conference on High Performance Distributed Computing. 2006, pp. 369–370.
[20] N. Eén and N. Sörensson, An Extensible SAT-solver, in SAT, LNCS Vol. 2919. 2003, pp.
502–518.
[21] J. Ferrez, K. Fukuda, and T. Liebling, Solving the fixed rank convex quadratic maximization in binary variables by a parallel zonotope construction algorithm, European Journalof Operational Research 166 (2005), pp. 35–50.
[22] E. Gawrilow and M. Joswig, polymake: a framework for analyzing convex polytopes,in Polytopes—combinatorics and computation (Oberwolfach, 1997), DMV Sem. Vol. 29,
Birkhäuser, Basel, 2000, pp. 43–73.
[23] J.P. Goux, S. Kulkarni, M. Yoder, and J. Linderoth, Master–worker: An enabling framework for applications on the computational grid, Cluster Computing 4 (2001), pp. 63–70.
[24] Y. Hamadi and C.M. Wintersteiger, Seven challenges in parallel SAT solving, in AAAI.
2012, pp. 2120–2125.
[25] J.F.R. Herrera, J.M.G. Salmerón, E.M.T. Hendrix, R. Asenjo, and L.G. Casado, On parallel branch and bound frameworks for global optimization, Journal of Global Optimization(2017), pp. 1–14.
[26] M.J. Heule, O. Kullmann, and V.W. Marek, Solving and Verifying the boolean Pythagorean
Triples problem via Cube-and-Conquer, in SAT, LNCS Vol. 9710. 2016, pp. 228–245.
[27] M.J. Heule, O. Kullmann, S. Wieringa, and A. Biere, Cube and Conquer: Guiding CDCLSAT Solvers by Lookaheads, in HVC, LNCS Vol. 7261. 2012.
[28] H. Imai, T. Masada, F. Takeuchi, and K. Imai, Enumerating triangulations in generaldimensions, International Journal of Computational Geometry & Applications 12 (2002),
pp. 455–480.
[29] C. Jordan, M. Joswig, and L. Kastner, Parallel enumeration of triangulations, Electronic
Journal of Combinatorics 25 (2018), p. P3.6.
[30] M. Joswig and L. Kastner, New Counts for the Number of Triangulations of Cyclic Polytopes, in ICMS, LNCS Vol. 10931. 2018, pp. 264–271.
[31] G. Katsirelos, A. Sabharwal, H. Samulowitz, and L. Simon, Resolution and Parallelizability: Barriers to the Efficient Parallelization of SAT Solvers, in AAAI. 2013, pp. 481–488.
[32] D.P. Kennedy, The Galton-Watson process conditioned on the total progeny, Journal ofApplied Probability 12 (1975), pp. 800–806.
[33] D.E. Knuth, Programs to read. http://www-cs-faculty.stanford.edu/~uno/programs.html.
[34] D.E. Knuth, The Art of Computer Programming, Volume 4A, Addison-Wesley Profes-

19

sional, 2011.
[35] A. Marzetta, ZRAM: A library of parallel search algorithms and its use in enumerationand combinatorial optimization, Ph.D. diss., Swiss Federal Institute of Technology Zurich,
1998.
[36] T. Mattson, B. Sanders, and B. Massingill, Patterns for Parallel Programming, 1st ed.,Addison-Wesley Professional, 2004.
[37] C. McCreesh and P. Prosser, The shape of the search tree for the maximum clique problem and the implications for parallel branch and bound, ACM Transactions on Parallel
Computing 2 (2015), pp. 8:1–8:27.
[38] A. Meir and J.W. Moon, On the altitude of nodes in random trees, Canadian Journal of
Mathematics 30 (1978), pp. 997–1015.
[39] J. Moon, Counting Labelled Trees, Canadian mathematical monographs, 1970.
[40] G. Pruesse and F. Ruskey, Generating the linear extensions of certain posets by transpositions, SIAM Journal on Discrete Mathematics 4 (1991), pp. 413–422.
[41] J. Rambau, TOPCOM: Triangulations of Point Configurations and Oriented Matroids,in Mathematical Software—ICMS 2002. World Scientific, 2002, pp. 330–340. Available at
http://nbn-resolving.de/urn:nbn:de:0297-zib-6849.
[42] J. Reinders, Intel Threading Building Blocks, O’Reilly & Associates, Inc., 2007.
[43] B. Schröter, Multi-splits and tropical linear spaces from nested matroids, Discrete & Computational Geometry 61 (2019), pp. 661–685.
[44] Y.L. Varol and D. Rotem, An algorithm to generate all topological sorting arrangements,
The Computer Journal 24 (1981), pp. 83–84.
[45] C. Weibel, Implementation and Parallelization of a Reverse-Search Algorithm for
Minkowski Sums, in 2010 Proceedings of the Twelfth Workshop on Algorithm Engineeringand Experiments (ALENEX). 2010, pp. 34–42.

20

Appendix A. Pseudocode

Algorithm 3 Master process
1: procedure

master(input data, max depth, max nodes, lmin, lmax , scale,num workers)
2:
Send (input data) to each worker
3:
Create empty table sdata
4:
Create empty list L
5:
Get start vertex from application, add to L
6:size ← num workers + 2
7:while L is not empty or some worker is marked as working do
8:while L is not empty and some worker not marked as working do
9:
if |L| < size · lmin then10:
maxd ← max depth
11:
else
12:
maxd ← ∞13:
end if14:
if |L| > size · lmax then15:
node budget ← scale · max nodes
16:
else
17:
node budget ← max nodes18:
end if19:
Remove next element start from L
20:
Send (start, maxd , node budget) to first free worker i
21:Mark i as working
22:
Send any shared data in sdata newer than i has
23:
end while24:
for each marked worker i do
25:
Check for new message unfinished from i26:
if incoming message unfinished from i then27:
Join list unfinished to L
28:
Receive shared data update from i29:
Unmark i as working
30:
if non-empty update then31:
Update i’s shared data in sdata
32:
end if33:
end if34:
end for35:
end while36:
Call application with final set of shared data
37:
Send terminate to all processes
38: end procedure

21

Algorithm 4 Worker process
1: procedure worker
2:
Receive (input data) from master
3:
Create empty shared data4:
while true do
5:Wait for message from master6:
if message is terminate then
7:
Exit
8:
end if9:
Receive (start vertex , max depth, max nodes)
10:
Receive shared data updates, update local copy
11:
Call search (start vertex , max depth, max nodes, shared data)
12:
Send list of unfinished vertices to master13:
Send shared data update to master14:
Send output list to consumer
15:
end while
16: end procedure

Algorithm 5 Consumer process
1: procedure consumer2:
while true do
3:
Wait for incoming message
4:
if message is terminate then
5:
Exit
6:
end if7:
Output this message
8:
end while
9: end procedure22