# Classical Planning as QBF Without Grounding
(extended version)

Irfansha Shaik1 , Jaco van de Pol1

###### Abstract

Most classical planners use grounding as a preprocessing step, essentially
reducing planning to propositional logic. However, grounding involves
instantiating all action rules with concrete object combinations, and results
in large encodings for SAT/QBF-based planners. This severe cost in memory
becomes a main bottleneck when actions have many parameters, such as in the
Organic Synthesis problems from the IPC 2018 competition. We provide a compact
QBF encoding that is logarithmic in the number of objects and avoids grounding
completely, by using universal quantification for object combinations. We show
that we can solve some of the Organic Synthesis problems, which could not be
handled before by any SAT/QBF based planners due to grounding.

##  1 Introduction

Automated planning has many real-world applications, such as Space Exploration
and Robotics, cf. the book by Ghallab, Nau, and Traverso (2004). The two main
research directions in automated planning are heuristic-based state-space
search and propositional satisfiability (SAT) based solving. While heuristic-
based search often finds some plan quickly, it may not guarantee to search the
whole search space. SAT-based solvers, on the other hand, can also be used to
prove the non-existence of plans up to a bounded length. For some
applications, quickly falsifying the existence of a plan can be useful.
Classical planning is the most simple problem; its aim is to find a valid
sequence of actions from a single initial state to some goal state, where the
state is completely known and the effect of all actions is deterministic.
Kautz and Selman (1992) reduced the planning problem to the bounded
reachability problem and provided a corresponding SAT encoding for some plan
length $k$.

Classical planning domains are usually defined by logical rules that describe
the pre-conditions and effects of applying actions. Usually, a single action
is applied to multiple objects, corresponding to the arity of that action. The
pre-conditions and effects contain predicates, which also refer to multiple
objects. A concrete planning problem defines a universe of concrete objects,
and an initial and goal condition. Many planning tools, both SAT-based and
heuristic, first apply a grounding step: all action rules are instantiated for
all possible combinations of objects. However, for domains with actions that
involve many objects, the grounded specification is very large, and memory
becomes the main bottleneck. Despite several improvements, such as action
splitting (Kautz and Selman 1992), explanatory frame axioms (Haas 1987),
invariants (Rintanen 2008) and parallel plans (Rintanen, Heljanko, and Niemelä
2006), the memory still remains a bottleneck for domains with large action
arity.

QBF (Quantified Boolean Formula) encodings are known for being more compact
than SAT encodings, so they are considered as an alternative when SAT
encodings suffer from memory problems. Dershowitz, Hanna, and Katz (2005) and
Jussila and Biere (2007) proposed a QBF encoding with $\exists\forall\exists$
quantifier alternation for reachability in Bounded Model Checking (BMC). It
generates only a single copy of the transition function, instead of $k$ copies
in SAT, by using quantification over state variables. Rintanen (2001) proposed
a reachability QBF encoding that is logarithmic in the length of the plan, and
uses only one transition function. Cashmore, Fox, and Giunchiglia (2012)
proposed the Compact Tree Encoding (CTE), which improves upon the logarithmic
encoding by Rintanen (in the context of planning) by efficient traversal of
the search tree. Although these QBF encodings are more concise than the SAT
encodings, it has been reported that the SAT encodings can usually be solved
faster than the QBF encodings by the current solvers (Cashmore, Fox, and
Giunchiglia 2012). More importantly, the QBF encodings mentioned above still
require the problem to be grounded first, so the memory bottleneck for actions
that involve many objects has not been solved.

Matloob and Soutchanski (2016) proposed Organic Synthesis benchmarks and
showed that SAT based encodings could not solve any of the non-split
instances. They compared Madagascar (among other SAT based planners) and Fast
Downward (Helmert 2011) on these benchmarks. This is consistent with the
findings from the IPC-$2018$ planning competition, in which SAT based planners
performed poorly on instances from Organic Synthesis. These benchmarks contain
actions that manipulate up to 17 objects, so the grounding step exhausts the
memory. This not only applies to all SAT/QBF based planners based on
grounding: Even heuristic planners that employ grounding will exhaust the
memory for this domain. Thus, to solve these problems, there is a need for
encodings that avoid grounding altogether.

#### Our Contribution and Overview of the Paper.

In this paper, we propose a QBF encoding of quantifier structure
$\exists\forall\exists$ which completely avoids grounding, by using universal
variables to represent combinations of objects. The encoding is linear in the
number of action names, predicates, and path length, and logarithmic in the
number of objects. We provide an open-source implementation
111https://github.com/irfansha/Q-Planner of the encoding.

We will explain our encoding in two steps, to make it more accessible. In the
first step (Section 3), we present an intermediate representation in SAT. The
difference with the traditional binary encoding is that we provide a little
more structure: To encode a grounded action $A(o_{1},\ldots,o_{n})$, we use a
binary encoding of the action name $A$, followed by binary encodings of each
object $o_{i}$. The number of bits is logarithmic in the number of action
names and the number of possible objects. We organize the constraints as a big
conjunction over all atoms, i.e., predicates instantiated with concrete object
combinations. We do not claim that this SAT encoding is more efficient than
the traditional SAT encoding. Instead, this extra structure just makes the
transition to the QBF encoding more smooth.

The SAT encoding still contains constraints for each grounded predicate and
action. Hence the size of the encoding grows exponentially in the number of
parameters of predicates and actions. Our QBF encoding (Section 4) avoids this
as follows: Each constraint is encoded only once, for a “symbolic” object
combination $(o_{1},\ldots,o_{n})$. We use universal quantifiers over these
variables to have them instantiated for each concrete object combination,
rather than explicit grounding. Now the constraints are organized as a
conjunction over ungrouded predicate names only, and the number of variables
is logarithmic in the number of objects.

In our experiments (Section 5), we generated the QBF encoding for 20 domains
from previous IPC competitions, and solve them with the QBF solver CAQE. We
compare the size of our QBF encoding with the simple SAT encoding of the best
SAT-based planner, Madagascar. We also compare the running time of solving the
QBF and SAT encodings.

Focusing on the Organic Synthesis benchmarks, we compare our proposal not only
with Madagascar (using its best encoding), but also with two of the best
heuristic solvers. We show that some of the Organic Synthesis problems that
could not be handled before by any SAT/QBF based planners can now be solved
using our encoding. In these cases, we can also show that there are no plans
of shorter length.

##  2 Preliminaries

We introduce the main notions of the classical planning problems and QBF. We
also present a running example of the blocks-world domain (Listing 1) in PDDL,
the Planning Domain Definition Language (Fox and Long 2003).

### Classical Planning

Listing 1: blocks-world domain and problem.

⬇

(define (domain blocksworld)

(:predicates (clear ?$y_{1}$)(ontable ?$y_{1}$)

(on ?$y_{1}$ ?$y_{2}$))

(:action unstack

:parameters (?$x_{1}$ ?$x_{2}$)

:precondition (and (clear ?$x_{1}$)

(on ?$x_{1}$ ?$x_{2}$))

:effect (and (not (on ?$x_{1}$ ?$x_{2}$))

(ontable ?$x_{1}$)(clear ?$x_{2}$)))

(:action stack

:parameters (?$x_{1}$ ?$x_{2}$)

:precondition (and (clear ?$x_{1}$)

(clear ?$x_{2}$)(ontable ?$x_{1}$))

:effect (and (not(clear ?$x_{2}$))

(not(ontable ?$x_{1}$))(on ?$x_{1}$ ?$x_{2}$))))

(define (problem BW_rand_2)

(:domain blocksworld)

(:objects $b_{1}$ $b_{2}$)

(:init (ontable $b_{1}$) (on $b_{2}$ $b_{1}$) (clear $b_{2}$))

(:goal (and (on $b_{1}$ $b_{2}$))))

We start with introducing a planning signature.

###### Definition 1

A planning signature
$\Sigma=\langle\operatorname{P},\operatorname{A},\operatorname{O},\operatorname{arity}\rangle$
is a $4$-tuple where $\operatorname{P}$ is a set of predicate symbols,
$\operatorname{A}$ is a set of action names, $\operatorname{O}$ is a set of
objects, and the function
$\operatorname{arity}:(\operatorname{P}\cup\operatorname{A}\to\mathbb{N}_{0})$
indicates the expected number of arguments.

In the example of Listing 1,
$\operatorname{P}=\\{\operatorname{clear},\operatorname{ontable},\operatorname{on}\\}$,
$\operatorname{O}=\\{b_{1},b_{2}\\}$,
$\operatorname{A}=\\{\operatorname{unstack},\operatorname{stack}\\}$, and
$\operatorname{arity}(\operatorname{on})=2$. A schematic action corresponds to
an action name with parameters, e.g. $\operatorname{stack}(?x_{1},?x_{2})$. It
can be grounded to a set of concrete actions, by replacing the parameters by
concrete object combinations. Predicate symbols are also equipped with
parameters, that can be grounded by concrete objects. To facilitate our
encodings, we unify the parameter names of all actions to a fixed sequence of
$x$’s, and the formal predicate parameters to a sequence of $y$’s. Note that
these action and predicate parameter names will be used later for (universal)
object combination variables in the QBF encoding. Since we use a sequential
plan semantics, a single set of action and predicate parameter variables is
sufficient to represent any chosen action at each time step.

Each action is specified schematically by preconditions and effects, which we
will discussed next.

###### Definition 2

Given a signature, we define the set of atoms and grounded atoms (or fluents)
as:

$\displaystyle\operatorname{Atom}$
$\displaystyle=\\{\operatorname{p}(\overrightarrow{x})\mid\operatorname{p}\in\operatorname{P},|\overrightarrow{x}|=\operatorname{arity}(\operatorname{p})\\}$
$\displaystyle\operatorname{F}$
$\displaystyle=\\{\operatorname{p}(\overrightarrow{\operatorname{o}})\mid\operatorname{p}\in\operatorname{P},\operatorname{o}_{i}\in\operatorname{O},|\overrightarrow{\operatorname{o}}|=\operatorname{arity}(\operatorname{p})\\}$

###### Definition 3

Given a signature
$\Sigma=\langle\operatorname{P},\operatorname{A},\operatorname{O},\operatorname{arity}\rangle$.
The planning problem
$\operatorname{\Pi}=\langle\operatorname{I},\operatorname{G},\operatorname{pre}^{+},\operatorname{pre}^{-},\operatorname{eff}^{+},\operatorname{eff}^{-}\rangle$
is a $6$-tuple where

  * •

Initial state $\operatorname{I}\subseteq\operatorname{F}$ and

  * •

Goal condition $\operatorname{G}=(g^{+},g^{-})$, where
$g^{+},g^{-}\subseteq\operatorname{F}$.

  * •

for each action $\operatorname{a}\in\operatorname{A}$, we have:

    * –

positive preconditions
$\operatorname{pre}^{+}(\operatorname{a})\subseteq\operatorname{Atom}$

    * –

negative preconditions
$\operatorname{pre}^{-}(\operatorname{a})\subseteq\operatorname{Atom}$

    * –

positive effects
$\operatorname{eff}^{+}(\operatorname{a})\subseteq\operatorname{Atom}$

    * –

negative effects
$\operatorname{eff}^{-}(\operatorname{a})\subseteq\operatorname{Atom}$

In the example, (on ?$x_{1}$ ?$x_{2}$) is a positive precondition for action
unstack, while (ontable ?$x_{1}$) is a negative effect for action stack.

### SAT encoding

The planning problem is encoded as finding a path in a graph, whose nodes
consist of assignments to the fluents and whose edges are defined by the
conditions and effects of grounded actions. Finding a plan of length $k$
corresponds to finding a path of length $k$ from the intial node to a goal
node. Usually, a SAT encoding uses propositional variables encoding the $k$
actions and $k+1$ states in the path. A direct encoding would use $k$
variables for each grounded action, but since we use sequential plan semantics
(in which only one action occurs at the time), this can be encoded by a number
of variables that is logarithmic in the number of grounded actions (still
linear in $k$).

We will present the constraints in circuit format (with nested $\wedge$ and
$\vee$), which can be transformed to CNF clauses by a standard procedure. We
will write $\bigwedge$ and $\bigvee$ for conjunctions and disjunctions over
finite (indexed) sets.

### Quantified Boolean Formulas

Quantified Boolean Formulas (QBF) extend propositional formulas in SAT with
universal quantification over some variables. A QBF formula in _prenex normal
form_ is of the shape $\Pi\phi$ where $\phi$ is called the matrix, which is a
propositional formula, and $\Pi=Q_{1}X_{1}\dots Q_{n}X_{n}$ is the prefix with
alternating existential and universal quantifiers
$Q_{i}\in\\{\forall,\exists\\}$ and disjoint sets of variables $X_{i}$. The
$Q_{i}$ specify the quantification of each variable that occurs in $\phi$. We
consider only closed formulas, i.e., the quantification of all variables is
known. A QBF is evaluated to either True or False and its truth value can be
computed by recursively solving the formula over each outermost variable. A
formula $\exists x\phi$ is true if and only if $\phi[\top/x]$ or
$\phi[\bot/x]$ is true. A formula $\forall x\phi$ is true if and only if both
$\phi[\top/x]$ and $\phi[\bot/x]$ are true. The order within each quantified
block does not influence the truth value of the formula. When expanded, a QBF
corresponds to an and-or tree.

##  3 Intermediate SAT encoding

We now provide the intermediate SAT encoding of planning problems, as an
introduction to our QBF encoding. Throughout the section, we assume a fixed
planning problem as in Definition 3. Recall that we introduced a fixed
sequence of action parameters $x$.

For the encoding, we generate copies of variables for each time step
(represented by superscript) for a path of length $k$. We use action variables
$\operatorname{A}^{i}=\\{\operatorname{a}^{i}_{b}\mid 1\leq
b\leq\operatorname{\sigma}\\}$ for each $0\leq i\leq k-1$ and
$\operatorname{\sigma}=\lceil\log(|\operatorname{A}|)\rceil$; here
$\operatorname{a}_{b}^{i}$ represents the $b$-th bit of a logarithmic encoding
of the action name that occurs at time $i$ in the plan. The action parameter
variables are $\operatorname{PM}^{i}=\\{\operatorname{x}^{i}_{j,b}\mid 1\leq
j\leq\operatorname{\zeta},1\leq b\leq\operatorname{\gamma}\\}$ for each $0\leq
i\leq k-1$, where $\operatorname{\zeta}$ is the maximum action arity and
$\operatorname{\gamma}=\lceil\log(|\operatorname{O}|)\rceil$. Here
$\operatorname{x}_{j,b}^{i}$ represents the $b$-th bit of parameter
$\operatorname{x}_{j}$ of the action scheduled at time $i$ in the plan. We
will write $\overrightarrow{\operatorname{x}^{i}_{j}}$ (sequence of
$\operatorname{\gamma}$ variables) for the parameter $\operatorname{x}_{j}$ at
time $i$. The state variables are
$\operatorname{F}^{i}=\\{\operatorname{f}^{i}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}\mid\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{F}\\}$,
i.e., one variable for every fluent and for each $0\leq i\leq k$.

The corresponding SAT encoding is based on these variables, and constraints
for the initial condition $\operatorname{I}$, goal condition
$\operatorname{G}$, transition function $\operatorname{T_{g}}$, and a domain
restriction $\operatorname{RC}$.

$\displaystyle\exists\operatorname{A}^{0},\operatorname{PM}^{0},\dots,\operatorname{A}^{k-1},\operatorname{PM}^{k-1}\exists{\operatorname{F}^{0},\ldots,\operatorname{F}^{k}}$
$\displaystyle\operatorname{I}(\operatorname{F}^{0})\land\operatorname{G}(\operatorname{F}^{k})\land\bigwedge_{i=0}^{k-1}\operatorname{T_{g}^{\mathit{i}}}(\operatorname{F}^{i},\operatorname{F}^{i+1},\operatorname{A}^{i},\operatorname{PM}^{i})\land{}$
$\displaystyle\bigwedge_{i=0}^{k-1}\operatorname{RC}(\operatorname{A}^{i},\operatorname{PM}^{i})$

In the constraint for the initial state, each variable is positive if the
proposition is in the set $\operatorname{I}$ and negative if it is not. For
the goal state, the variable is positive if the proposition is in
$\operatorname{g}^{+}$ and negative if it is in $\operatorname{g}^{-}$. Note
that this provides a unique initial state, but there may be multiple states
that satisfy the goal condition. We group the constraints (throughout the
artice) based on the predicates for the sake of easy understanding of the
correctness proof (in Section 4).

###### Definition 4

Initial constraint $\operatorname{I}(\operatorname{F}^{0})=$

$\displaystyle\bigwedge_{\operatorname{p}\in\operatorname{P}}\bigwedge_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{F}}\\{\operatorname{f}^{0}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}|\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{I}\\}\land{}$
$\displaystyle\bigwedge_{\operatorname{p}\in\operatorname{P}}\bigwedge_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{F}}\\{\neg\operatorname{f}^{0}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}|\operatorname{p}(\overrightarrow{\operatorname{o}})\notin\operatorname{I}\\}$

###### Definition 5

Goal constraint $\operatorname{G}(\operatorname{F}^{k})=$

$\displaystyle\bigwedge_{\operatorname{p}\in\operatorname{P}}\bigwedge_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{F}}\\{\operatorname{f}^{k}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}|\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{g}^{+}\\}\land{}$
$\displaystyle\bigwedge_{\operatorname{p}\in\operatorname{P}}\bigwedge_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{F}}\\{\neg\operatorname{f}^{k}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}|\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{g}^{-}\\}$

To encode the transition function, we will generate five constraints for each
proposition variable. These constraints define the value of all fluents and
time stamps, just before or after some action occurs. The first four
constraints correspond to the positive preconditions, negative preconditions,
positive effects and negative effects, respectively. The last constraint
corresponds to the frame axiom, which indicates that untouched propositions
should not change.

###### Definition 6

The grounded transition function is:

$\operatorname{T_{g}^{\mathit{i}}}(\operatorname{F}^{i},\operatorname{F}^{i+1},\operatorname{A}^{i},\operatorname{PM}^{i})=\bigwedge_{\operatorname{p}\in\operatorname{P}}\bigwedge_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{F}}\operatorname{PC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}^{i}$

where the Proposition Constraint
$\operatorname{PC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}^{i}$
=

$\displaystyle(\operatorname{AC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{pre}^{+})\implies{\operatorname{f}}^{i}_{\operatorname{p}(\overrightarrow{\operatorname{o}})})\wedge{}$
$\displaystyle(\operatorname{AC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{pre}^{-})\implies\neg{\operatorname{f}}^{i}_{\operatorname{p}(\overrightarrow{\operatorname{o}})})\wedge{}$
$\displaystyle(\operatorname{AC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{eff}^{+})\implies{\operatorname{f}}^{i+1}_{\operatorname{p}(\overrightarrow{\operatorname{o}})})\wedge{}$
$\displaystyle(\operatorname{AC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{eff}^{-})\implies\neg{\operatorname{f}}^{i+1}_{\operatorname{p}(\overrightarrow{\operatorname{o}})})\wedge{}$
$\displaystyle(({\operatorname{f}}^{i}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}={\operatorname{f}}^{i+1}_{\operatorname{p}(\overrightarrow{\operatorname{o}})})\vee\operatorname{AC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{eff}^{+})\vee{}$
$\displaystyle\qquad\operatorname{AC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{eff}^{-}))$

Consider the positive precondition constraint: in plain words it expresses
that if some action occurs at time step $i$, and some fluent (grounded
predicate) is in the positive precondition of that action, then the
corresponding variable is true at time step $i$. Similarly, the proposition
variables corresponding to the positive (negative) effects should be set to
true (false) at time step $i+1$. The last constraint encodes the frame axiom:
it expresses that either the value of a proposition variable stays the same,
or some positive or negative effect occurs that defines this proposition.

We still need to encode when a positive/negative condition/effect $\Phi$ is
associated with the current action. We also need to define the set of grounded
instances of a predicate.

###### Definition 7

Given an action $\operatorname{a}\in\operatorname{A}$, a set of atoms
$\Phi\in\\{\operatorname{pre}^{+},\operatorname{pre}^{-},\operatorname{eff}^{+},\operatorname{eff}^{-}\\}$,
and sequence of objects
$\overrightarrow{\operatorname{o}}\in\operatorname{O}^{n}$ with
$n=\operatorname{arity}(\operatorname{a})$, its grounding
$\operatorname{GD}(\Phi,\operatorname{a},\overrightarrow{\operatorname{o}})\subseteq\operatorname{F}$
is a set of fluents, defined
$\operatorname{GD}(\Phi,\operatorname{a},\overrightarrow{\operatorname{o}}):=\\{\phi[\overrightarrow{x}/\overrightarrow{\operatorname{o}}]\mid\phi\in\Phi({\operatorname{a}})\\}$.

The grounding of an action with given object parameters returns the
corresponding grounded preconditions/effects. In the running example, the
positive precondition of action $\operatorname{stack}$ for object parameters
$(b_{1},b_{2})$ is grounded as
$\operatorname{GD}(\operatorname{pre}^{+},\operatorname{stack},(b_{1},b_{2}))=\\{\operatorname{clear}(b_{1}),\operatorname{clear}(b_{2}),\operatorname{ontable}(b_{1})\\}$.

Below, we use “$\operatorname{bin}$” to express the logarithmic encoding of
objects by $\gamma$ bits and of action names by $\sigma$ bits. We also use “=”
to denote a bit-wise conjunction of bi-implications.

###### Definition 8

Given the set of action names $\operatorname{A}$ and a set of atoms
$\Phi\in\\{\operatorname{pre}^{+},\operatorname{pre}^{-},\operatorname{eff}^{+},\operatorname{eff}^{-}\\}$
and a fluent $\operatorname{f}$, the grounded action constraint
$\operatorname{AC}_{\operatorname{f}}(\operatorname{A}^{i},\operatorname{PM}^{i},\Phi)$
=

$\displaystyle\bigvee_{\operatorname{a}\in\operatorname{A}}\bigvee_{\begin{array}[]{c}\scriptstyle
n=\operatorname{arity}(a)\\\\[-2.84526pt]
\scriptstyle\overrightarrow{\operatorname{o}}\in\operatorname{O}^{n}\end{array}}\big{\\{}(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{a}))\land\bigwedge^{n}_{j=1}(\overrightarrow{\operatorname{x}^{i}_{j}}=\operatorname{bin}(\operatorname{o}_{j}))\mid$
$\displaystyle\hskip
156.49014pt\operatorname{f}\in\operatorname{GD}(\Phi,\operatorname{a},\overrightarrow{\operatorname{o}})\big{\\}}$

In the grounded action constraint, for each grounded action
$\operatorname{a}(\overrightarrow{\operatorname{o}})$ that contains fluent
$\operatorname{f}$ in its grounded precondition/effect $\Phi$, we generate
equality constraints for action and parameter variables. For example, for
fluent $\operatorname{clear}(b_{1})$, $\Phi=\operatorname{pre}^{+}$ and
grounded action $\operatorname{stack}(b_{1},b_{2})$, we generate a disjunct
$\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\wedge\overrightarrow{x_{1}^{i}}=\operatorname{bin}(b_{1})\wedge\overrightarrow{x_{2}^{i}}=\operatorname{bin}(b_{2})$.

Finally, due to the use of logarithmic variables, invalid actions are possible
when the number of objects and actions are non-powers of $2$. To maintain
consistency we restrict the invalid action and parameter values by the
$\operatorname{RC}$-constraint. Here $<$ denotes the bit-blasted comparison
operator on binary numbers.

###### Definition 9

Restricted constraints
$\operatorname{RC}(\operatorname{A}^{i},\operatorname{PM}^{i})$ =

$\big{(}\overrightarrow{\operatorname{A}^{i}}<|\operatorname{A}|\big{)}\land\bigwedge_{1\leq
j\leq\operatorname{\zeta}}\big{(}\overrightarrow{\operatorname{x}^{i}_{j}}<|\operatorname{O}|\big{)}$

In practice, this constraint can still be refined if one has type information
on the objects, as in typed PDDL domains.

##  4 New Ungrounded QBF encoding

Similar to the intermediate SAT encoding, the QBF encoding of a plan of length
$k$ corresponds to finding a path of length $k$ from the initial state to some
goal state. From the SAT encoding, we can observe that the values of the
propositional variables only depend on the action variables, i.e., given a
sequence of actions and (complete) initial state, the intermediate states
until the goal state are completely determined. From the constraints on the
propositional variables, we can observe that their values are independent of
each other, so these constraints can be enforced independently (at each time
step and for each action). Fluents are generated by grounding the predicates,
i.e., by instantiating all object combinations. The propositional variables
are then generated for each fluent and each time step.

For the QBF encoding, the idea is to avoid grounding by representing all
object combinations as universal variables and generate constraints on the
predicate variables directly. Essentially the universal object combination
variables and existential predicate variables replace the existential
propositional variables in the intermediate SAT encoding.

The action variables ($\operatorname{A}$) and action parameter variables
($\operatorname{PM}$) are the same as for SAT encoding. We define object
combinations and predicates separately. The object combination variables are
$\operatorname{OC}=\\{\operatorname{y}_{j,b}\mid 1\leq
j\leq\operatorname{\eta},1\leq b\leq\operatorname{\gamma}\\}$ where
$\operatorname{\eta}$ is the maximum arity of predicates; and
$\operatorname{\gamma}$ is defined before. Here, $\operatorname{y}_{j,b}$
represents the $b$-th bit of the $j$th object variable and
$\operatorname{y}_{j}$ (sequence of $\operatorname{\gamma}$ variables)
represents the $j$th object variable. The predicate variables are
$\operatorname{P}^{i}=\\{\operatorname{q}^{i}_{\operatorname{p}}\mid\operatorname{p}\in\operatorname{P}\\}$
for each $0\leq i\leq k$. Note that $\operatorname{A}$ and $\operatorname{P}$
are ungrounded!

$\displaystyle\exists\overrightarrow{\operatorname{A}^{0}}\exists\overrightarrow{\operatorname{x}^{0}_{1}}\exists\overrightarrow{\operatorname{x}^{0}_{2}}\phantom{a}\exists\overrightarrow{\operatorname{A}^{1}}\exists\overrightarrow{\operatorname{x}^{1}_{1}}\exists\overrightarrow{\operatorname{x}^{1}_{2}}$
$\displaystyle\forall\overrightarrow{y_{1}}\forall\overrightarrow{y_{2}}$
$\displaystyle\exists\operatorname{q}_{\operatorname{clear}}^{0}\exists\operatorname{q}_{\operatorname{ontable}}^{0}\exists\operatorname{q}_{\operatorname{on}}^{0}$
$\displaystyle\exists\operatorname{q}_{\operatorname{clear}}^{1}\exists\operatorname{q}_{\operatorname{ontable}}^{1}\exists\operatorname{q}_{\operatorname{on}}^{1}$
$\displaystyle\exists\operatorname{q}_{\operatorname{clear}}^{2}\exists\operatorname{q}_{\operatorname{ontable}}^{2}\exists\operatorname{q}_{\operatorname{on}}^{2}$
Initial state:
$\displaystyle((\operatorname{bin}(b_{2})=\overrightarrow{y_{1}})\iff\operatorname{q}_{\operatorname{clear}}^{0})\land{}$
$\displaystyle((\operatorname{bin}(b_{1})=\overrightarrow{y_{1}})\iff\operatorname{q}_{\operatorname{ontable}}^{0})\land{}$
$\displaystyle((\operatorname{bin}(b_{2})=\overrightarrow{y_{1}})\land(\operatorname{bin}(b_{1})=\overrightarrow{y_{2}})\iff\operatorname{q}_{\operatorname{on}}^{0})\land{}$
Goal state:
$\displaystyle((\operatorname{bin}(b_{1})=\overrightarrow{y_{1}})\land(\operatorname{bin}(b_{2})=\overrightarrow{y_{2}}))\implies\operatorname{q}_{\operatorname{on}}^{2}\land{}$
For time steps i = 0,1 clear:
$\displaystyle\big{(}(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\land(\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}}\lor\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{1}}))\vee{}$
$\displaystyle\quad\text{
}(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{unstack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}})\big{)}\implies\operatorname{q}_{\operatorname{clear}}^{i}\land{}$
$\displaystyle(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{unstack})\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{1}})\implies\operatorname{q}_{\operatorname{clear}}^{i+1}\land$
$\displaystyle(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{1}})\implies\neg\operatorname{q}_{\operatorname{clear}}^{i+1}\land{}$
$\displaystyle((\operatorname{q}_{\operatorname{clear}}^{i}=\operatorname{q}_{\operatorname{clear}}^{i+1})\lor(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{unstack})\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{1}})$
$\displaystyle\quad{}\lor(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{1}}))\text{
}\land{}$ ontable:
$\displaystyle(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}})\implies\operatorname{q}_{\operatorname{ontable}}^{i}\land{}$
$\displaystyle(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{unstack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}})\implies\operatorname{q}_{\operatorname{ontable}}^{i+1}\land{}$
$\displaystyle(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}})\implies\neg\operatorname{q}_{\operatorname{ontable}}^{i+1}\land{}$
$\displaystyle((\operatorname{q}_{\operatorname{ontable}}^{i}=\operatorname{q}_{\operatorname{ontable}}^{i+1})\lor(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{unstack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}})$
$\displaystyle\quad{}\lor(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}}))\land{}$
on:
$\displaystyle(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{unstack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}}\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{2}})\implies\operatorname{q}_{\operatorname{on}}^{i}\land{}$
$\displaystyle(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}}\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{2}})\implies\operatorname{q}_{\operatorname{on}}^{i+1}\land{}$
$\displaystyle(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{unstack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}}\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{2}})\implies\neg\operatorname{q}_{\operatorname{on}}^{i+1}\land{}$
$\displaystyle((\operatorname{q}_{\operatorname{on}}^{i}=\operatorname{q}_{\operatorname{on}}^{i+1})\lor(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{stack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}}\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{2}})$
$\displaystyle\quad{}\lor(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{unstack})\land\overrightarrow{x_{1}^{i}}=\overrightarrow{y_{1}}\land\overrightarrow{x_{2}^{i}}=\overrightarrow{y_{2}}))$

Figure 1: Ungrounded Encoding for the blocks-world domain with a path length
of 2 actions

The corresponding Ungrounded Encoding is:

$\displaystyle\exists\operatorname{A}^{0},\operatorname{PM}^{0},\dots,\operatorname{A}^{k-1},\operatorname{PM}^{k-1}\forall\operatorname{OC}\exists\operatorname{P}^{0},\dots,\operatorname{P}^{k}$
$\displaystyle\operatorname{I_{u}}(\operatorname{P}^{0},\operatorname{OC})\land\operatorname{G_{u}}(\operatorname{P}^{k},\operatorname{OC})\land{}$
$\displaystyle\bigwedge_{i=0}^{k-1}\operatorname{T_{u}^{\mathit{i}}}(\operatorname{P}^{i},\operatorname{P}^{i+1},\operatorname{OC},\operatorname{A}^{i},\operatorname{PM}^{i})\land\bigwedge_{i=0}^{k-1}\operatorname{RC}(\operatorname{A}^{i},\operatorname{PM}^{i})$

In the sequel, we will define the auxiliary constraints for the initial and
goal states and the transition functions. The domain restriction
$\operatorname{RC}$ does not depend on the universal variables
$\operatorname{OC}$, so it remains unchanged from the SAT encoding (refer
Definition 9). We refer to the example in Figure 1 for an illustration of the
encoding in a concrete example. Finally, we comment on the equivalence of the
SAT and the QBF encoding. When the universal variables in the ungrounded QBF
encoding expanded, the resulted conjunction of constraints have correponding
equivalent constraints in the intermediate SAT encoding.

The initial and goal constraints must be consistent with object combinations,
so for each predicate, we specify in which forall branches, i.e., for which
objects instantiations it is positive or negative.

###### Definition 10

The Ungrounded Initial constraint
$\operatorname{I_{u}}(\operatorname{P}^{0},\operatorname{OC})$:

$\bigwedge_{\operatorname{p}\in\operatorname{P}}\big{(}\bigvee_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{I}}\bigwedge^{|\overrightarrow{\operatorname{o}}|}_{j=1}(\operatorname{bin}(\operatorname{o}_{j})=\overrightarrow{\operatorname{y}_{j}})\big{)}\iff\operatorname{q}^{0}_{\operatorname{p}}$

###### Definition 11

The Ungrounded goal constraint
$\operatorname{G}_{u}(\operatorname{P}^{k},\operatorname{OC})=\operatorname{G}^{+}\land\operatorname{G}^{-}$
where

$\displaystyle\operatorname{G}^{+}=\bigwedge_{\operatorname{p}\in\operatorname{P}}\big{(}\bigvee_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{g}^{+}}\bigwedge^{|\overrightarrow{\operatorname{o}}|}_{j=1}(\operatorname{bin}(\operatorname{o}_{j})=\overrightarrow{\operatorname{y}_{j}})\big{)}\implies\operatorname{q}_{\operatorname{p}}^{k},$
$\displaystyle\operatorname{G}^{-}=\bigwedge_{\operatorname{p}\in\operatorname{P}}\big{(}\bigvee_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{g}^{-}}\bigwedge^{|\overrightarrow{\operatorname{o}}|}_{j=1}(\operatorname{bin}(\operatorname{o}_{j})=\overrightarrow{\operatorname{y}_{j}})\big{)}\implies\neg\operatorname{q}_{\operatorname{p}}^{k}$

###### Definition 12

The ungrounded transition function

$\operatorname{T_{u}^{\mathit{i}}}(\operatorname{P}^{i},\operatorname{P}^{i+1},\operatorname{OC},\operatorname{A}^{i},\operatorname{PM}^{i})={\bigwedge_{\operatorname{p}\in\operatorname{P}}\operatorname{UPC}_{\operatorname{p}}^{i}}$

where the ungrounded predicate constraint
$\operatorname{UPC}^{i}_{\operatorname{p}}$ =

$\displaystyle(\operatorname{AC}_{\operatorname{p}}^{u}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{OC},\operatorname{pre}^{+})\implies\operatorname{q}^{i}_{\operatorname{p}})\wedge{}$
$\displaystyle(\operatorname{AC}_{\operatorname{p}}^{u}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{OC},\operatorname{pre}^{-})\implies\neg\operatorname{q}^{i}_{\operatorname{p}})\wedge{}$
$\displaystyle(\operatorname{AC}_{\operatorname{p}}^{u}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{OC},\operatorname{eff}^{+})\implies\operatorname{q}^{i+1}_{\operatorname{p}})\wedge{}$
$\displaystyle(\operatorname{AC}_{\operatorname{p}}^{u}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{OC},\operatorname{eff}^{-})\implies\neg\operatorname{q}^{i+1}_{\operatorname{p}})\wedge{}$
$\displaystyle((\operatorname{q}^{i}_{\operatorname{p}}=\operatorname{q}^{i+1}_{\operatorname{p}})\vee\operatorname{AC}_{\operatorname{p}}^{u}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{OC},\operatorname{eff}^{+})\vee{}$
$\displaystyle\qquad\operatorname{AC}_{\operatorname{p}}^{u}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{OC},\operatorname{eff}^{-}))$

For each predicate, if any of the action constraints is true in the
corresponding preconditions or effects, then the corresponding variable is
constrained to the appropriate value. We will expand on the action constraints
in the following definition. The constraints are similar to that of SAT
encoding, for example the positive precondition constraint represents if the
action with the predicate as positive precondition is true then the
corresponding predicate variable is set to true in time step $i$. The last
constraint is called the frame axiom; it says that either the value of
predicate stays the same or some positive or negative effect constraint is
true.

###### Definition 13

Given the set of actions $\operatorname{A}$ and
$\Phi\in\\{\operatorname{pre}^{+},\operatorname{pre}^{-},\operatorname{eff}^{+},\operatorname{eff}^{-}\\}$,
the ungrounded action constraint

$\displaystyle\operatorname{AC}_{\operatorname{p}}^{u}(\operatorname{A}^{i},\operatorname{PM}^{i},\operatorname{OC},\Phi)=\bigvee_{\operatorname{a}\in\operatorname{A}}(\overrightarrow{\operatorname{A}^{i}}=\operatorname{bin}(\operatorname{a}))\land{}$
$\displaystyle\qquad\bigvee\big{\\{}\bigwedge^{n}_{j=1}(\overrightarrow{\operatorname{x}^{i}_{l_{j}}}=\overrightarrow{\operatorname{y}_{j}})\mid\operatorname{p}(\operatorname{x}_{l_{1}},\dots,\operatorname{x}_{l_{n}})\in\Phi(\operatorname{a})\big{\\}}$

Similar to the initial and goal constraints, the value of the predicate
variables must be constrained in each forall branch. As we discuss before,
each forall branch corresponds to one instantiation of object combinations.
The ungrounded action constraint specifies which branches are evaluated to
true. In plain words, for every forall branch where the predicate parameters
variables are equal to the universal variables the ungrounded action
constraint is evaluated to true. Note that the predicate parameters from the
preconditions and effects are simply a subset of the action parameter
variables.

Regarding the frame axioms, we use the following performance optimisations in
our implementation: We do not need to propagate static predicates, i.e.,
predicates that do not appear in any of the action effects. Instead, for
static predicates we introduce only one copy, used across all time steps. In
particular, the type predicates in typed planning domains are handled as
static predicates. Equality-predicates are treated specially, since they
impose constraints between action parameters only, independent of forall
variables. We simply generate (in)equality constraints between action
parameters directly, similar to the RC-constraint.

### Correctness

We demonstrate correctness, by showing how the SAT encoding can be stepwise
transformed into the equivalent QBF encoding. Let
$\operatorname{\delta}=2^{\operatorname{\gamma}\times\operatorname{\eta}}$ be
the number of object combinations, and $n=|\operatorname{P}|$. Then the
constraints on the propositions in time step $i$ and $i+1$ in the SAT encoding
are:

$\displaystyle\exists\operatorname{f}^{i}_{\operatorname{p}_{1}(\overrightarrow{\operatorname{o}_{1}})}\dots\exists\operatorname{f}^{i}_{\operatorname{p}_{1}(\overrightarrow{\operatorname{o}_{\operatorname{\delta}}})}$
$\displaystyle\dots$
$\displaystyle\exists\operatorname{f}^{i}_{\operatorname{p}_{n}(\overrightarrow{\operatorname{o}_{1}})}\dots\exists\operatorname{f}^{i}_{\operatorname{p}_{n}(\overrightarrow{\operatorname{o}_{\operatorname{\delta}}})}$
$\displaystyle\qquad\bigwedge_{\operatorname{p}\in\operatorname{P}}\bigwedge_{\operatorname{p}(\overrightarrow{\operatorname{o}})\in\operatorname{F}}\operatorname{PC}_{\operatorname{p}(\overrightarrow{\operatorname{o}})}^{i}$

Here the existential blocks of propositional variables are grouped based on
the predicate symbols. Since each of the propositions appears in only one
constraint, we can push the existential variables inside the conjuction. Thus
the constraints are equivalent to the following groups of constraints in non-
prenex form:

$\displaystyle\exists\operatorname{f}^{i}_{\operatorname{p}_{1}(\overrightarrow{\operatorname{o}_{1}})}\dots\exists\operatorname{f}^{i}_{\operatorname{p}_{1}(\overrightarrow{\operatorname{o}_{\operatorname{\delta}}})}\bigwedge_{\operatorname{p}_{1}(\overrightarrow{\operatorname{o}})\in\operatorname{F}}\operatorname{PC}_{\operatorname{p}_{1}(\overrightarrow{\operatorname{o}})}^{i}$
$\displaystyle{}\land\dots\land{}$
$\displaystyle\exists\operatorname{f}^{i}_{\operatorname{p}_{n}(\overrightarrow{\operatorname{o}_{1}})}\dots\exists\operatorname{f}^{i}_{\operatorname{p}_{n}(\overrightarrow{\operatorname{o}_{\operatorname{\delta}}})}\bigwedge_{\operatorname{p}_{n}(\overrightarrow{\operatorname{o}})\in\operatorname{F}}\operatorname{PC}_{\operatorname{p}_{n}(\overrightarrow{\operatorname{o}})}^{i}$

Since all the constraints have a uniform shape, we can abbreviate the
conjunction by a for-all quantification in QBF. So the previous formula is
equivalent to the grouping with object combinations variables in the QBF
encoding:

$\displaystyle\forall\operatorname{OC}\text{
}\exists\operatorname{q}^{i}_{\operatorname{p}_{1}}\operatorname{UPC}_{\operatorname{p}_{1}}^{i}\land\dots\land\exists\operatorname{q}^{i}_{\operatorname{p}_{n}}\operatorname{UPC}_{\operatorname{p}_{n}}^{i}$

Remember that the action and parameter variables are the same for both SAT and
QBF encoding. This proves the equivalence between the SAT and the QBF
encodings.

| Q-planner |  | Madagascar |  | FDS |  | PL
---|---|---|---|---|---|---|---
Domains (Total) | I | UI | pm |  | I | UI | pm |  | I | UI | pm |  | I | UI | pm
OS-Sat18 ($20$) | $12$ | $1$ | $4.9$ |  | - | - | - |  | $3$ | - | $2.2$ |  | $\mathbf{15}$ | $\mathbf{4}$ | $1.1$
OS-Opt18 ($20$) | $\mathbf{20}$ | - | $2.6$ |  | - | - | - |  | $9$ | - | $15.7$ |  | $\mathbf{20}$ | - | $8.4$
Alkene ($18$) | $\mathbf{18}$ | - | $0.06$ |  | $1$ | - | $115.9$ |  | $\mathbf{18}$ | - | $15.7$ |  | $\mathbf{18}$ | - | $0.02$
MitExams ($20$) | $8$ | $1$ | $4.8$ |  | - | - | - |  | $1$ | - | $1.8$ |  | $\mathbf{12}$ | $\mathbf{5}$ | $8.4$
Table $1$: Running 4 tools with $300$ GB memory and $3$ hour time limit on $4$
Organic-Synthesis domains. We report “I”, the number of solved instances,
“UI”, the number of uniquely solved instances and “pm”, the peak memory for
the solved instances in GB.

##  5 Implementation and Experiments

We implemented our encoding of PDDL problems to QBF problems in QCIR format as
a Python program, which is available
online.222https://github.com/irfansha/Q-Planner The tool handles domains with
types and equality predicates by treating them as static predicates; it also
handles negative preconditions and constants, but it cannot yet handle domains
with conditional effects. To solve the encoded problems for a given length
$k$, we transform them to QDIMACS format, and use the QBF solver CAQE (Rabe
and Tentrup 2015) with the internal preprocessor Bloqqer (Biere, Lonsing, and
Seidl 2011). Some initial experiments with other preprocessors and solvers
indicated that CAQE+Bloqqer is a very good combination; we leave a systematic
comparison as future work. Finally, our tool extracts a concrete plan from
CAQE’s output, and validates that the plan is indeed correct. In the sequel,
we refer to the combination of our encoding, CAQE and Bloqqer as “Q-Planner”.

We performed two experiments: in the first experiment, we run Q-Planner on
planning problems from 4 Organic Synthesis domains: $2$ from IPC-18 (non-split
Satisfying and Optimizing track) and the 2 original benchmarks (Alkene and
Mitexams) (Masoumi, Antoniazzi, and Soutchanski
2015).333https://www.cs.ryerson.ca/mes/publications/ The domains submitted to
IPC-18 are simplified domains of the original benchmarks, which received the
outstanding domain submission award. We compare Q-Planner with 3 state-of-the-
art planners, specified below.

In the second experiment, we encoded all classical planning problems from
previous IPC planning competions that our translation can handle, resulting in
20 domains, including 2 for Organic Synthesis. We are mainly interested in the
number of instances that can be solved in each domain (within a given time and
memory limit). In this experiment, we compared Q-Planner with Madagascar,
using a simple SAT encoding (no invariants or parallel plans) to compare the
effect of our ungrounded encoding on the encoding size, memory usage and
solving time.

### Experimental Setup

For the first experiment, we compare Q-planner with 3 other planners: (1)
Madagascar (Rintanen 2014) with relaxed existential step encoding (Rintanen,
Heljanko, and Niemelä 2006), a SAT based planner which first grounds the
planning problem; (2) Fast Downward Stone Soup 2018 (Helmert and Röger 2011),
a non-SAT based planner which was the winner of IPC-2018 competitions in the
satisfying track; and (3) Powerlifted (PL) (Corrêa et al. 2020), a non-SAT
based planner which avoids grounding and is the state-of-the-art for the
Organic synthesis domains. We use recommended configurations for all three
planners for fair comparisons. We allow $300$GB of main memory and $3$ hours
of time limit for solving each instance of Organic Synthesis.

For the second experiment, we want to compare the ungrounded QBF encoding
(using Q-Planner) with the grounded SAT encoding (using Madagascar). To
eliminate other factors, we use Madagascar in its simplest configuration
without invariants and with sequential plan semantics (here called M-simple),
i.e., a standard sequential SAT encoding with direct encoding of objects and
actions. Since the CAQE solver calls SAT-solver Crypto-minisat (Soos, Nohl,
and Castelluccia 2009), we also use Crypto-minisat to solve the SAT encodings
in Madagascar.

For each instance, we generate encodings of increasing plan length in steps of
$5$ (steps of $1$ for Organic Synthesis domains) until a solution is found. We
abort the run when either a time limit of $5000$ seconds is reached or the
peak memory exceeds $8$GB. We iterate over all instances within a given
domain, but we stop once there are $5$ timed-out instances since we assume
that their difficulty increases (mostly due to an increase in the number of
objects). Since Bloqqer is called internally by CAQE, the solving time
includes the preprocessing time.

We ran our experiments on a Grendel-s444http://www.cscaa.dk/grendel-s/ Huawei
FusionServer Pro V1288H V5 server nodes for all the computations, each with 48
cores of 3.0 GHz (Intel Xeon Gold 6248R) and 384 GB main memory (but only one
core is used per problem).

### Results

| Domains | Q-planner | M-simple
---|---|---|---
|  | #solved | size | #solved | size
Typed IPC domains | Blocks | $28$ | 0.14 | $\mathbf{30}$ | 4.8
DriverLog | $\mathbf{11}$ | 0.27 | $\mathbf{11}$ | 5.7
Elevator | $34$ | 0.20 | $\mathbf{43}$ | 2.1
Hiking | $\mathbf{9}$ | 0.49 | $6$ | 75.8
OS-Opt18 | $\mathbf{20}$ | 2.6 | $0$ | -
OS-Sat18 | $\mathbf{11}$ | 3.2 | $0$ | -
Satellite | $\mathbf{6}$ | 0.23 | $\mathbf{6}$ | 1.7
Tidybot | $1$ | 1.7 | $\mathbf{13}$ | 519.9
Termes | $2$ | 0.68 | $\mathbf{3}$ | 14.3
Thoughtful | $0$ | 1.7 | $\mathbf{5}$ | 857.5
Visitall | $7$ | 0.41 | $\mathbf{13}$ | 2.5
Untyped IPC domains | Blocks-3op | $17$ | 0.16 | $\mathbf{19}$ | 63.2
Movie | $\mathbf{30}$ | 0.15 | $\mathbf{30}$ | 0.28
Depot | $4$ | 0.32 | $\mathbf{6}$ | 70.9
Gripper | $3$ | 0.19 | $\mathbf{5}$ | 0.80
Logistics | $\mathbf{12}$ | 0.34 | $\mathbf{12}$ | 4.0
Mprime | $17$ | 0.36 | $\mathbf{34}$ | 1954
Mystery | $3$ | 0.36 | $\mathbf{13}$ | 399.1
Grid | $\mathbf{2}$ | 0.52 | $\mathbf{2}$ | 47.9
Freecell | $2$ | 1.1 | $\mathbf{6}$ | 631.1
| Total sum | 219 | 15.12 | 257 | 4656
Table $2$: Instances solved within $5000$s and $8$GB internal memory. We also
show the size (in MB) of the encoding for the maximum instance after
preprocessing (if possible).

For the first experiment (Table $1$), Q-Planner solves $58$ instances in
total, while never using more than $4.9$GB memory for all the solved
instances; whereas Madagascar only solves $1$ instance using $116$GB memory.
These results are consistent with the IPC-$2018$ competitions, where $2$
variants of Madagascar could not solve any of the (non-split) organic
synthesis benchmarks in the satisfying track based on SAT solving. This is due
to the presence of actions with many parameters ($>17$), thus even with action
splitting and other optimisations the grounded encodings are too big. It is
clear that Q-Planner outperforms Madagascar significantly.

Concerning the non-SAT based planners: FDS, which has a special strategy for
partial grounding, solves $31$ instances in total, but on the other instances
it still exhausts all the memory during the grounding (translation) phase.
This emphasizes the problem with grounding even in non-SAT based planners. The
Powerlifted planner solves $65$ instances, in total solving $7$ more instances
than Q-planner. Interestingly, Q-Planner solves one instance uniquely in the
hardest set of benchmarks, i.e., MitExams. The good performance of Powerlifted
is expected, since it also avoids grounding on actions while using optimized
database queries on grounded states. We expect this is due to the large number
of grounded propositions in the initial state which is harder for Powerlifted.

We found some interesting observations regarding the Powerlifted planner: If
it finds a plan successfully, then it never takes more than a couple of
hundred MB and finds a plan quickly (except for one instance in both MitExams
and OS-Opt18, which takes $8.4$GB). On the failed instances, however,
Powerlifted either exhausts all the memory or runs out of time. Our Q-Planner,
on the other hand, might exceed the time-limit, but never used more than
$20$GB for refuting the existence of a plan of shorter lengths, even when it
could not solve the instance completely. For the unsolved instances in domains
MitExams and OS-Sat18, the minimum and maximum plan refutation length is $3$
and $7$, respectively, with an average length of $5$. This is the strength of
SAT/QBF based planners, for problems where quickly refuting the existence of a
plan of bounded length is useful.

Concerning the second experiment, the Ungrounded QBF Encoding never exceeds
$2$MB (or $3$MB in case of Organic Synthesis), so it is orders of magnitude
more compact than the SAT encoding (which sometimes exceeds $1950$MB). When
comparing the time for solving, the situation is different: Madagascar
performs better than Q-Planner on most other benchmarks (except Hiking), with
better peak memory and running times. This is expected since most benchmarks
in the IPC domains are easy to ground. For domains with a large number of
action parameters (Hiking, Organic Synthesis), our QBF encoding outperforms
the SAT encoding.

The peak memory (see Figure 3) consumed by solving the Ungrounded Encodings is
usually higher than the SAT encodings. This reflects the fact that QBF is
PSPACE complete, where SAT is merely NP-complete. In Figure 3, only instances
which are solved by both encodings are compared. However, there are some
instances where UE takes less memory than the SAT encoding, and the UE
encoding solves the problem whereas the SAT encoding could not (Hiking and
Organic Synthesis benchmarks). The higher peak memory usage by the CAQE solver
can be understood by considering its solution approach. CAQE solver generates
abstract propositional clauses and calls SAT solver (Crypto-minisat) as a
subroutine while taking advantage of the structure of the QBF formula given.
While the peak memory is higher for CAQE, the structure of the QBF encoding
allows it to handle the grounding bottleneck which we will see in the Organic
Synthesis problems. We leave experiments with other QBF solvers for future
work.

Figure 2: Solving times of M-simple and Q-Planner

.

Figure 3: Peak memory of M-simple and Q-planner

.

From the results on $20$ IPC domains, it is clear that (with current QBF
solvers) our QBF encoding is not a replacement for SAT based solvers, but
rather a complement for domains where grounding is hard due to many action
parameters.

##  6 Related Work

We first discuss some approaches in the literature that avoid grounding in SAT
encodings by allowing quantification, using EPR, CP, or SMT. Then we discuss
related work on QBF.

Navarro Pérez and Voronkov (2013) presented an encoding of planning problems
in EPR (Effectively Propositional Logic), a fragment of First Order Logic.
While EPR can encode planning problems with fluent dependencies, the
satisfiability problem of this class is NEXPTIME-complete (Lewis 1980).
Because we use only one universal block of variable branches, our QBF encoding
still stays in the 3rd level of the polynomial hierarchy, combining a compact
encoding with relatively efficient solving.

Other approaches, such as numerical planning as SMT (Satisfiability Modulo
Theories) by Bofill, Espasa, and Villaret (2016) and numerical planning as CP
(Constraint Programming) by Espasa et al. (2019), also avoid grounding for
compact encodings. It would be interesting to apply those approaches to
Organic Synthesis.

Cashmore, Fox, and Giunchiglia (2013) proposed a QBF encoding with _partial
grounding_ , which grounds a subset of the propositions and handles the
ungrounded propositions using universal variables. Our work extends their
partially grounded QBF encoding, whose core idea uses predicate variables to
represent ungrounded propositions and _universal variables for only one
object_. Equation 1 from Cashmore, Fox, and Giunchiglia (2013), shows the
prefix for their proposed encoding. In plain words, it states that there
exists an assignment to the grounded variables and action-lock variables
(i.e., ungrounded parameter variables) such that for all assignments of one
object, there exists an assignment to $n+1$ sets of predicate variables, such
that the constraints hold.

$\exists X^{g}_{1}\dots X^{g}_{n+1}\forall a_{1}\dots a_{m}\exists
X^{u}_{1}\dots X^{u}_{n+1}$ (1)

However, the problem with their encoding comes with using universal variables
to represent only one object. However, this leads to problems with propagating
untouched propositions at each time step. By quantifying over one object only,
_not all_ values of propositions are propagated. To avoid incorrect plans,
they must resort to _partial_ grounding: the restriction is that every
predicate can have at most one ungrounded parameter. This can become costly:
When a predicate parameter is grounded, all the corresponding action
parameters need to be grounded as well, resulting in a large number of
partially grounded actions.

We see our work as a generalisation of the technique by Cashmore, Fox, and
Giunchiglia (2013). We consider _object combinations_ in the universal layer
of the encoding, thus avoiding grounding completely. This results in more
compact QBF encodings. Since the software from partial grounding encoding is
not available to us we could not compare it with Q-planner. Partial grounding
of some parameters is trivial in our approach (it can be done on the domain
file directly), however, we expect that the result will be suboptimal. In case
of organic synthesis, partially grounding some predicates still results in
very large encodings.

The main focus of compact QBF encodings for reachability, synthesis and
planning has been on reducing the number of transition function copies
(Rintanen 2001; Cashmore, Fox, and Giunchiglia 2012). While avoiding unrolling
reduces the encoding size, it comes at the cost of losing inference between
different time steps. On the other hand, using universal quantification to
avoid grounding, while keeping the inference between time steps, might be a
better way to use the advances in the QBF solving, as shown for planning
problems in this paper. Since the encodings are generated directly from
(restricted) First-order Logic representations, the resulting encodings are
compact and more scalable.

##  7 Conclusion and Future Work

In this paper, we propose the Ungrounded Encoding for classical planning
problems to QBF, which results in compact encodings by avoiding grounding
completely. The size of this QBF encoding is linear in the number of action
names, predicates and the path length, and logarithmic in the number of
objects. We provide an open source implementation of the Ungrounded Encoding,
translating classical planning problems in PDDL to QBF problems in QCIR
format. The resulting QBF formulas can be preprocessed and solved by existing
QBF tools (we used Bloqqer and CAQE).

The experiments show that our encodings effectively avoid the memory
bottleneck due to grounding. This is relevant for domains with actions that
involve many objects, such as Organic Synthesis. Our main result is to solve
many instances of Organic Synthesis, which so far could not be handled by any
SAT/QBF based planner. We solve $58$ problems in the $4$ Organic Synthesis
domains. We compare our implementation with the state-of-the-art SAT based
planner Madagascar, which only solves $1$ instance, using $116$GB memory. We
also compare with the non-SAT based planners Fast Downward Stone Soup
(FDS-2018) and Powerlifted. FDS was the winner of the satisfying track in IPC
2018 and solves $31$ instances. Powerlifted avoids grounding actions, and
solves $65$ instances altogether.

#### Future Work.

There are several research directions from here. One direction is to extend
the Ungrounded Encoding to planning problems with uncertainty or planning with
adversaries. QBF encodings have been demonstrated to be useful for such
domains, such as conformant planning (Rintanen 1999, 2007). To this end, the
Ungrounded Encoding must be extended, in order to handle some dependencies
between state predicates, and to handle conditional effects.

Another direction is to improve the efficiency of the Ungrounded Encoding: One
could consider to incorporate automatically generated invariants (Rintanen
2008) to speed up the search. Similarly, one could consider extending the
Ungrounded Encoding with compact QBF encodings, such as the non-copying
Iterative Squaring Encoding (Rintanen 2001) and the Compact Tree Encoding
(Cashmore, Fox, and Giunchiglia 2012). These encodings could in principle lead
to an even more concise encoding (logarithmic in the length of the plan), but
we expect less spectacular benefits than compared to SAT encodings, since our
encoding is already quite small. It would also be interesting to investigate
ungrounded versions of _parallel plans_ (Rintanen, Heljanko, and Niemelä
2006), but currently the sequentiality of plans is deeply embedded in our
encoding.

Finally, we hope to inspire new research on pre-processing and solving QBF
problems, by submitting our problems to the QBFeval competition. Our encodings
are very concise, but the current QBF solvers do not yet take advantage of the
structure of the Ungrounded Encoding. While SAT solvers are rather mature, the
field of QBF solvers is still improving rapidly. An advance in QBF solvers
could make the Q-Planner approach competitive to the SAT approach for general
classical planning problems.

### Acknowledgments

We thank Michael Cashmore for discussions and clarifications on partially
grounded QBF encoding, Leander Tentrup for support regarding the CAQE QBF
solver, and Mikhail Soutchanski for providing original Organic Synthesis
benchmarks. The numerical results presented in this work were obtained at the
Centre for Scientific Computing, Aarhus (CSCAA).

## References

  * Biere, Lonsing, and Seidl (2011) Biere, A.; Lonsing, F.; and Seidl, M. 2011.  Blocked Clause Elimination for QBF.  In _CADE_ , volume 6803 of _Lecture Notes in Computer Science_ , 101–115. Springer.
  * Bofill, Espasa, and Villaret (2016) Bofill, M.; Espasa, J.; and Villaret, M. 2016.  The RANTANPLAN planner: system description.  _Knowl. Eng. Rev._ , 31(5): 452–464.
  * Cashmore, Fox, and Giunchiglia (2012) Cashmore, M.; Fox, M.; and Giunchiglia, E. 2012.  Planning as Quantified Boolean Formula.  In _ECAI_ , volume 242 of _Frontiers in Artificial Intelligence and Applications_ , 217–222. IOS Press.
  * Cashmore, Fox, and Giunchiglia (2013) Cashmore, M.; Fox, M.; and Giunchiglia, E. 2013.  Partially Grounded Planning as Quantified Boolean Formula.  In _ICAPS_. AAAI.
  * Corrêa et al. (2020) Corrêa, A. B.; Pommerening, F.; Helmert, M.; and Francès, G. 2020.  Lifted Successor Generation Using Query Optimization Techniques.  In _ICAPS_ , 80–89. AAAI Press.
  * Dershowitz, Hanna, and Katz (2005) Dershowitz, N.; Hanna, Z.; and Katz, J. 2005.  Bounded Model Checking with QBF.  volume 3569 of _Lecture Notes in Computer Science_ , 408–414. Springer.
  * Espasa et al. (2019) Espasa, J.; Coll, J.; Miguel, I.; and Villaret, M. 2019.  Towards lifted encodings for numeric planning in Essence Prime.  In _CP 2019 Workshop on Constraint Modelling and Reformulation_.
  * Fox and Long (2003) Fox, M.; and Long, D. 2003.  PDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains.  _J. Artif. Intell. Res._ , 20: 61–124.
  * Ghallab, Nau, and Traverso (2004) Ghallab, M.; Nau, D.; and Traverso, P. 2004.  _Automated Planning: theory and practice_.  Elsevier.
  * Haas (1987) Haas, A. R. 1987.  The case for domain-specific frame axioms.  In _The Frame Problem in Artificial Intelligence_ , 343–348. Elsevier.
  * Helmert (2011) Helmert, M. 2011.  The Fast Downward Planning System.  _CoRR_ , abs/1109.6051.
  * Helmert and Röger (2011) Helmert, M.; and Röger, G. 2011.  Fast Downward Stone Soup : A Baseline for Building Planner Portfolios.
  * Jussila and Biere (2007) Jussila, T.; and Biere, A. 2007.  Compressing BMC Encodings with QBF.  _Electronic Notes in Theoretical Computer Science_ , 174(3): 45–56.
  * Kautz and Selman (1992) Kautz, H. A.; and Selman, B. 1992.  Planning as Satisfiability.  In _ECAI_ , volume 92, 359–363.
  * Lewis (1980) Lewis, H. R. 1980.  Complexity results for classes of quantificational formulas.  _Journal of Computer and System Science_ , 21(3).
  * Masoumi, Antoniazzi, and Soutchanski (2015) Masoumi, A.; Antoniazzi, M.; and Soutchanski, M. 2015.  Modeling Organic Chemistry and Planning Organic Synthesis.  In _GCAI_ , volume 36 of _EPiC Series in Computing_ , 176–195. EasyChair.
  * Matloob and Soutchanski (2016) Matloob, R.; and Soutchanski, M. 2016.  Exploring Organic Synthesis with State-ofthe-Art Planning Techniques.
  * Navarro Pérez and Voronkov (2013) Navarro Pérez, J. A.; and Voronkov, A. 2013.  Planning with Effectively Propositional Logic.  In Voronkov, A.; and Weidenbach, C., eds., _Programming Logics - Essays in Memory of Harald Ganzinger_ , volume 7797 of _Lecture Notes in Computer Science_ , 302–316. Springer.
  * Rabe and Tentrup (2015) Rabe, M. N.; and Tentrup, L. 2015.  CAQE: A Certifying QBF Solver.  136–143. IEEE.
  * Rintanen (1999) Rintanen, J. 1999.  Constructing Conditional Plans by a Theorem-Prover.  _J. Artif. Intell. Res._ , 10: 323–352.
  * Rintanen (2001) Rintanen, J. 2001.  Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae.  In _International Conference on Logic for Programming Artificial Intelligence and Reasoning – LPAR 2001_ , volume 2250 of _Lecture Notes in Computer Science_ , 362–376. Springer.
  * Rintanen (2007) Rintanen, J. 2007.  Asymptotically optimal encodings of conformant planning in QBF.  In _AAAI_ , 1045–1050.
  * Rintanen (2008) Rintanen, J. 2008.  Regression for Classical and Nondeterministic Planning.  In _ECAI_ , volume 178 of _Frontiers in Artificial Intelligence and Applications_ , 568–572. IOS Press.
  * Rintanen (2014) Rintanen, J. 2014.  Madagascar: Scalable Planning with SAT.
  * Rintanen, Heljanko, and Niemelä (2006) Rintanen, J.; Heljanko, K.; and Niemelä, I. 2006.  Planning as satisfiability: parallel plans and algorithms for plan search.  _Artif. Intell._ , 170(12-13): 1031–1080.
  * Soos, Nohl, and Castelluccia (2009) Soos, M.; Nohl, K.; and Castelluccia, C. 2009.  Extending SAT Solvers to Cryptographic Problems.  In _SAT_ , volume 5584 of _Lecture Notes in Computer Science_ , 244–257. Springer.


[Jasper et al., 2007]
Jasper, A. W., Klippenstein, S. J., Harding, L. B., & Ruscic, B. 2007,
Journal of Physical Chemistry A, 111, 3932, 10.1021/jp067585p

[Javoy et al., 2003]
Javoy, S., Naudet, V., Abid, S., & Paillard, C. 2003, Experimental thermal and
fluid science, 27, 371

[Jessup et al., 2015]
Jessup, K. L., Marcq, E., Mills, F., et al. 2015, , 258, 309,

[Jodkowski et al., 1995]
Jodkowski, J. T., Ratajczak, E., Fagerström, K., et al. 1995,
Chemical Physics Letters, 240, 63, 10.1016/0009-2614(95)00470-O

[Johnson & de Oliveira, 2019]
Johnson, N. M., & de Oliveira, M. R. R. 2019, Earth and Space Science, 6,
1299, 10.1029/2018EA000536

[Jourdain et al., 1979]
Jourdain, J., Bras, G. L., & Combourieu, J. 1979, International Journal of
Chemical Kinetics, 11, 569

[Ju & Wang, 2010]
Ju, L., & Wang, D. 2010, International Journal of Chemical Kinetics, 42, 289

[Karkach & Osherov, 1999]
Karkach, S. P., & Osherov, V. I. 1999, , 110, 11918,

[Katayama et al., 1973]
Katayama, D. H., Huffman, R. E., & O'Bryan, C. L. 1973, , 59, 4309,

[Keller-Rudek et al., 2013]
Keller-Rudek, H., Moortgat, G. K., Sander, R., & Sörensen, R.
2013, Earth System Science Data Discussions, 6, 411,

[Keyser, 1980]
Keyser, L. 1980, The Journal of Physical Chemistry, 84, 11

[Kley & Welge, 1965]
Kley, D., & Welge, K. H. 1965, Zeitschrift Naturforschung Teil A, 20, 124,

[Klippenstein et al., 2009]
Klippenstein, S. J., Harding, L., Ruscic, B., et al. 2009, The Journal of
Physical Chemistry A, 113, 10241

[Klippenstein & Kim, 1993]
Klippenstein, S. J., & Kim, Y.-W. 1993, , 99, 5790,

[Knipovich et al., 1988]
Knipovich, O., Rubtsova, E., & Nekrasov, L. 1988, Volume Recombination Of
Nitrogen-Atoms In Afterglow Of Condensed Discharges,  MEZHDUNARODNAYA KNIGA
39 DIMITROVA UL., 113095 MOSCOW, RUSSIA

[Knollenberg & Hunten, 1980]
Knollenberg, R. G., & Hunten, D. M. 1980, ournal of Geophysical Research: Space Physics, 85, 8039

[Koch & Skibowski, 1971]
Koch, E. E., & Skibowski, M. 1971, Chemical Physics Letters, 9, 429,

[Krasnoperov et al., 1984]
Krasnoperov, L. N., Chesnokov, E. N., & Panfilov, V. N. 1984, Chemical
Physics, 89, 297, 10.1016/0301-0104(84)85317-3

[Krasnoperov & Michael, 2004]
Krasnoperov, L. N., & Michael, J. V. 2004, Journal of Physical Chemistry
A, 108, 5643, 10.1021/jp040186e

[Krasnopolsky, 1982]
Krasnopolsky, V. A. 1982, Moscow Izdatel Nauka

[Krasnopolsky, 2007]
—. 2007, , 191, 25, 10.1016/j.icarus.2007.04.028

[Krasnopolsky, 2008]
—. 2008, , 197, 377, 10.1016/j.icarus.2008.05.020

[Krasnopolsky, 2010]
—. 2010a, , 209, 314,

[Krasnopolsky, 2010]
—. 2010b, , 208, 539,

[Krasnopolsky, 2012]
—. 2012, , 218, 230, 10.1016/j.icarus.2011.11.012

[Krasnopolsky, 2013]
—. 2013, , 225, 570, 10.1016/j.icarus.2013.04.026

[Krasnopolsky, 2014]
—. 2014, , 237, 340, 10.1016/j.icarus.2014.04.043

[Krasnopolsky, 2015]
—. 2015, , 252, 327, 10.1016/j.icarus.2015.01.024

[Krasnopolsky, 2016]
—. 2016, , 274, 33, 10.1016/j.icarus.2016.03.010

[Krasnopolsky, 2017]
—. 2017, , 286, 134, 10.1016/j.icarus.2016.10.003

[Krasnopolsky & Pollack, 1994]
Krasnopolsky, V. A., & Pollack, J. B. 1994, , 109, 58,

[Krasnopolsky & Belyaev , 2016]
Krasnopolsky, V. A., & Belyaev, D. A. 2016, , 293, 114, 10.1016/j.icarus.2017.04.016

[Kronebusch & Berkowitz, 1976]
Kronebusch, P. L., & Berkowitz, J. 1976, International Journal of Mass
Spectrometry and Ion Processes, 22, 283, 10.1016/0020-7381(76)80088-5

[Kurbanov & Mamedov, 1995]
Kurbanov, M., & Mamedov, K. F. 1995, Kinetics and catalysis, 36

[Kurtén et al., 2010]
Kurtén, T., Lane, J. R., Jørgensen, S., & Kjaergaard, H. G.
2010, Physical Chemistry Chemical Physics (Incorporating Faraday
Transactions), 12, 12833, 10.1039/c0cp00383b

[Laidler & Wojciechowski, 1961]
Laidler, K. J., & Wojciechowski, B. W. 1961, Proceedings of the Royal
Society of London Series A, 260, 103, 10.1098/rspa.1961.0016

[Lamb et al., 1984]
Lamb, J., Mozurkewich, M., & Benson, S. 1984, Journal of physical chemistry
(1952), 88, 6441

[Lane & Kjaergaard, 2008]
Lane, J. R., & Kjaergaard, H. G. 2008, Journal of Physical Chemistry A,
112, 4958, 10.1021/jp710863r

[Lavendy et al., 1984]
Lavendy, H., Gandara, G., & Robbe, J. M. 1984, Journal of Molecular
Spectroscopy, 106, 395, 10.1016/0022-2852(84)90170-X

[Lavendy et al., 1987]
Lavendy, H., Robbe, J. M., & Gandara, G. 1987, Journal of Physics B
Atomic Molecular Physics, 20, 3067, 10.1088/0022-3700/20/13/018

[Lawrence, 1972]
Lawrence, G. M. 1972a, , 56, 3435, 10.1063/1.1677717

[Lawrence, 1972]
—. 1972b, , 57, 5616, 10.1063/1.1678271

[Lee & Chiang, 1982]
Lee, L., & Chiang, C. 1982, Chemical Physics Letters, 19, 3

[Lee et al., 1973]
Lee, L. C., Carlson, R. W., Judge, D. L., & Ogawa, M. 1973, ,
13, 1023, 10.1016/0022-4073(73)90075-7

[Lee et al., 1977]
Lee, L. C., Slanger, T. G., Black, G., & Sharpless, R. L. 1977, ,
67, 5602, 10.1063/1.434759

[Li et al., 2004]
Li, H.-Y., Pu, M., Ji, Y.-Q., Xu, Z.-F., & Feng, W.-L. 2004,
Chemical Physics, 307, 35, 10.1016/j.chemphys.2004.07.014

[Lias et al., 1970]
Lias, S. G., Collin, G. J., Rebbert, R. E., & Ausloos, P. 1970, ,
52, 1841, 10.1063/1.1673226

[Lilenfeld & Richardson, 1977]
Lilenfeld, H. V., & Richardson, R. J. 1977, , 67, 3991,

[Lin et al., 1978]
Lin, C. L., Rohatgi, N. K., & Demore, W. B. 1978, , 5, 113,

[Lincowski et al., 2021]
Lincowski, A. P., Meadows, V. S., Crisp, D., Akins, A. B., Schwieterman, E. W., Arney, G. N., Wong, M. L., Steffes, P. G., Parenteau, M. N., & Domagal-Goldman, S. 2021, , 908, L44

[Lingam & Loeb, 2020]
Lingam, M., & Loeb, A. 2020, arXiv e-prints, arXiv:2009.07835.

[Linkin et al., 1986]
Linkin, V., Kerzhanovich, V., Lipatov, A., et al. 1986, Science, 231, 1417

[Lissianski et al., 1995]
Lissianski, V., Yang, H., Qin, Z., et al. 1995, Chemical Physics
Letters, 240, 57, 10.1016/0009-2614(95)00496-Q

[Liu et al., 2010]
Liu, C.-F., Shih, S.-M., & Huang, T.-B. 2010, Industrial & engineering
chemistry research, 49, 9052

[Lofthus & Krupenie, 1977]
Lofthus, A., & Krupenie, P. H. 1977, Journal of Physical and Chemical
Reference Data, 6, 113, 10.1063/1.555546

[Lombos et al., 1967]
Lombos, B. A., Sauvageau, P., & Sandorfy, C. 1967, Journal of Molecular
Spectroscopy, 24, 253, 10.1016/0022-2852(67)90089-6

[Loomis & Walters, 1927]
Loomis, A., & Walters, J. 1927, Journal of the Franklin Institute, 203, 333

[Lovejoy et al., 1996]
Lovejoy, E. R., Hanson, D. R., & Huey, L. G. 1996, The Journal of Physical
Chemistry, 100, 19911

[Lovejoy et al., 1987]
Lovejoy, E. R., Wang, N.-S., & Howard, C. J. 1987, Journal of physical
chemistry, 91, 5749

[Lu et al., 2003]
Lu, C.-W., Wu, Y.-J., Lee, Y.-P., Zhu, R. S., & Lin, M. C. 2003,
Journal of Physical Chemistry A, 107, 11020, 10.1021/jp036025c

[Lukirskii et al., 1964]
Lukirskii, A., Brytov, I., & Zimkina, T. 1964, OptSp, 17, 234

[Lyons, 2008]
Lyons, J. R. 2008, Journal of Sulfur Chemistry, 29, 269

[Magnotta & Johnston, 1980]
Magnotta, F., & Johnston, H. S. 1980, , 7, 769,

[Maiorov et al., 2005]
Maiorov, B. S., Ignat'ev, N. I., Moroz, V. I., et al. 2005, Solar
System Research, 39, 267, 10.1007/s11208-005-0042-1

[Manion et al., 2015]
Manion, J., Huie, R., Levin, R., et al. 2015, URL: http://kinetics.nist.gov
(Date: 27.01. 2018)

[Marcq et al., 2013]
Marcq, E., Bertaux, J.-L., Montmessin, F., & Belyaev, D. 2013, Nature
Geoscience, 6, 25, 10.1038/ngeo1650

[Marcq et al., 2008]
Marcq, E., Bézard, B., Drossart, P., et al. 2008, Journal of
Geophysical Research (Planets), 113, E00B07, 10.1029/2008JE003074

[Marcq et al., 2005]
Marcq, E., Bézard, B., Encrenaz, T., & Birlan, M. 2005, ,
179, 375, 10.1016/j.icarus.2005.06.018

[Marcq et al., 2006]
Marcq, E., Encrenaz, T., Bézard, B., & Birlan, M. 2006, ,
54, 1360, 10.1016/j.pss.2006.04.024

[Marcq et al., 2015]
Marcq, E., Lellouch, E., Encrenaz, T., et al. 2015, , 113, 256,

[Marcq et al., 2018]
Marcq, E., Mills, F. P., Parkinson, C. D., & Vandaele, A. C. 2018,
, 214, 10, 10.1007/s11214-017-0438-5

[Marcq et al., 2020]
Marcq, E., Lea Jessup, K., Baggio, L., et al. 2020, , 335,
113368, 10.1016/j.icarus.2019.07.002

[Markiewicz et al., 2018]
Markiewicz, W. J., Petrova, E. V. & Shalygina, O. S. 2018, , 299, 272

[Markwalder et al., 1993]
Markwalder, B., Gozel, P., & Van den Bergh, H. 1993, The Journal of Physical
Chemistry, 97, 5260

[Marmo, 1953]
Marmo, F. F. 1953, Journal of the Optical Society of America (1917-1983), 43,

[Martínez et al., 2000]
Martínez, E., Albaladejo, J., Jiménez, E., Notario, A., &
Díaz de Mera, Y. 2000, Chemical Physics Letters, 329, 191,

[Martinotti et al., 1968]
Martinotti, F. F., Welch, M. J., & Wolf, A. P. 1968, Chemical Communications
(London), 115

[Masuoka & Samson, 1981]
Masuoka, T., & Samson, J. A. R. 1981, , 74, 1093,

[Materic & Smedley, 2011]
Materic, V., & Smedley, S. I. 2011, Industrial & engineering chemistry
research, 50, 5927

[Matsumi et al., 2002]
Matsumi, Y., Comes, F. J., Hancock, G., et al. 2002, Journal of
Geophysical Research (Atmospheres), 107, 4024, 10.1029/2001JD000510

[Matsunaga & Watanabe, 1967]
Matsunaga, F., & Watanabe, K. 1967, Sci. Light, 16, 31

[Matsunaga & Watanabe, 1967]
Matsunaga, F. M., & Watanabe, K. 1967, , 46, 4457,

[Matthes et al., 2017]
Matthes, K., Funke, B., Andersson, M. E., et al. 2017, Geoscientific
Model Development, 10, 2247, 10.5194/gmd-10-2247-2017

[McNesby & Okabe, 1964]
McNesby, J., & Okabe, H. 1964, Advances in Photochemistry, 3, 166

[McNesby et al., 1962]
McNesby, J. R., Tanaka, I., & Okabe, H. 1962, , 36, 605,

[Meadows & Crisp, 1996]
Meadows, V. S., & Crisp, D. 1996, , 101, 4595,

[Mentall et al., 1971]
Mentall, J. E., Gentieu, E. P., Krauss, M., & Neumann, D. 1971, ,
55, 5471, 10.1063/1.1675711

[Messerli et al., 2005]
Messerli, M. A., Amaral-Zettler, L. A., Zettler, E., et al. 2005, Journal of
experimental biology, 208, 2569

[Metzger & Cook, 1964]
Metzger, P. H., & Cook, G. R. 1964, , 41, 642,

[Michels & Wassenaar, 1950]
Michels, A., & Wassenaar, T. 1950, Physica, 16, 221,

[Miller et al., 2003]
Miller, J. A., Klippenstein, S. J., & Glarborg, P. 2003, Combustion and flame,
135, 357

[Mills, 1998]
Mills, F. P. 1998, PhD thesis, CALIFORNIA INSTITUTE OF TECHNOLOGY

[Mills et al., 2007]
Mills, F. P., Esposito, L. W., & Yung, Y. L. 2007, Washington DC
American Geophysical Union Geophysical Monograph Series, 176, 73,

[Mogul et al., 2021]
Mogul, R., Limaye, S. S., Way, M., & Cordova Jr, J. A. 2021, , e2020GL091327

[Molina et al., 1981]
Molina, L. T., Lamb, J. J., & Molina, M. J. 1981, , 8, 1008,

[Molina & Arguello, 1979]
Molina, M. J., & Arguello, G. 1979, , 6, 953,

[Monks et al., 1993]
Monks, P. S., Romani, P. N., Nesbitt, F. L., Scanlon, M., & Stief,
L. J. 1993, , 98, 17115, 10.1029/93JE01789

[Montoya et al., 2005]
Montoya, A., Sendt, K., & Haynes, B. S. 2005, Journal of Physical
Chemistry A, 109, 1057, 10.1021/jp047903p

[Moortgat & Warneck, 1975]
Moortgat, G. K., & Warneck, P. 1975, Zeitschrift Naturforschung Teil A,
30, 835, 10.1515/zna-1975-6-720

[Moroz et al., 1979]
Moroz, V. I., Moshkin, B. E., Ekonomov, A. P., et al. 1979, Soviet
Astronomy Letters, 5, 118

[Moroz et al., 1990]
Moroz, V. I., Spankuch, D., Titov, D. V., et al. 1990, Advances in
Space Research, 10, 77, 10.1016/0273-1177(90)90168-Y

[Moses et al., 1992]
Moses, J. I., Allen, M., & Yung, Y. L. 1992, , 99, 318,

[Moses et al., 2002]
Moses, J. I., Zolotov, M. Y., & Fegley, B. 2002, , 156, 76,

[Moule & Foo, 1971]
Moule, D. C., & Foo, P. D. 1971, , 55, 1262, 10.1063/1.1676214

[Mount & Moos, 1978]
Mount, G. H., & Moos, H. W. 1978, , 224, L35, 10.1086/182753

[Mousavipour et al., 2003]
Mousavipour, S. H., Namdar-Ghanbari, M. A., & Sadeghian, L. 2003,
Journal of Physical Chemistry A, 107, 3752, 10.1021/jp022291z

[Mousavipour et al., 2009]
Mousavipour, S. H., Pirhadi, F., & Habibagahi, A. 2009, Journal of
Physical Chemistry A, 113, 12961, 10.1021/jp905197h

[Mukhin et al., 1983]
Mukhin, L., Gel'man, B., Lamonov, N., et al. 1983, Kosmicheskie
Issledovaniya, 21, 225

[Mukhin et al., 1982]
Mukhin, L. M., Gelman, B. G., Lamonov, N. I., et al. 1982, Soviet
Astronomy Letters, 8, 216

[Murakami et al., 2003]
Murakami, Y., Onishi, S., Kobayashi, T., et al. 2003, Journal of
Physical Chemistry A, 107, 10996, 10.1021/jp030471i

[Myer & Samson, 1970]
Myer, J. A., & Samson, J. A. R. 1970, , 52, 266,

[Na et al., 1990]
Na, C. Y., Esposito, L. W., & Skinner, T. E. 1990, , 95, 7485,

[Nakata et al., 1965]
Nakata, R., Watanabe, K., & Matsunaga, F. 1965, Sci. Light Tokyo, 14, 54V71

[Nakayama et al., 1959]
Nakayama, T., Kitamura, M. Y., & Watanabe, K. 1959, , 30, 1180,

[Nakayama & Watanabe, 1964]
Nakayama, T., & Watanabe, K. 1964, , 40, 558,

[Natarajan et al., 1997]
Natarajan, K., Woiki, D., & Roth, P. 1997, International Journal of Chemical
Kinetics, 29, 35

[Nava & Stief, 1989]
Nava, D. F., & Stief, L. J. 1989, The Journal of Physical Chemistry, 93, 4044

[Nee & Lee, 1984]
Nee, J. B., & Lee, L. C. 1984, , 81, 31, 10.1063/1.447387

[Nicholas et al., 1979]
Nicholas, J. E., Amodio, C. A., & Baker, M. J. 1979, Journal of the Chemical
Society, Faraday Transactions 1: Physical Chemistry in Condensed Phases, 75,

[Nickolaisen et al., 1994]
Nickolaisen, S. L., Friedl, R. R., & Sander, S. P. 1994, The Journal of
Physical Chemistry, 98, 155

[Nuth & Glicker, 1982]
Nuth, J. A., & Glicker, S. 1982, , 28, 223,

[Okabe, 1970]
Okabe, H. 1970, , 53, 3507, 10.1063/1.1674525

[Okabe, 1978]
—. 1978, Photochemistry of small molecules (John Wiley &. Sons)

[Okabe, 1980]
—. 1980, , 72, 6642, 10.1063/1.439123

[Okabe, 1981]
—. 1981, , 75, 2772, 10.1063/1.442348

[Okabe, 1983]
—. 1983, , 78, 1312, 10.1063/1.444868

[Okabe & Becker, 1963]
Okabe, H., & Becker, D. A. 1963, , 39, 2549, 10.1063/1.1734060

[Okabe et al., 1971]
Okabe, H., Laufer, A. H., & Ball, J. J. 1971, , 55, 373,

[Oschlisniok et al., 2012]
Oschlisniok, J., Häusler, B., Pätzold, M., et al. 2012,
, 221, 940, 10.1016/j.icarus.2012.09.029

[Oyama et al., 1979]
Oyama, V. I., Carle, G. C., Woeller, F., & Pollack, J. B. 1979,
Science, 203, 802, 10.1126/science.203.4382.802

[Oyama et al., 1980]
Oyama, V. I., Carle, G. C., Woeller, F., et al. 1980, , 85, 7891,

[Padial et al., 1985]
Padial, N. T., Collins, L. A., & Schneider, B. I. 1985, , 298, 369,

[Pagsberg et al., 1979]
Pagsberg, P. B., Eriksen, J., & Christensen, H. 1979, Journal of Physical
Chemistry, 83, 582

[Parkinson et al., 2015]
Parkinson, C. D, Gao, P., Schulte, R., Bougher, S.W., Yung, Y.L., Bardeen, C.G., Wilquet, V., Vandaele, A.C., Mahieux, A., Tellmann, S., & Pätzold, M.. 2015, Planetary and Space Science, 113, 205

[Peralta et al., 2017]
Peralta, J., Lee, Y., Hueso, R., et al. 2017, Geophysical Research Letters,
44, 3907

[Petrova, 2018]
Petrova, E. V. 2018, , 306, 163

[Peucker-Ehrenbrink, 1996]
Peucker-Ehrenbrink, B. 1996, Geochimica et Cosmochimica Acta, 60, 3187

[Phillips et al., 1977]
Phillips, E., Lee, L. C., & Judge, D. L. 1977, , 18, 309,

[Phillips, 1981]
Phillips, L. F. 1981, Journal of Physical Chemistry, 85, 3994

[Pinto et al., 2021]
Pinto, J.P., Li, J., Mills, F.P., Marcq, E., Evdokimova, D., Belyaev, D. and Yung, Y.L.. 2021, Nature Communications, 12, 1

[Pollack et al., 1993]
Pollack, J. B., Dalton, J. B., Grinspoon, D., et al. 1993, ,
103, 1, 10.1006/icar.1993.1055

[Porter & Noyes Jr, 1959]
Porter, R. P., & Noyes Jr, W. A. 1959, Journal of the American Chemical
Society, 81, 2307

[Pouilly et al., 1983]
Pouilly, B., Robbe, J. M., Schamps, J., & Roueff, E. 1983, Journal of
Physics B Atomic Molecular Physics, 16, 437,

[Pritchard & Lauterbur, 1961]
Pritchard, J., & Lauterbur, P. 1961, Journal of the American Chemical Society,
83, 2105

[Ranjan et al., 2020]
Ranjan, S., Schwieterman, E. W., Harman, C., et al. 2020, , 896,
148, 10.3847/1538-4357/ab9363

[Rimmer & Helling, 2016]
Rimmer, P. B., & Helling, C. 2016, , 224, 9,

[Rimmer & Helling, 2019]
—. 2019, , 245, 20, 10.3847/1538-4365/ab5192

[Rimmer & Rugheimer, 2019]
Rimmer, P. B., & Rugheimer, S. 2019, , 329, 124,

[Rimmer et al., 2020]
Rimmer, P. B., Ferus, M., Waldmann, I. P., et al. 2020, , 888, 21,

[Robertson & Smith, 2006]
Robertson, R., & Smith, G. P. 2006, Journal of Physical Chemistry A, 110,
6673, 10.1021/jp055863z

[Roose et al., 1978]
Roose, T., Hanson, R., & Kruger, C. 1978, Shock tube and shock wave research,

[Rowe et al., 1998]
Rowe, B. R., Brownsword, R. A., Smith, I. W., et al. 1998, Journal of the
Chemical Society, Faraday Transactions, 94, 2889

[Roxlo & Mandl, 1980]
Roxlo, C., & Mandl, A. 1980, Journal of Applied Physics, 51, 2969,

[Sagan, 1975]
Sagan, C. 1975, Journal of Atmospheric Sciences, 32, 1079,

[Salahub & Sandorfy, 1971]
Salahub, D. R., & Sandorfy, C. 1971, Chemical Physics Letters, 8, 71,

[Samson & Cairns, 1964]
Samson, J. A., & Cairns, R. 1964, Journal of Geophysical Research, 69, 4583

[Samson & Cairns, 1965]
—. 1965, JOSA, 55, 1035

[Sandor & Clancy, 2005]
Sandor, B. J., & Clancy, R. T. 2005, , 177, 129,

[Sandor & Clancy, 2012]
—. 2012, , 220, 618, 10.1016/j.icarus.2012.05.016

[Sandor et al., 2010]
Sandor, B. J., Todd Clancy, R., Moriarty-Schieven, G., & Mills, F. P.
2010, , 208, 49, 10.1016/j.icarus.2010.02.013

[Sauter, 1931]
Sauter, F. 1931, Ann. Phys.(Leipzig), 11, 454

[Saxon et al., 1983]
Saxon, R. P., Lengsfield, B. H., I., & Liu, B. 1983, , 78, 312,

[Schaefer & Fegley, 2004]
Schaefer, L., & Fegley, B. 2004, , 168, 215,

[Schindler et al., 1996]
Schindler, R. N., Dethlefs, J., & Schmidt, M. 1996, Berichte der
Bunsengesellschaft für physikalische Chemie, 100, 1242

[Schoen, 1962]
Schoen, R. I. 1962, , 37, 2032, 10.1063/1.1733423

[Schurath et al., 1969]
Schurath, U., Tiedemann, P., & Schindler, R. N. 1969, The Journal of Physical
Chemistry, 73, 456

[Schürgers & Welge, 1968]
Schürgers, M., & Welge, K. H. 1968, Zeitschrift Naturforschung Teil A,
23, 1508, 10.1515/zna-1968-1011

[Seinfeld & Pandis, 2016]
Seinfeld, J. H., & Pandis, S. N. 2016, Atmospheric chemistry and physics: from
air pollution to climate change (John Wiley & Sons)

[Sellevåg et al., 2009]
Sellevåg, S. R., Georgievskii, Y., & Miller, J. A. 2009, Journal
of Physical Chemistry A, 113, 4457, 10.1021/jp8110524

[Selwyn et al., 1977]
Selwyn, G., Podolske, J., & Johnston, H. S. 1977, , 4, 427,

[Sendt & Haynes, 2005]
Sendt, K., & Haynes, B. S. 2005, Journal of Physical Chemistry A, 109,
8180, 10.1021/jp052622i

[Sendt et al., 2002]
Sendt, K., Jazbec, M., & Haynes, B. 2002, Proceedings of the Combustion
Institute, 29, 2439

[Senosiain et al., 2006]
Senosiain, J. P., Klippenstein, S. J., & Miller, J. A. 2006, Journal of
Physical Chemistry A, 110, 5772, 10.1021/jp054934r

[Shao et al., 2020]
Shao, W. D., Zhang, X., Bierson, C. J., & Encrenaz, T. 2020, Journal
of Geophysical Research (Planets), 125, e06195, 10.1029/2019JE006195

[Sharkey et al., 1994]
Sharkey, P., Sims, I. R., Smith, I. W., Bocherel, P., & Rowe, B. R. 1994,
Journal of the Chemical Society, Faraday Transactions, 90, 3609

[Shum & Benson, 1985]
Shum, L. G., & Benson, S. W. 1985, International journal of chemical kinetics,
17, 749

[Singleton & Cvetanović, 1988]
Singleton, D. L., & Cvetanović, R. J. 1988, Journal of Physical and
Chemical Reference Data, 17, 1377, 10.1063/1.555811

[Sinozaki et al., 1926]
Sinozaki, H., Hara, R., & Mitsukuri, S. 1926, Bulletin of the Chemical Society
of Japan, 1, 59

[Slack, 1976]
Slack, M. W. 1976, , 64, 228, 10.1063/1.431955

[Slanger & Black, 1982]
Slanger, T. G., & Black, G. 1982, , 77, 2432, 10.1063/1.444111

[Smith et al., 2006]
Smith, C. A., Pope, F. D., Cronin, B., Parkes, C. B., & Orr-Ewing,
A. J. 2006, Journal of Physical Chemistry A, 110, 11645,

[Smith et al., 1998]
Smith, N. S., Bénilan, Y., & Bruston, P. 1998, , 46, 1215,

[Smrekar et al., 2020]
Smrekar, S., Dyar, D., Helbert, J., Hensley, S., Nunes, D., & Whitten, J. 2020, VERITAS (Venus Emissivity, Radio Science, InSAR, Topography and Spectroscopy): A Proposed Discovery Mission. In European Planetary Science Congress EPSC2020-447

[Snellen et al., 2020]
Snellen, I. A. G., Guzman-Ramirez, L., Hogerheijde, M. R., Hygate,
A. P. S., & van der Tak, F. F. S. 2020, arXiv e-prints, arXiv:2010.09761.

[Steer & Knight, 1968]
Steer, R., & Knight, A. 1968, The Journal of Physical Chemistry, 72, 2145

[Stief et al., 1972]
Stief, L. J., Donn, B., Glicker, S., Gentieu, E. P., & Mentall,
J. E. 1972, , 171, 21, 10.1086/151253

[Stobbe, 1930]
Stobbe, M. 1930, Annalen der Physik, 399, 661

[Stock, 2008]
Stock, J. 2008, diploma thesis, Technische Universität Berlin, Straße
des 17. Juni 135, 10623 Berlin, Germany

[Stockwell & Calvert, 1978]
Stockwell, W. R., & Calvert, J. G. 1978, Journal of Photochemistry, 8, 193

[Stoeckel et al., 1985]
Stoeckel, F., Schuh, M. D., Goldstein, N., & Atkinson, G. H. 1985,
Chemical Physics, 95, 135, 10.1016/0301-0104(85)80154-3

[Stone & Rowley, 2005]
Stone, D., & Rowley, D. M. 2005, Physical Chemistry Chemical Physics
(Incorporating Faraday Transactions), 7, 2156, 10.1039/B502673C

[Strausz et al., 1968]
Strausz, O., Donovan, R., & De Sorgo, M. 1968, Berichte der Bunsengesellschaft
für physikalische Chemie, 72, 253

[Streit et al., 1976]
Streit, G. E., Howard, C. J., Schmeltekopf, A. L., Davidson, J. A., &
Schiff, H. I. 1976, , 65, 4761, 10.1063/1.432930

[Strom et al., 1994]
Strom, R. G., Schaber, G. G., & Dawsow, D. D. 1994, , 99, 10899,

[Stull, 1947]
Stull, D. R. 1947, Industrial & Engineering Chemistry, 39, 517

[Sun & Weissler, 1955]
Sun, H., & Weissler, G. L. 1955, , 23, 1160, 10.1063/1.1742205

[Surkov et al., 1987]
Surkov, I. A., Shcheglov, O. P., Ryvkin, M. L., Sheinin, D. M., &
Davydov, N. A. 1987, Kosmicheskie Issledovaniia, 25, 678

[Surkov et al., 1984]
Surkov, Y. A., Barsukov, V. L., Moskalyeva, L. P., Kharyukova, V. P.,
& Kemurdzhian, A. L. 1984, Lunar and Planetary Science Conference
Proceedings, 89, B393, 10.1029/JB089iS02p0B393

[Surkov et al., 1982]
Surkov, Y. A., Ivanova, V. F., Pudov, A. N., et al. 1982, Pisma v
Astronomicheskii Zhurnal, 8, 411

[Surkov et al., 1986]
Surkov, Y. A., Moskalyova, L. P., Kharyukova, V. P., et al. 1986, ,
91, E215, 10.1029/JB091iB13p0E215

[Takahashi & Miyazaki, 1977]
Takahashi, S., & Miyazaki, S. 1977, Bulletin of the Chemical Society of Japan,
50, 1627

[Tanaka et al., 1953]
Tanaka, Y., Inn, E. C., & Watanabe, K. 1953, The Journal of Chemical Physics,
21, 1651

[Tellinghuisen, 2003]
Tellinghuisen, J. 2003, Journal of Physical Chemistry A, 107, 753,

[Terraglio & Manganelli, 1967]
Terraglio, F. P., & Manganelli, R. M. 1967, Journal of the Air Pollution
Control Association, 17, 403

[Thompson et al., 1963]
Thompson, B. A., Harteck, P., & Reeves, R. R. 1963, , 68, 6431,

[Thompson, 2020]
Thompson, M. A. 2020, arXiv e-prints, arXiv:2010.15188.

[Titov, 1983]
Titov, D. V. 1983, Kosmicheskie Issledovaniia, 21, 401

[Titov et al., 2018]
Titov, D. V., Ignatiev, N. I., McGouldrick, K., Wilquet, V., &
Wilson, C. F. 2018, , 214, 126, 10.1007/s11214-018-0552-z

[Tizniti et al., 2010]
Tizniti, M., Le Picard, S. D., Canosa, A., Sims, I. R., & Smith, I.
W. M. 2010, Physical Chemistry Chemical Physics (Incorporating Faraday
Transactions), 12, 12702, 10.1039/C0CP00591F

[Toby et al., 1984]
Toby, S., Sheth, S., & Toby, F. S. 1984, International journal of chemical
kinetics, 16, 149

[Townsend et al., 2012]
Townsend, T. M., Allanic, A., Noonan, C. & Sodeau, J. R. 2012, Journal of Physical Chemistry A, 116, 4035

[Tsai et al., 2017]
Tsai, S.-M., Lyons, J. R., Grosheintz, L., et al. 2017, , 228, 20,

[Tsang et al., 2008]
Tsang, C. C. C., Irwin, P. G. J., Wilson, C. F., et al. 2008, Journal
of Geophysical Research (Planets), 113, E00B08, 10.1029/2008JE003089

[Tsang, 1987]
Tsang, W. 1987, Journal of physical and chemical reference data, 16, 471

[Tsang, 1992]
Tsang, W. 1992, Journal of Physical and Chemical Reference Data, 21, 753,

[Tsang & Hampson, 1986]
Tsang, W., & Hampson, R. F. 1986, Journal of Physical and Chemical
Reference Data, 15, 1087, 10.1063/1.555759

[Tsang & Herron, 1991]
Tsang, W., & Herron, J. T. 1991, Journal of Physical and Chemical
Reference Data, 20, 609, 10.1063/1.555890

[Tsang & Walker, 1992]
Tsang, W., & Walker, J. A. 1992, The Journal of Physical Chemistry, 96, 8378

[Tsuboi & Hashimoto, 1981]
Tsuboi, T., & Hashimoto, K. 1981, Combustion and Flame, 42, 61

[Tsuboi et al., 1981]
Tsuboi, T., Katoh, M., Kikuchi, S., & Hashimoto, K. 1981, Japanese
Journal of Applied Physics, 20, 985, 10.1143/JJAP.20.985

[Tsuchiya et al., 1997]
Tsuchiya, K., Kamiya, K., & Matsui, H. 1997, International Journal of Chemical
Kinetics, 29, 57

[Tsuchiya et al., 1996]
Tsuchiya, K., Yamashita, K., Miyoshi, A., & Matsui, H. 1996, The Journal of
Physical Chemistry, 100, 17202

[Tsuchiya et al., 1994]
Tsuchiya, K., Yokoyama, K., Matsui, H., Oya, M., & Dupre, G. 1994, The Journal
of Physical Chemistry, 98, 8419

[Turányi et al., 2012]
Turányi, T., Nagy, T., Zsély, I. G., et al. 2012, International
Journal of Chemical Kinetics, 44, 284

[Vaghjiani & Ghanshyam, 1993]
Vaghjiani, & Ghanshyam, L. 1993, , 99, 5936, 10.1063/1.465917

[van Dishoeck, 1987]
van Dishoeck, E. F. 1987, , 86, 196, 10.1063/1.452610

[van Dishoeck & Dalgarno, 1984]
van Dishoeck, E. F., & Dalgarno, A. 1984, , 59, 305,

[Vandaele et al., 2017]
Vandaele, A. C., Korablev, O., Belyaev, D., et al. 2017a,
, 295, 16, 10.1016/j.icarus.2017.05.003

[Vandaele et al., 2017]
—. 2017b, , 295, 1, 10.1016/j.icarus.2017.05.001

[Vandeputte et al., 2010]
Vandeputte, A. G., Reyniers, M.-F., & Marin, G. B. 2010, Journal of
Physical Chemistry A, 114, 10531, 10.1021/jp103357z

[Verner et al., 1996]
Verner, D. A., Ferland, G. J., Korista, K. T., & Yakovlev, D. G. 1996,
, 465, 487, 10.1086/177435

[Verner & Yakovlev, 1995]
Verner, D. A., & Yakovlev, D. G. 1995, , 109, 125

[Vidal et al., 2017]
Vidal, T. H. G., Loison, J.-C., Jaziri, A. Y., et al. 2017, ,
469, 435, 10.1093/mnras/stx828

[Wakelam et al., 2012]
Wakelam, V., Herbst, E., Loison, J. C., et al. 2012, , 199, 21,

[Walker & Kelly, 1972]
Walker, T. E. H., & Kelly, H. P. 1972, Chemical Physics Letters, 16, 511,

[Wang & Hou, 2005]
Wang, B., & Hou, H. 2005, Chemical Physics Letters, 410, 235,

[Wang et al., 1998]
Wang, J., Novaro, O., Bokhimi, X., et al. 1998, Materials letters, 35, 317

[Wang & Howard, 1990]
Wang, N. S., & Howard, C. J. 1990, Journal of physical chemistry, 94, 8787

[Watanabe, 1954]
Watanabe, K. 1954, , 22, 1564, 10.1063/1.1740459

[Watanabe, 1958]
—. 1958, Advances in Geophysics, 5, 153,

[Watanabe & Jursa, 1964]
Watanabe, K., & Jursa, A. S. 1964, , 41, 1650,

[Watanabe et al., 1967]
Watanabe, K., Matsunaga, F. M., & Sakai, H. 1967, , 6, 391,

[Watanabe & Sood, 1965]
Watanabe, K., & Sood, S. 1965, Sci. Light, 14, 36

[Watanabe & Zelikoff, 1953]
Watanabe, K., & Zelikoff, M. 1953, Journal of the Optical Society of
America (1917-1983), 43, 753

[Watson et al., 1976]
Watson, R., Machado, G., Fischer, S., & Davis, D. D. 1976, , 65,
2126, 10.1063/1.433369

[Weast, 1971]
Weast, R. 1971, CRC Handbook of Chemistry and Physics: A Ready-reference Book
of Chemical and Physical Data, CRC handbook series (Chemical Rubber Company).

[Weaver et al., 1976]
Weaver, J., Meagher, J., & Heicklen, J. 1976, Journal of Photochemistry, 6,

[Wei & Timmons, 1975]
Wei, C.-N., & Timmons, R. B. 1975, , 62, 3240,

[West & Berry, 1974]
West, G. A., & Berry, M. J. 1974, , 61, 4700,

[Williams & Golden, 1993]
Williams, L. R., & Golden, D. M. 1993, , 20, 2227

[Wilquet et al., 2012]
Wilquet, V., Drummond, R., Mahieux, A., et al. 2012, , 217, 875,

[Wilquet et al., 2009]
Wilquet, V., Fedorova, A., Montmessin, F., et al. 2009, Journal of
Geophysical Research (Planets), 114, E00B42, 10.1029/2008JE003186

[Wilson et al., 1981]
Wilson, W. J., Klein, M. J., Kahar, R. K., et al. 1981, , 45,
624, 10.1016/0019-1035(81)90029-4

[Wine et al., 1988]
Wine, P., Wells, J., & Nicovich, J. 1988, The Journal of Physical Chemistry,
92, 2223

[Woiki & Roth, 1995]
Woiki, D., & Roth, P. 1995, International journal of chemical kinetics, 27, 59

[Woitke et al., 2018]
Woitke, P., Helling, C., Hunter, G. H., et al. 2018, , 614, A1,

[Woitke et al., 2020]
Woitke, P., Herbort, O., Helling, C., et al. 2020, arXiv e-prints,

[Wooldridge et al., 1996]
Wooldridge, S. T., Hanson, R. K., & Bowman, C. T. 1996, International Journal
of Chemical Kinetics, 28, 245

[Wu & Judge, 1981]
Wu, C. Y. R., & Judge, D. L. 1981, , 74, 3804,

[Wu et al., 2007]
Wu, Y.-J., Lu, H.-C., Chen, H.-K., et al. 2007, , 127, 154311,

[Xu & Lin, 2009]
Xu, S., & Lin, M.-C. 2009, International Journal of Chemical Kinetics, 41, 667

[Xu & Sun, 1999]
Xu, Z.-F., & Sun, C.-C. 1999, Journal of Molecular Structure: THEOCHEM, 459,

[Xu & Sun, 1998]
Xu, Z.-F., & Sun, J.-Z. 1998, Journal of Physical Chemistry A, 102, 1194,

[Yamamoto, 2014]
Yamamoto, M. 2014, Earth, Planets, and Space, 66, 27,

[Yasunaga et al., 2008]
Yasunaga, K., Kubo, S., Hoshikawa, H., Kamesawa, T., & Hidaka, Y. 2008,
International Journal of Chemical Kinetics, 40, 73

[Yaws, 1999]
Yaws, C. 1999, Chemical Properties Handbook, Chemical engineering books
(McGraw-Hill Education).

[Yoshimura et al., 1992]
Yoshimura, M., Koshi, M., Matsui, H., Kamiya, K., & Umeyama, H.
1992, Chemical Physics Letters, 189, 199,

[Yoshino et al., 1993]
Yoshino, K., Esmond, J. R., Freeman, D. E., & Parkinson, W. H. 1993,
, 98, 5205, 10.1029/93JD00028

[Young, 1973]
Young, A. T. 1973, , 18, 564, 10.1016/0019-1035(73)90059-6

[Young, 1972]
Young, L. D. G. 1972, , 17, 632, 10.1016/0019-1035(72)90029-2

[Yung & Demore, 1982]
Yung, Y. L., & Demore, W. B. 1982, , 51, 199,

[Yung et al., 2009]
Yung, Y. L., Liang, M. C., Jiang, X., et al. 2009, Journal of
Geophysical Research (Planets), 114, E00B34, 10.1029/2008JE003094

[Zahnle et al., 2016]
Zahnle, K., Marley, M. S., Morley, C. V., & Moses, J. I. 2016, ,
824, 137, 10.3847/0004-637X/824/2/137

[Zanchet et al., 2018]
Zanchet, A., del Mazo, P., Aguado, A., et al. 2018, Physical Chemistry
Chemical Physics (Incorporating Faraday Transactions), 20, 5415,

[Zasova et al., 2007]
Zasova, L., Ignatiev, N., Khatuntsev, I., & Linkin, V. 2007, Planetary and
Space Science, 55, 1712

[Zasova et al., 1993]
Zasova, L. V., Moroz, V. I., Esposito, L. W., & Na, C. Y. 1993,
, 105, 92, 10.1006/icar.1993.1113

[Zelikoff & Watanabe, 1953]
Zelikoff, M., & Watanabe, K. 1953, Journal of the Optical Society of
America (1917-1983), 43, 756

[Zelikoff et al., 1953]
Zelikoff, M., Watanabe, K., & Inn, E. C. Y. 1953, , 21, 1643,

[Zhang et al., 1998]
Zhang, Q., Wang, H., Dalla Lana, I. G., & Chuang, K. T. 1998, Industrial &
engineering chemistry research, 37, 1167

[Zhang et al., 2012]
Zhang, X., Liang, M. C., Mills, F. P., Belyaev, D. A., & Yung, Y. L.
2012, , 217, 714, 10.1016/j.icarus.2011.06.016

[Zhang et al., 2010]
Zhang, X., Liang, M.-C., Montmessin, F., et al. 2010, Nature
Geoscience, 3, 834, 10.1038/ngeo989

[Zhang & Bauer, 1997]
Zhang, Y.-X., & Bauer, S. 1997, The Journal of Physical Chemistry B, 101, 8717

[Zimmer et al., 2016]
Zimmer, K., Zhang, Y., Lu, P., et al. 2016, Computers and Geosciences,
90, 97, 10.1016/j.cageo.2016.02.013