CSS Minification via Constraint Solving(Technical Report)
Matthew Hague1 , Anthony W. Lin2,3 and Chih-Duo Hong3
1
2Royal Holloway, University of London, UK
Technische Universität Kaiserslautern, Germany
3
University of Oxford, UK
Abstract

Minification is a widely-accepted technique which aims at reducing the size of the code transmitted over the web. This paper concerns the problem of semantic-preserving minification of Cascading
Style Sheets (CSS) — the de facto language for styling web documents — based on merging similar
rules.
The cascading nature of CSS makes the semantics of CSS files sensitive to the ordering of rules in
the file. To automatically identify rule-merging opportunities that best minimise file size, we reduce
the rule-merging problem to a problem concerning “CSS-graphs”, i.e., node-weighted bipartite graphswith a dependency ordering on the edges, where weights capture the number of characters.
Constraint solving plays a key role in our approach. Transforming a CSS file into a CSS-graphproblem requires us to extract the dependency ordering on the edges (an NP-hard problem), which
requires us to solve the selector intersection problem. To this end, we provide the first full formalisation of CSS3 selectors (the most stable version of CSS) and reduce their selector intersection problem
to satisfiability of quantifier-free integer linear arithmetic, for which highly-optimised SMT-solvers
are available. To solve the above NP-hard graph optimisation problem, we show how Max-SAT
solvers can be effectively employed. We have implemented our rule-merging algorithm, and tested
it against approximately 70 real-world examples (including examples from each of the top 20 mostpopular websites). We also used our benchmarks to compare our tool against six well-known minifiers (which implement other optimisations). Our experiments suggest that our tool produced larger
savings. A substantially better minification rate was shown when our tool is used together with theseminifiers.

1

Introduction

Minification [62, Chapter 12] is a widely-accepted technique in the web programming literature thataims at decreasing the size of the code transmitted over the web, which can directly improve theresponse-time performance of a website. Page load time is of course crucial for users’ experience,
which impacts the performance of an online business and is increasingly being included as a ranking
factor by search engines [61]. Minification bears a resemblance to traditional code compilation. In particular, it is applied only once right before deploying the website (therefore, its computation time does
not impact the page load time). However, they differ in at least two ways. First, the source and target
languages for minification are the same (high-level) languages. The code to which minification can beapplied is typically JavaScript or CSS, but it can also be HTML, XML, SVG, etc. Second, minification
applies various semantic-preserving transformations with the objective of reducing the size of the code.
This paper concerns the problem of minifying CSS (Cascading Style Sheets), which is the de facto
language for styling web documents (HTML, XML, etc.) as developed and maintained by the World
Wide Web Constortium (W3C) [4]. We will minify the CSS without reference to the documents it may
be designed to style. We refer the reader to Section 9 for a discussion of document-independent anddocument-dependent related work.
1

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

A CSS file consists of a list of CSS rules, each containing a list of selectors — each selecting nodes
in the Document Object Model (DOM), which is a tree structure representing the document — and a listof declarations, each assigning values to selected nodes’ display attributes (e.g. blue to the property
color). Real-world CSS files can easily have many rules (in the order of magnitude of 1000), e.g., see
the statistics for popular sites [1] on http://cssstats.com/. As Souders wrote in his book [62],which is widely regarded as the bible of web performance optimisation:
The greatest potential for [CSS file] size savings comes from optimizing CSS — merging identical classes, removing unused classes, etc. This is a complex problem, given theorder-dependent nature of CSS (the essence of why it’s called cascading). This area warrants further research and tool development.
More and more CSS minifiers have been, and are being, developed. These include YUI Compressor[59], cssnano [13], minify [16], clean-css [51], csso [19], and cssmin [8], to name a few.
Such CSS minifiers apply various syntactic transformations, typically including removing whitespacecharacters and comments, and using abbreviations (e.g. #f60 instead of #ff6600 for the colour
orange).
In this paper, we propose a new class of CSS transformations based on merging similar or duplicate
rules in the CSS file (thereby removing repetitions across multiple rules in the file) that could reduce
file size while preserving the rendering information. To illustrate the type of transformations that we
focus on in this paper (a more detailed introduction is given in Section 2), consider the following simple
CSS file.
#a { color:red; font-size:large }#c { color:green }#b { color:red; font-size:large }The selector #a selects a node with ID a (if it exists). Note that the first and the third rules above havethe same property declarations. Since one ID can be associated with at most one node in a DOM-tree,
we can merge these rules resulting in the following equivalent file.
#a, #b { color:red; font-size:large }#c { color:green }Identifying such a rule-merging-based minification opportunity — which we shall call merging opportunity for short — in general is non-trivial since a CSS file is sensitive to the ordering of rules that may
match the same node, i.e., the problem mentioned in Souders’ quote above. For example, let us assume
that the three selectors #a, #b, and #c in our CSS example instead were .a, .b, and .c, respectively.
The selector .a selects nodes with class a. Since a class can be associated with multiple nodes in a
DOM-tree, the above merging opportunity could change how a page is displayed and therefore would
not be valid, e.g., consider a page with an element that has two classes, .b and .c. This element would
be displayed as red by the original file (since red appears later), but as green by the file after applying
the transformation. Despite this, in this case we would still be able to merge the subrules of the first andthe third rules (associated with the font-size property) resulting in the following smaller equivalentfile:.a { color:red }.c { color:green }.b { color:red }.a, .b { font-size:large }2

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. HongThis example suggests two important issues. First, identifying a merging opportunity in a general way
requires a means of checking whether two given selectors may intersect, i.e., select the same node insome document tree. Second, a given CSS file could have a large number of merging opportunities at thesame time (the above example has at least two). Which one shall we pick? There are multiple answers tothis question. Note first that merging rules can be iterated multiple times to obtain increasingly smaller
CSS files. In fact, we can define an optimisation problem which, given a CSS file, computes a sequenceof applications of semantic-preserving merging rules that yields a globally minimal CSS file. Finding
a provably globally minimal CSS file is a computationally difficult problem that seems well beyond
the reach of current technologies (constraint solving, and otherwise). Therefore, we propose to use thesimple greedy strategy: while there is a merging opportunity that can make the CSS file smaller, apply
an optimal one, i.e., a merging opportunity that reduces the file size the most1 . There are now two
problems to address. First, can we efficiently find an optimal merging opportunity for a given CSS file?
This paper provides a positive answer to this question by exploiting a state-of-the-art constraint solving
technology. Second, there is a potential issue of getting stuck at a local minimum (as is common withany optimisation method based on gradient descent). Does the greedy strategy produce a meaningful
space saving? As we will see in this paper, the greedy approach could already produce space savings
that are beyond the reach of current CSS minification technologies.

1.1

Contributions

We first formulate a general class of semantic-preserving transformations on CSS files that captures
the above notion of merging “similar” rules in a CSS file. Such a program transformation has a clean
graph-theoretic formulation (see Section 4). Loosely speaking, a CSS rule corresponds to a biclique(complete bipartite graph) B, whose edges connect nodes representing selectors and nodes representing
property declarations. Therefore, a CSS file F corresponds to a sequence of bicliques that covers all of
the edges in the bipartite graph G which is constructed by taking the (non-disjoint) union of all bicliques
in F . Due to the cascading nature of CSS, the file F also gives rise to an (implicit) ordering ≺ on theedges of G. Therefore, any new CSS file F ′ that we produce from F must also be a valid covering of
the edges of G and respect the order ≺. As we will see, the above notion of merging opportunity can be
defined as a pair (B, j) of a new rule B and a position j in the file, and that applying this transformationentails inserting B in position j and removing all redundant nodes (i.e. either a selector or a property
declaration) in rules at position i < j.
Several questions remain. First is how to compute the edge order ≺. The core difficulty of this problem is to determine whether two CSS selectors can be matched by the same node in some document tree
(a.k.a. the selector intersection problem). Second, among the multiple potential merging opportunities,
how do we automatically compute a rule-merging opportunity that best minimises the size of the CSS
file. We provide solutions to these questions in this paper.
Computing the edge order ≺. In order to handle the selector intersection problem, we first provide
a complete formalisation of CSS3 selectors [15] (currently the most stable version of CSS selectors).
We then give a polynomial-time reduction from the selector intersection problem to satisfiability overquantifier-free theory of integer linear arithmetic, for which highly optimised SMT-solvers (e.g. Z3[18]) are available. To achieve this reduction, we provide a chain of polynomial-time reductions. First,
we develop a new class of automata over data trees [9], called CSS automata, which can capture theexpressivity of CSS selectors. This reduces the selector intersection problem to the language intersection
problem for CSS automata. Second, unlike the case for CSS selectors, the languages recognised by
1 Not to be confused with the smallest CSS file that is equivalent with the original file, which in general cannot be obtained byapplying a single merging

3

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. HongCSS automata enjoy closure under intersection. [.b .a and .c .a are individually CSS selectors,
however their conjunction is not a CSS selector2 .] This reduces language intersection of CSS automata
to language non-emptiness of CSS automata. To finish this chain of reductions, we provide a reduction
from the problem of language non-emptiness of CSS automata to satisfiability over quantifier-free theoryof integer linear arithmetic. The last reduction is technically involved and requires insights from logic
and automata theory, which include several small model lemmas (e.g. the sufficiency of considering
trees with a small number of node labels that can be succinctly encoded). This is despite the fact thatCSS selectors may force the smallest satisfying tree to be exponentially big.
Formulation of the “best” rule-merging opportunity and how to find it. Since our objective is tominimise file size, we may equip the graph G by a weight function wt which maps each node to thenumber of characters used to define it (recall that a node is either a selector or a property declaration).
Hence, the function wt allows us to define the size of a CSS file F (i.e. a covering of G respecting ≺) bytaking the sum of weights wt(v) ranging over all nodes v in F . The goal, therefore, is to find a merging
opportunity (B, j) of F that produces F ′ with a minimum file size. We show how this problem can beformulated as a (partially weighted) Max-SAT instance [3] in such a way that several existing Max-SAT
solvers (including Z3 [7] and MaxRes [46]) can handle it efficiently. This Max-SAT encoding is nontrivial: the naive encoding causes Max-SAT solvers to require prohibitively long run times even on small
examples. A naive encoding would allow the Max-SAT solver to consider any rule constructed from thenodes of the CSS file, and then contain clauses that prohibit edges that do not exist in the original CSS
file (as these would introduce new styling properties). Our encoding forces the Max-SAT solver to only
consider rules that do not introduce new edges. We do this by enumerating all maximal bicliques in thegraph G (maximal with respect to set inclusion) and developing an encoding that allows the Max-SAT
solver to only consider rules that are contained within a maximal biclique. We employ the algorithm
from [36] for enumerating all maximal bicliques in a bipartite graph, which runs in time polynomialin the size of the input and output. Therefore, to make this algorithm run efficiently, the number ofmaximal bicliques in the graph G cannot be very large. Our benchmarking (using approximately 70
real-world examples including CSS files from each of the top 20 websites [1]) suggests that this is thecase for graphs G generated by CSS files (with the maximum ratio between the number of bicliques
and the number of rules being 2.05). Our experiments suggest that the combination of the enumeration
algorithm of [36] and Z3 [7] makes the problem of finding the best merging opportunity for CSS files
practically feasible.
Experiments We have implemented our CSS minification algorithm in the tool S AT CSS which greedily searches for and applies the best merging opportunity to a given CSS file until no more rule-merging
can reduce file size. This will be made available in the supplementary material. The source code and aworking disk image are also available from the following URLs:
https://github.com/matthewhague/sat-css-tool
http://www.cs.rhul.ac.uk/home/hague/sat-css-tool.img.txz
Our tool utilises Z3 [18, 7] as a backend solver for Max-SAT and SMT over integer linear arithmetic.
We have tested our tool on around 70 examples from real-world websites (including examples fromeach of the top 20 websites [1]) with promising experimental results. We found that S AT CSS (which
only performs rule-merging) yields larger savings on our benchmarks in comparison to six popular CSS
minifiers [60], which support many other optimisations but not rule-merging. More precisely, when
run individually, S AT CSS reduced the file size by a third quartile of 6.90% and a median value of
2 The conjunction can be expressed by the selector group .b

4.c .a, .c .b .a, .b.c .a.

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong3.79%. The six mainstream minifiers achieved savings with third quantiles and medians up to 5.45%
and 3.29%, respectively. Since these are orthogonal minification opportunities, one might suspect that
applying these optimisations together could further improve the minification performance, which iswhat we discover during our experiments. More precisely, when we run our tool after running any
one of these minifiers, the third quartile of the savings can be increased to 8.26% and the median to
4.70%. The additional gains obtained by our tool on top of the six minifiers (as a percentage of theoriginal file size) have a third quartile of 5.03% and a median value of 2.80%, Moreover, the ratiosof the percentage of savings made by S AT CSS to the percentage of savings made by the six minifiers
have third quartiles of at least 136% and medians of at least 48%. In fact, in the case of cleancss
which has a third quartile saving of 5.26% and median saving of 3.03%, applying S AT CSS thereafter
results in a third quartile saving of 9.50% and median saving of 6.10%. These figures clearly indicate
a substantial proportion of extra space savings made by S AT CSS. See Table 1 and Figure 15 for moredetailed statistics.

1.2

Organisation

Section 2 provides a gentle and more detailed introduction (by example) to the problem of CSS minification via rule-merging. Preliminaries (notation, and basic terminologies) can be found in Section 3. In
Section 4 we formalise the rule-merging problem in terms of what we will call CSS-graphs. In Section 5,
we provide a formalisation of CSS3 selectors and an outline of an algorithm for solving their intersection problem, from which we can extract the edge order of a CSS-graph that is required when reducing
the rule-merging problem to the edge-covering problem of CSS-graphs. Since the algorithm solving theselector intersection problem is rather intricate, we dedicate one full section (Section 6) for it. In Section
7 we show how Max-SAT solvers can be exploited to solve the rule-merging problem of CSS-graphs.
We describe our experimental results in Section 8. In Section 9 we give a detailed discussion of related
work. Finally, we conclude in Section 10. Additional details can be found in the appendix. The Python
code and benchmarks for our tool have been included in the supplementary material, with a brief user
guide. A full artefact, including virtual machine image will be included when appropriate. These arepresently available from the URLs above.

2

CSS Rule-Merging: Example and Outline

In this section, we provide a gentler and more detailed introduction to CSS minification via merging
rules, while elaborating on the difficulties of the problem. We also give a general overview of thealgorithm, which may serve as a guide to the article. We begin by giving a basic introduction to HTMLand CSS. Our formal models of HTML and CSS are given in Section 5.

2.1

HTML and CSS

In this section we give a simple example to illustrate HTML and CSS. Note, in this article our analysis
takes as input a CSS file only. We cover HTML here to aid the description of CSS.
An HTML document is given in Figure 1. The format is similar to (but not precisely) XML, andis organised into a tree structure. The root node is the html element (or tag), and its two children are
the head and body nodes. These contain page header information (particularly the title), which is notdirectly displayed, and the main page contents respectively.
The body node contains two children which represent the page content. The first child is a div
element, which is used to group together parts of the page for the convenience of the developer. In thiscase, the developer has chosen to collect all parts of the page containing the displayed heading of the5

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong<html><head><title>Shopping List</title></head><body><div id="heading"><img class="banner" src="banner.jpg"/><h1>An Example HTML Document</h1></div><ul><li id="apple" class="fruit">Apple</li><li id="broccoli">Broccoli</li></ul></body></html>Figure 1: A simple HTML document.

html

body

head

title

div
id="heading"imgclass="banner"
src="header.jpg"

ul

h1

li
id="apple"
class="fruit"li
id="broccoli"

Figure 2: The HTML file in Figure 1 drawn as a tree.

page into one div. This div has an id which takes the value heading. Values specified in this way
are called attributes. ID attributes uniquely identify a given node in the HTML, that is, no two nodes
should have the same ID. The div has two children, which are an image (img) element and a textual
heading (h1). The source of the image is given by src, which is also an attribute. The image also
has a class attribute which takes the value banner. The class attribute is used to distinguish nodes
which have the same tag. For example, the developer may want an image with the class banner to be
displayed differently to an image with the class illustration.
The second child of the body node is an unordered list (ul). This lists contains two food items,with appropriate ID and class attributes.
To emphasize the tree structure, we give in Figure 2 the same HTML document drawn as a tree. We
will give a refined version of this diagram in Section 5 when defining DOM trees formally.
A CSS file consists of a sequence of rules, each of the form
selectors { declarations }where selectors contains one or more (node-)selectors (separated by commas) and declarations contains
a sequence of (visual) property declarations (separated by semicolons). An example CSS file containing
two rules is given in Figure 3.
The semantics of a rule is simple: if a node can be matched by at least one of the selectors, then label
the node by all the visual properties in the rule. Both rules in Figure 3 have one selector. The selector
6

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

img.banner { width: 100% }#heading h1 { font-size: 30pt; font-weight: bold }Figure 3: An example CSS file.

in the first rule img.banner matches all img elements which have the class banner. The notation. is used to indicate a class. Thus, this rule will match the img node in our example document and will
specify that the image is to be wide.
The second selector demonstrates that selectors may reason about the structure of the tree. The#heading means that the match should begin at the node with ID heading. Then, the space means
the match should move to any descendent of the #heading node, i.e., any node contained within thediv with ID heading in our example page. Next, the h1 is used to choose h1 elements. Thus, thisselector matches any node with element h1 that occurs below a node with ID heading. The text ofany such match should be rendered in a 30pt bold font.
There are many other features of selectors. These are described in full in Section 5.

2.2

CSS Rule-Merging by Example

We will now discuss more advanced features of CSS files and give an example of rule-merging. Figure
4 contains a simple CSS file (with four rules).
#apple { color:blue; font-size:small }.fruit, #broccoli { color:red; font-size:large }#orange { color:blue }#tomato { color:red; font-size:large;
background-color:lightblue }Figure 4: A simple example of a CSS file.

The sequence of rules in a file is applied to a node v in a “cascading” fashion (hence the nameCascading Style Sheets). That is, read the rules from top to bottom and check if v can be matched byat least one selector in the rule. If so, assign the properties to v (perhaps overriding previously assigned
properties, e.g., color) provided that the selectors matching v in the current rule have higher “values”(a.k.a. specificities) than the selectors previously matching v. Intuitively, the specificity of a selector[15] can be calculated by taking a weighted sum of the number of classes, IDs, tag names, etc. in theselector, where IDs have higher weights than classes, which in turn have higher weights than tag names.
For example, let us apply this CSS file to a node matching .fruit and #apple. In this case, theselectors in the first (#apple) and the second rules (.fruit) are applicable. However, since #apple
has a higher specificity than .fruit, the node gets labels color:blue and font-size:small.
Two syntactically different CSS files could be “semantically equivalent” in the sense that, on each
DOM tree T , both CSS files will precisely yield the same tree T ′ (which annotates T with visual
information). In this paper, we only look at semantically equivalent CSS files that are obtained bymerging similar rules. Given a CSS rule R, we say that it is subsumed by a CSS file F if each possible
selector/property combination in R occurs in some rule in F . Notice that a rule can be subsumed in a
CSS file F without occurring in F as one of the rules. For example, the rule R1.fruit, #broccoli, #tomato { color:red; font-size:large }is subsumed in our CSS file example (not so if background-color:lightblue were added toR1 ). A (rule-)merging opportunity consists of a CSS rule subsumed in the CSS file and a position in the
7

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong#apple { color:blue; font-size:small }.fruit, #broccoli { color:red; font-size:large }#orange { color:blue }#tomato { color:red; font-size:large;
background-color:lightblue }.fruit, #broccoli, #tomato { color:red; font-size:large }(a) The CSS file in Figure 4 with a rule inserted at the end.

#apple { color:blue; font-size:small }#orange { color:blue }#tomato { background-color:lightblue }.fruit, #broccoli, #tomato { color:red; font-size:large }(b) The result of trimming the CSS file in Figure 5a.
Figure 5: An example of insertion and trimming.

file to insert the rule into. An example of a merging opportunity in our CSS file example is the rule R1
and the end of the file as the insertion position. This results in a new (bigger) CSS file show in Figure 5a.
We then “trim” this resulting CSS file by eliminating “redundant” subrules. For example, the second
rule is redundant since it is completely contained in the new rule R1 . Also, notice that the subrule:#tomato { color:red; font-size:large }of the fourth rule in the original file is also completely redundant since it is contained in R1 . Removing
these, we obtain the trimmed version of the CSS file, which is shown in Figure 5b. This new CSS filecontains fewer bytes.
We may apply another round of rule-merging by inserting the rule#apple, #orange { color:blue }at the end of the second rule (and trim). The resulting file is even smaller. Computing such merging
opportunities (i.e. which yields maximum space saving) is difficult.
Two remarks are in order. Not all merging opportunities yield a smaller CSS file. For example, if#tomato is replaced by the fruit vegetable#vigna_unguiculata_subsp_sesquipedalis
the first merging opportunity above would have resulted in a larger file, which we should not apply. The
second remark is related to the issue of order dependency. Suppose we add the selector .vegetable
to the third rule in the original file, resulting in the following rule.vegetable, #orange { color:blue }Any node labeled by .fruit and .vegetable but no IDs will be assigned color:blue. However, using the first merging opportunity above yields a CSS file which assigns color:red to fruit
vegetables, i.e., not equivalent to the original file. To tackle the issue of order dependency, we need toaccount for selectors specificity and whether two selectors with the same specificity can intersect (i.e.
can be matched by a node in some DOM tree). Although for our examples the problem of selector intersection is quite obvious, this is not the case for CSS selectors in general. For example, the following
two selectors are from a real-world CSS example found on The Guardian website.
8

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong.commercial--masterclasses .lineitem:nth-child(4).commercial--soulmates:nth-child(n+3)
Interested readers unfamiliar with CSS may refer to Section 5.2 for a complete definition of selectors.
The key feature is the use of :nth-child. In the first selector it is used to only match nodes that are
the fourth child of some node. For a node to match the second selector, there must be some n ≥ 0 suchthat the node is the (n + 3)th child of some node. I.e. the third, fourth, fifth, etc. These two selectors
have a non-empty intersection, while changing n+3 to 2n+3 would yield the intersection empty!

2.3

CSS Rule-Merging Outline

The component parts of our algorithm are given in the schematic diagram in Figure 6.
From an input CSS file, the first step is to construct a formal model of the CSS that we can manipulate. This involves extracting the selector and property declaration pairs that appear in the file. Thenthe edge ordering, which records the order in which selector/declaration pairs should appear, needs tobe built. To compute the edge ordering, it is important to be able to test whether two selectors may
match the same node in some document tree. Thus, computing the edge ordering requires an algorithm
for computing whether the intersection of two selectors is empty. This process is described in detail in
Section 5 and Section 6.
Once a model has been constructed, it is possible to systematically search for semantics-preserving
rule-merging opportunities that can be applied to the file to reduce its overall size. The search is formulated as a MaxSAT problem and a MaxSAT solver is used to find the merging opportunity that represents
the largest size saving. This encoding is described in Section 7. If a merging opportunity is found, it isapplied and the search begins for another merging opportunity. If none is found, the minimised CSS fileis output.

3

Preliminaries

3.1

Maths

As usual, Z denotes the set of all integers. We use N to denote the set {0, 1, . . . , } of all natural numbers.
Let N>0 = N\{0} denote the set of all positive integers. For an integer x we define |x| to be the absolutevalue of x. For two integers i, j, we write [i, j] to denote the set {i, . . . , j}. Similar notations for open
intervals will also be used for integers (e.g. (i, j) to mean {i + 1, . . . , j − 1}). For a set S, we will writeS ∗ (resp. S + ) to denote the set of sequences (resp. non-empty sequences) of elements from S. Whenthe meaning is clear, if S is a singleton {s}, we will denote {s}∗ (resp. {s}+ ) by s∗ (resp. s+ ). Given a(finite) sequence σ = s1 , . . . , sn , i ∈ [0, n], and a new element s, we write σ[s → i] to denote the new
sequence s1 , . . . , si , s, si+1 , . . . , sn , i.e., inserting the element s right after the position i in σ.

3.2

Trees

We review a standard formal definition of (rooted) unranked ordered trees [22, 37, 47] from the databaseresearch community, which use it to model XML. We will use this in Section 5 to define document trees.
“Unranked” means that there is no restriction on the number of children of a node, while “ordered”
means that the children of each node are linearly ordered from the left-most child to the right-mostchild. An unranked ordered tree consists of a tree domain and a labelling, which we define below.
We identify a node by the unique path in the tree to the given node. A tree domain defines the set of∗nodes in the tree and is a set of sequences of natural numbers D ⊆ (N>0 ) . The empty sequence is the9

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. HongCSS File

Build CSS
Model

Find
Merging
Opp.

Apply
MergingOpp.

uses

Construct
Edge Order

uses

MaxSAT

uses

Selector
Intersection

Merging
Opp.
Exists?

yesnoMinified CSS File
Figure 6: A Schematic Diagram of Our Approachroot node. The sequence 1 would be the first child of the root node, while 2 would be the second child.
The sequence 21 would denote the first child of the second child of the root node, and so on. The tree
in Figure 2 has D = {ε, 1, 2, 11, 21, 22, 211, 212, 221, 222}.
We require that D is both prefix-closed and preceding-sibling closed. By prefix-closed we formallymean ηι ∈ D implies η ∈ D; this says that the parent of each node is also a node in the tree. By
preceding-sibling closed we formally mean ηι ∈ D implies ηι′ ∈ D for all ι′ < ι; for example, thismeans that if a node has a second child, it also has a first. Observe, we write η for a tree node (elementof D) and ι for an element of N>0 .
Our trees will also be labelled by items such as element names and attribute values. In general, aΣ-labelled tree is a pair T = (D, λ) where D is a tree domain, and λ : D → Σ is a labelling functionof the nodes of T with items from a set of labels Σ. A simple encoding of the tree in Figure 2 will havethe labelling
λ(ε)
λ(1)
λ(2)
λ(11)
λ(21)
λ(22)
λ(211)λ(212)λ(221)λ(222)
10

=
=
=
=
=
=
=
=
=
=

html
head
body
title
div id="heading"ul
img class="banner" src="header.jpg"
h1
li id="apple" class="fruit"li id="broccoli" .

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

Note, in Section 5, we will use a more complex labelling of DOM trees to fully capture all requiredfeatures.
Next we recall terminologies for relationships between nodes in trees. To avoid notational clutter,
we deliberately choose notation that resembles the syntax of CSS, which we define in Section 5. In the+≫ η ′ if η is a (strict) ancestor of η ′ , i.e., there is some η ′′ ∈ N>0
following, take η, η ′ ∈ D. We write η ⃝
′
′′
′
′
>
such that η = ηη . We write η ⃝ η if η is the parent of η , i.e., there is some ι ∈ N>0 such that+ η ′ if η is the direct preceding sibling of η ′ , i.e., there is some η ′′ and ι ∈ N>0
η ′ = ηι. We write η ⃝′′∼ η ′ if η is a preceding sibling of η ′ , i.e., there issuch that η = η (ι − 1) and η ′ = η ′′ ι. We write η ⃝
′′
′
′
′′
some η and ι, ι ∈ N>0 with ι < ι such that η = η ι and η ′ = η ′′ ι′ .

3.3

Max-SATIn this paper, we will reduce the problem of identifying an optimal merging opportunity to partial
weighted Max-SAT [3]. Partial weighted Max-SAT formulas are boolean formulas in CNF with hardconstraints (a.k.a. clauses that must be satisfied) and soft constraints (a.k.a. clauses that may be violatedwith a specified cost or weight). A minimal-cost solution is the goal. Note that our clauses will not
be given in CNF, but standard satisfiability-preserving conversions to CNF exist (e.g. see [12]) which
straightforwardly extend to partial weighted Max-SAT.
We will present Max-SAT problems in the following form (ΠH , ΠS ) where• ΠH are the hard constraints – that is, a set of boolean formulas that must be satisfied – and• ΠS are the soft constraints – that is a set of pairs (φ, ω) where φ is a boolean formula and ω ∈ N
is the weight of the constraint.
Intuitively, the weight of a soft constraint is the cost of not satisfying the constraint. The partial weighted
Max-SAT problem is to find an assignment to the boolean variables that satisfies all hard constraints andminimises the sum of the weights of unsatisfied soft constraints.

3.4

Existential Presburger Arithmetic

In this paper, we present several encodings into existential Presburger arithmetic, also known as thequantifier-free theory of integer linear arithmetic. Here, we use extended existential Presburger for∑kmulas ∃x1 , . . . , xk .φ where φ is a boolean combination of expressions i=1 ai xi ∼ b for constants
a1 , . . . , ak , b ∈ Z and ∼∈ {≤, ≥, <, >, =} with constants represented in binary. A formula is satisfiable if there is an assignment of a non-negative integer to each variable x1 , . . . , xk such that φ issatisfied. For example, a simple existential Presburger formula is shown below∃x, y, z . 0 > 2y + z − x ∧ 0 > z − ywhich is satisfied by any assignment to the variables x, y, and z such that x < 2y + z and y > z.
The assignment x = 2, y = 3, z = 0 is one such satisfying assignment. Note, when writing existential
Presburger formulas, we will allow formulas that do not strictly match the format specified above. This
is to aid readability and we will always be able to rewrite the formulas into the correct format. The
above example formula may be written∃x, y, z . x < 2y + z ∧ y < z .
It is well-known that satisfiability of existential Presburger formulas is NP-complete even with theabove extensions (cf. [55]). Such problems can be solved efficiently by SMT solvers such as Z3.
11

CSS Minification via Constraint Solving

4

M. Hague, A. W. Lin, and C.-H. Hong

Formal definition of CSS rule-merging and minification

The semantics of a CSS file can be formally modelled as a CSS-graph. A CSS-graph is a 5-tuple
G = (S, P, E, ≺, wt), where (S, P, E) is a bipartite graph (i.e. the set V of vertices is partitioned into
two sets S and P with E ⊆ S × P ), ≺ ⊆ E × E gives the order dependency on the edges, andwt : S ∪ P → Z>0 is a weight function on the set of vertices. Vertices in S are called selectors,
whereas vertices in P are called properties. For example, the CSS graph corresponding to the CSS filein Figure 4 with the selector .vegetable added to the third rule is the following bipartite graph#apple.fruit#broccoli#orange.vegetable#tomatocolor:blue
font-size:small
color:red
font-size:large
background-color:lightblue

such that the weight of a node is 1 + (length of the text), e.g., wt(#orange) = 1 + 7 = 8. The reason for the extra +1 is to account for the selector/property separators (i.e. commas or semi-colons), as
well as the character ‘{’ (resp. ‘}’) at the end of the sequence of selectors (resp. properties). Thatis, in a rule, selectors are followed by a comma if another selector follows, or ‘{’ if it is the last
selector, and properties are followed by a semi-color if another property follows, or ‘}’ if it is thelast property declaration. We refer to ≺ as the edge order and it intuitively states that one edge
should appear strictly before the other in any CSS file represented by the graph. In this case we have(.fruit, color:red) ≺ (.vegetable, color:blue) because any node labeled by .fruitand .vegetable but no IDs should be assigned the property color:blue. There are no other orderings since each node can have at most one ID3 and .fruit and .vegetable are the selectorsof the lowest specificity in the file. More details on how to compute ≺ from a CSS file are given in
Section 5.4.
A biclique in G is a complete bipartite subgraph, i.e., a pair B = (X, Y ) of a nonempty set X ⊆ S
of selectors and a nonempty set Y ⊆ P of properties such that X × Y ⊆ E (i.e. each pair of a selector
and a property in the rule is an edge). A (CSS) rule is a pair B = (B, ◁) of a biclique and a total order ◁on the set of properties. The reason for the order on the properties, but not on the selectors, is illustrated
by the following example of a CSS rule:.a, .b { color:red; color:rgba(255,0,0,0.5) }That is, nodes matching .a or .b are assigned a semi-transparent red with solid red being defined as afallback when the semi-transparent red is not supported by the document reader. Therefore, swapping
the order of the properties changes the semantics of the rule, but swapping the order of the selectors
does not. We will often denote a rule as (X, Y ) where Y = {pi }mi=1 if Y = {p1 , . . . , pm } and p1 ◁· · · ◁ pm .
A covering C of G is a sequence of rules that covers G (i.e. the union of all the edges in C equals E).
Given an edge e ∈ E, the index index(e) of e is defined to be the index of the last rule in the sequence
C that contains e. We say that C is valid if, for all two edges e = (s, p), e′ = (s′ , p′ ) in E with e ≺ e′ ,either of the following holds:
3 Strictly speaking, this is only true if we are only dealing with namespace html (which is the case almost always in web
programming and so is a reasonable assumption unless the user specifies otherwise). A node could have multiple IDs, each witha different namespace. See Section 5.

12

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

• index(e) < index(e′ )• index(e) = index(e′ ) and, if (X, {pi }mi=1 ) is the rule at position index(e) in C, it is the case thatp = pj and p′ = pk with j ≤ k.
In the example of Figure 4 with the selector .vegetable in the third rule, we can verify that it
is indeed a valid covering of itself by observing the only ordering is (.fruit, color:red) ≺(.vegetable, color:blue) and we haveindex((.fruit, color:red)) = 2

and index((.vegetable, color:blue)) = 3 .

This last-occurrence semantics reflects the cascading aspect of CSS. To relate this to the world of
CSS, the original CSS file F may be represented by a CSS-graph G, but F also turns out to be a valid
covering of G. In fact, the set of valid coverings of G correspond to CSS files that are equivalent (up toreordering of selectors and property declarations) to the original CSS file. That is, if two files cover thesame graph, then they will specify the same property declarations on any node of any given DOM.
To define the optimisation problem, we need to define the weight of a rule and the weight of acovering. To this end, we extend the function wt to rules and coverings by summing the weights of thenodes. More precisely, given a rule B = (X, Y ), define∑
wt(w).
wt(B) =w∈X∪Y

Similarly, given a covering C = {B i }m
i=1 , the weight wt(C) of C is∑m

i=1 wt(B i ). It is easy to verify
that the weight of a rule (resp. covering) corresponds to the number of non-whitespace characters in a
CSS rule (resp. file). The minification problem is, given a CSS-graph G, to compute a valid coveringwith the minimum weight.

(Optimal) Rule-Merging Problem Given a CSS-graph G and a covering C, we define the trim C↓ of
C to be the covering C ′ obtained by removing from each rule B = (X, Y ) (say at position i) in C allnodes v ∈ X ∪ Y that are not incident to at least one edge e with index(e) = i (i.e. the last occurrenceof e in C). Such nodes v may be removed since they do not affect the validity of the covering C.
We can now explain formally the file size reduction shown in Figure 5. First observe in Figure 5bthat the second rule.fruit, #broccoli { color:red; font-size:large }has been removed. Consider the node .fruit and its incident edges (.fruit, color:red) and(.fruit, font-size:large). Both of these edges have index 5 (̸= 2) since they also appear in thelast rule of Figure 5a. Thus we can remove the .fruit node from this rule. A similar argument can bemade for all nodes in this rule, which means that we remove them, leaving an empty rule (not shown).
In the fourth rule, the node color:red is incident only to (#tomato, color:red) which has index
5 (̸= 4). The situation is the same for the node font-size:large, thus both of these nodes are
removed from the rule.
The trim C↓ can be computed from C and G in polynomial time in a straightforward way. Moreprecisely, first build a hashmap for the index function. Second, go through all rules B in the covering C,
each node v in B, and each edge e incident with v checking if at least one such e satisfies index(e) = i,where B is the ith rule in C. Note that C↓ is uniquely defined given C.
We define a (rule)-merging opportunity to be a pair (B, j) of rule B and a number j ∈ (0, |C|) suchthat C[B → j] is a valid covering of G. The result of applying this merging opportunity is the covering
C[B → j]↓ obtained by trimming C[B → j]. The (rule)-merging problem can be defined as follows:
given a CSS-graph G and a valid covering C, find a merging opportunity that results in a covering withthe minimum weight. This rule-merging problem is NP-hard even in the non-weighted version [72, 52].
13

CSS Minification via Constraint Solving

5

M. Hague, A. W. Lin, and C.-H. HongCSS Selector Formalisation and its Intersection Problem

In this section, we will show how to efficiently compute a CSS-graph G = (S, P, E, ≺, wt) from a given
CSS file with the help of a fast solver of quantifier-free theory of integer linear arithmetic, e.g., Z3 [18].
The key challenge is how to extract the order dependency ≺ from a CSS file, which requires an algorithm
for the (selector-)intersection problem, i.e., to check whether two given selectors can be matched by thesame element in some document. To address this, we provide a full formalisation of CSS3 selectors [15]and a fast algorithm for the intersection problem. Since our algorithm for the intersection problem istechnically very involved, we provide a short intuitive explanation behind the algorithm in this section
and leave the details to Section 6.

5.1

Definition of Document Trees

We define the semantics of CSS3 in terms of Document Object Models (DOMs), which we also refer toas document trees. The reader may find it helpful to recall the definition of trees from Section 3.2.
A document tree consists of a number of elements, which in turn may have sub-elements as children. Each node has a type consisting of an element name (a.k.a. tag name) and a namespace. For
example, an element p in the default html namespace is a paragraph. Namespaces commonly featurein programming languages (e.g. C++) to allow the use of multiple libraries whilst minimising the risk ofoverloading names. For example, the HTML designers introduced a div element to represent a sectionof an HTML document. Independent designers of an XML representation of mathematical formulas
may represent division using elements also with the name div. Confusion is avoided by the designers
specifying a namespace in addition to the required element names. In this case, the HTML designers
would introduce the div element to the html namespace, while the mathematical div may belong toa namespace math. Hence, there is no confusion between html:div and math:div. As an aside,
note that an HTML file may contain multiple namespaces, e.g., see [30].
Moreover, nodes may also be labelled by attributes, which take string values. For example, anHTML img element has a src attribute specifying the source of the image. Finally, a node may belabelled by a number of pseudo-classes. For example :enabled means that the node is enabled andthe user may interact with it. The set of pseudo-classes is fixed by the CSS specification.
We first the formal definition before returning to the example in Section 2.1.
5.1.1

Formal Definition

In the formal definition below we permit a possibly infinite set of element, namespace, and attributenames. CSS stylesheets are not limited to HTML documents (which have a fixed set of element names,
but not attribute names since you can create custom data-* attributes), but they can also be applied
to documents of other types (e.g. XML) that permit custom element names, namespaces, and attributenames. Thus, the sets of possible names cannot be fixed to finite sets from the point of view of CSS
selectors, which may be applied to any document.
When it is known that the set of elements or attribute names is fixed (e.g. when only consideringHTML), it is possible to adapt our approach. In particular, the small model property in Proposition 6.4
may be avoided, slightly simplifying the technique.
We denote the set of pseudo-classes as{}:link, :visited, :hover, :active, :focus, :target,P =.
:enabled, :disabled, :checked, :root, :empty
Then, given a possibly infinite set of namespaces NS, a possibly infinite set of element names E LE, a
14

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongpossibly infinite set of attribute names A, and a finite alphabet4 Γ containing the special charactersand - (space and dash respectively), a document tree is a Σ-labelled tree (D, λ), where()Σ := NS × E LE × Ffin (NS × A, Γ∗ ) × 2P .
Here the notation Ffin (NS × A, Γ∗ ) denotes the set of partial functions from (NS × A) to Γ∗ whose
domain is finite. In other words, each node in a document tree is labeled by a namespace, an element,a function associating a finite number of namespace-attribute pairs with attribute values (strings), andzero or more of the pseudo-classes. For a function fA ∈ Ffin (NS × A, Γ∗ ) we say fA (s, a) = ⊥ whenfA is undefined over s ∈ NS and a ∈ A, where ⊥ ∈/ Γ∗ is a special undefined value. Furthermore, we
assume special attribute names class, id ∈ A that will be used to attach classes (see later) and IDs to
nodes.
When λ(η) = (s, e, fA , P ) we define the following projections of the labelling function
λS (η) =λE (η) =λA (η) =λP (η) =s,e,fA , andP.

We will use the following standard XML notation: for an element name e, a namespace s, and an
attribute name a, let s:e (resp. s:a) denote the pair (s, e) (resp. (s, a)). The notation helps to clarify therole of namespaces as a means of providing contextual or scoping information to an element/attribute.
There are several consistency constraints on the node labellings.
• For each s ∈ NS, there are no two nodes in the tree with the same value of s:id.
• A node cannot be labelled by both :link and :visited.
• A node cannot be labelled by both :enabled and :disabled.
• Only one node in the tree may be labelled :target.
• A node contains the label :root iff it is the root node.
• A node labelled :empty must have no children.
From now on, we will tacitly assume that document trees satisfy these consistency constraints. We write
Trees(NS, E LE, A, Γ) for the set of such trees.
5.1.2

ExampleConsider the HTML file in Figure 1. This file can be represented precisely by the tree in Figure 7. In thistree, each node is first labelled by its type, which consists of its namespace and its element name. In allcases, the namespace is the html namespace, while the element names are exactly as in the HTML file.
In addition, we label each node with the attributes and pseudo-classes with which they are labelled. The
html:html node is labelled with :root since it is the root element of the tree. The html:div nodeis labelled with the ID heading. The html:img node is labelled with the attribute class with value
banner and the attribute html:src with value banner.jpg, as well as the pseudo-class :empty
indicating that the node has no contents. The remaining nodes however are not labelled :empty sinceeven the leaf nodes contain some text (which is not represented in our tree model as it is not matchable
by a selector). Hence, a node with no child may still be non-empty.
4 See the notes at the end of the section.

15

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Honghtml:html,:root

html:body

html:head

html:title

html:div,
html:id="heading"

html:img,
html:class="banner",
html:src="header.jpg",:emptyhtml:h1

html:ul

html:li,
html:id="apple",
html:class="fruit"

html:li,
html:id="broccoli"

Figure 7: A DOM tree representation of the HTML file.

Formally, the DOM tree is (D, λ) where D = {ε, 1, 2, 11, 21, 22, 211, 212, 221, 222} and
λ(ε)
λ(1)
λ(2)
λ(11)
λ(21)
λ(22)

=
=
=
=
=
=

λ(211) =λ(212) =λ(221) =λ(222) =5.2(html, html, ∅, {:root})(html, head, ∅, ∅)(html, body, ∅, ∅)(html, title, ∅, ∅)(html, div, (html, id) 7→ heading, ∅)(html,ul, ∅, ∅)(())(html, class) 7→ banner,html, img,
, {:empty}(html, src) 7→ header.jpg(html,
h1,
∅,
∅)
(
(
) )
(html, id) 7→ apple,
html, li,,∅
(html, class) 7→ fruit(html, li, (html, id) 7→ broccoli, ∅) .

Definition of CSS3 selectors

In the following sections we define CSS selectors syntax and semantics. Informally, a CSS selector consists of node selectors σ — which match individual nodes in the tree — combined using the operators >>,>, +, and ˜. These operators express the descendant-of, child-of, neighbour-of, and sibling-of relations
respectively. Note that the blank space character is used instead of >> in CSS3, though we opt for the latter in the formalisation for the sake of readability. So, for example, we use .journal >> .science(i.e. choose all nodes with class .science that is a descendant of nodes with class .journal) instead of the standard syntax .journal .science. In addition, in order to distinguish syntax from
≫ ⃝,
> ⃝,
+ and ⃝.
∼
meaning, we use slightly different notation to their counterpart semantical operators ⃝,We remark that a comma (,) is not an operator in the CSS selector syntax. Instead a selector groupis a comma-separated list of selectors that is matched if any of its selectors is matched. A CSS rulethus consists of a selector group and a list of property declarations. For the purposes of rule-merging it
is desirable to treat selectors individually as it allows the most flexibility in reorganising the CSS file.
Hence we treat a selector group simply as a set of selectors that can be separated if needed.
A node selector σ has the form τ Θ where τ constrains the type of the node. That is, τ places
16

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongrestrictions on the element label of the node, e.g., p for paragraph elements and * (or an empty string)for all elements. The rest of the selector is a set Θ of simple selectors (written as a concatenation ofstrings representing these simple selectors) that assert atomic properties of the node. There are fourtypes of simple selectors.
Type 1: attribute selectors of the form [s|a op v] for some namespace s, attribute a, operator op ∈{=, ~=, |=, ^=, $=, *=}, and some string v ∈ Γ∗ . We may write [a op v] to mean that a node can bematched by [s|a op v] for some s. The operators =, ^=, $=, and *= take their meaning from regularexpressions. That is, equals, begins-with, ends-with, and contains respectively. The remaining operators
are more subtle. The ~= operator means the attribute is a string of space-separated values, one of whichis v. The |= operator is intended for use with language identification, e.g., as in the attribute selector[lang |= "en-GB"] to mean “English” as spoken in Great Britain. Thus |= asserts that either theattribute has value v or is a string of the form v-v ′ where - is the dash character, and v ′ is some string.
Note that if the lang attribute value of a node is en-GB, the node also matches the simple selector[lang |= "en"]. In addition, recall that class and id are two special attribute names. For this reason, CSS introduces the shorthands .v and #v for, respectively, the simple selectors [class ~= v] and[id = v], i.e., asserting that the node has a class or ID v. An example of a valid CSS selector is the selector h1.fruit.vegetable, which chooses all nodes with class fruit and vegetable, and element name h1 (which includes the following two elements: <h1 class="fruit vegetable">and <h1 class="vegetable fruit">).
Type 2. attribute selectors of the form [s|a], asserting that the attribute is merely defined on the node.
As before, we may write [a] to mean that the node may be matched by [s|a] for some namespace s.
As an example, img[alt] chooses all img elements where the attribute alt is defined.
Type 3. pseudo-class label of a node, e.g., the selector :enabled ensures the node is currently enabledin the document. There are several further kinds of pseudo-classes that assert counting constraints on
the children of a selected node. Of particular interest are selectors such as :nth-child(αn + β),which assert that the node has a particular position in the sibling order. For example, the selector:nth-child(2n + 1) means there is some n ≥ 0 such that the node is the (2n + 1)st node in thesibling order.
Type 4. negations :not(θ) of a simple selector θ with the condition that negations cannot be nested
or apply to multiple atoms. For example, :not(.fruit):not(.vegetable) is a valid selector,
whereas :not(:not(.vegetable)) and :not(.fruit.vegetable) are not a valid selectors.
5.2.1

SyntaxFix the sets NS, E LE, A, and Γ. We define S EL for the set of (CSS) selectors and NS EL for the set ofwill be used to separate syntax alternatives, while | is an item ofnode selectors. In the following
CSS syntax. The set S EL is the set of formulas φ defined as:
φ ::= σφ >> σ

φ>σ

φ+σ

φ˜σ

where σ ∈ NS EL is a node selector with syntax σ ::= τ Θ with τ having the form
τ ::= *

(s|*)

e

(s|e)

where s ∈ NS and e ∈ E LE and Θ is a (possibly empty) set of conditions θ with syntax
θ ::= θ¬:not(σ¬ )17

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongwhere θ¬ and σ¬ are conditions that do not contain negations, i.e.:σ¬θ¬::= * (s|*) e (s|e) θ¬::= [s|a] [s|a op v] [a] [a op v]:link:visited:enabled:root:hover:disabled:empty:focus:checked:target:nth-child(αn + β):nth-of-type(αn + β)op:active:nth-last-child(αn + β):nth-last-of-type(αn + β)

:only-child :only-of-type::= = ~= |= ^= $= *=where s ∈ NS, e ∈ E LE, a ∈ A, v ∈ Γ∗ , and α, β ∈ Z. Whenever Θ is the empty set, we will denotethe node selector τ Θ as τ instead of τ ∅.
5.2.2

Semantics

The semantics of a selector is defined with respect to a document tree and a node in the tree. Moreprecisely, the semantics of CSS3 selectors φ are defined inductively with respect to a document tree
T = (D, λ) and a node η ∈ D as follows. (Note: (1) p ranges over the set P of pseudo-classes, (2) vv ′is the concatenation of the strings v and v ′ , and (3) v-v ′ is the concatenation of v and v ′ with a “-” inbetween.)T, η |= φ >> σ

≫ η . (T, η ′ |= φ) and (T, η |= σ)⇔ ∃η ′ ⃝T, η |= φ > σ> η . (T, η ′ |= φ) and (T, η |= σ)⇔ ∃η ′ ⃝T, η |= φ + σ+ η . (T, η ′ |= φ) and (T, η |= σ)⇔ ∃η ′ ⃝T, η |= φ ˜ σ∼ η . (T, η ′ |= φ) and (T, η |= σ)⇔ ∃η ′ ⃝T, η |= τ Θ⇔T, η |= (s|*)

def⇔ s = λS (η)

T, η |= *⇔ ⊤T, η |= (s|e)⇔ s = λS (η) ∧ e = λE (η)

T, η |= e⇔ T, η |= (s|e) for some s ∈ NST, η |= p⇔ p ∈ λP (η)

T, η |= :not(θ¬ )⇔ ¬ (T, η |= θ¬ )T, η |= [a]⇔ T, η |= [s|a] for some s ∈ NST, η |= [a op v]⇔ T, η |= [s|a op v] for some s ∈ NST, η |= [s|a]⇔ λA (η)(s, a) ̸= ⊥T, η |= [s|a = v]

⇔ λA (η)(s, a) = v()(λA (η)(s, a) = v) ordef⇔∃v ′ . (λA (η)(s, a) = v-v ′ )T, η |= [s|a |= v]
18

def

def
def

def

def

(T, η |= τ ) and ∀θ ∈ Θ . (T, η |= θ)

def
def

def

def
def

def

def

def
def

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. HongT, η |= [s|a ^= v]⇔ ∃v ′ ∈ Γ∗ . λA (η)(s, a) = vv ′T, η |= [s|a $= v]⇔ ∃v ′ ∈ Γ∗ . λA (η)(s, a) = v ′ v

T, η |= [s|a *= v]⇔ ∃v1 , v2 ∈ Γ∗ . λA (η)(s, a) = v1 vv2

def
def
def

with the missing attribute selector being (noting v v ′ is the concatenation of v and v ′ with the spacecharacter in between)
T, η |= [a ~= v] ⇔ λA (η)(s, a) = v or ∃v ′ . (λA (η)(s, a) = v v ′ ) ordef∃v ′ . (λA (η)(s, a) = v ′ v) or ∃v1 , v2 . (λA (η)(s, a) = v1 v v2 )then, for the counting selectors
T, η |= :nth-child(αn + β)def

⇔ there is some n ∈ N such that η is the αn + βth
child

T, η |= :only-childT, η |= :nth-of-type(αn + β)def

⇔ the parent of η has precisely one childdef⇔ there is some n ∈ N such that the parent of η has
precisely αn + β − 1 children with namespace λS (η)
and element name λE (η) for some n that are (strictly)
preceding siblings of ηT, η |= :only-of-type

def⇔ the parent of η has precisely one child withnamespace λS (η) and element name λE (η)

Finally, the semantics of the remaining two selectors, which are :nth-last-child(αn + β) and:nth-last-of-type(αn + β), is exactly the same as :nth-child(αn + β) and :nth-of-type(αn + β),respectively, except with the sibling ordering reversed (i.e. the rightmost child of a parent is treated as
the first).
Remark 5.1. Readers familiar with HTML may have expected more constraints in the semantics. For
example, if a node matches :hover, then its parent should also match :hover. However, this is partof the HTML5 specification, not of CSS3. In fact, the CSS3 selectors specification explicitly states thata node matching :hover does not imply its parent must also match :hover.
5.2.3

Divergences from full CSS

Note that we diverge from the full CSS specification in a number of places. However, we do not lose
expressivity.
• We assume each element has a namespace. In particular, we do not allow elements without anamespace. There is no loss of generality here since we can simply assume a “null” namespace
is used instead. Moreover, we do not support default name spaces and assume namespaces are
explicitly given.
• We did not include :lang (l). Instead, we will assume (for convenience) that all nodes arelabelled with a language attribute with some fixed namespace s. In this case, :lang (l) is
equivalent5 to [s|lang |= l].
5 The CSS specification defines :lang (l) in this way. A restriction of the language values to standardised language codes isonly a recommendation.

19

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

• We did not include :indeterminate since it is not formally part of the CSS3 specification.
• We omit the selectors :first-child and :last-child, as well as:first-of-type and :last-of-type, since they are expressible using the other operators.
• We omitted even and odd from the nth child operators since these are easily definable as 2n and
2n + 1.
• We do not explicitly handle document fragments. These may be handled in a number of ways.
For example, by adding a phantom root element (since the root of a document fragment does notmatch :root) with a fresh ID ι and adjusting each node selector in the CSS selector to assert:not(#ι). Similarly, lists of document fragments can be modelled by adding several subtrees
to the phantom root.
• A CSS selector can be suffixed with a pseudo-element of the form ::first-line, ::first-letter,::before, and ::after. Pseudo-elements are easy to handle and only provide a distraction
to our presentation. For this reason, we relegate them into the appendix.
• We define our DOM trees to use a finite alphabet Γ. Currently the CSS3 selectors specification
uses Unicode as its alphabet for lexing. Although the CSS3 specification is not explicit about
the finiteness of characters appearing in potential DOMs, since Unicode is finite [70] (with amaximal possible codepoint) we feel it is reasonable to assume DOMs are also defined over afinite alphabet.

5.3

Solving the intersection problem

We now address the problem of checking the intersection of two CSS selectors. Let us write[[φ]] := {(T, η) : T, η |= φ}to denote the set of pairs of tree and node satisfying the selector φ. The intersection problem of CSS
selectors is to decide if [[φ]] ∩ [[φ′ ]] ̸= ∅, for two given selectors φ and φ′ . A closely related decision
problem is the non-emptiness problem of CSS selectors, which is to decide if [[φ]] ̸= ∅, for a given
selector φ. The two problems are not the same since CSS selectors are not closed under intersection(i.e. the conjunction of two CSS selectors is in general not a valid CSS selector).
Theorem 5.2 (Non-Emptiness). The non-emptiness problem for CSS selectors is efficiently reducible
to satisfiability over quantifier-free theory over integer linear arithmetic. Moreover, the problem is NPcomplete.
Theorem 5.3 (Intersection). The intersection problem for CSS selectors is efficiently reducible to satisfiability over quantifier-free theory over integer linear arithmetic. Moreover, the problem is NP-complete.
Recall from Section 3 that satisfiability over quantifier-free theory over integer linear arithmetic is in
NP and can be solved by a highly-optimised SMT solver (e.g. Z3 [18]). The NP-hardness in the above
theorems suggests that our SMT-based approach is theoretically optimal. In addition, our experimentswith real-world selectors (see Section 8) suggest that our SMT-based approach can be optimised to be
fast in practice (see Appendix D.1), with each problem instance solved within moments.
20

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. HongIdea behind our SMT-based approach We now provide the idea behind the efficient reduction toquantifier-free theory over integer linear arithmetic. Our reduction first goes via a new class of tree
automata (called CSS automata), which — like CSS selectors — are symbolic representations of setsof pairs containing a document tree and a node in the tree. We will call such sets languages recognisedby the automata. Given a CSS selector φ, we can efficiently construct a CSS automaton A that cansymbolically represent [[φ]]. Unlike CSS selectors, however, we will see that languages recognised by
CSS automata enjoy closure under intersection, which will allow us to treat the intersection problem as
the non-emptiness problem. More precisely, a CSS automaton navigates a tree structure in a similarmanner to a CSS selector: transitions may only move down the tree or to a sibling, while checking a
number of properties on the visited nodes. The difficulty of taking a direct intersection of two selectors
is that the two selectors may descend to different child nodes, and then meet again after the applicationof a number of sibling combinators, i.e., their paths may diverge and combine several times. CSS
automata overcome this difficulty by always descending to the first child, and then move from sibling
to sibling. Thus, the intersection of CSS automata can be done with a straightforward automata productconstruction, e.g., see [71].
Next, we show that the non-emptiness of CSS automata can be decided in NP by a polynomial-time
reduction to satisfiability of quantifier-free theory of integer linear arithmetic. In our experiments, weused an optimised version of the reduction, which is detailed in Appendix D.1. For non-emptiness,
ideally, we would like to show that if a CSS automaton has a non-empty language, then it accepts asmall tree (i.e. with polynomially many nodes). This is unfortunately not the case, as the reader cansee in our NP-hardness proof idea below. Therefore, we use a different strategy. First , we prove three“small model lemmas”. The first is quite straightforward and shows that, to prove non-emptiness, itsuffices to consider a witnessing automata run of length n for an automaton with n transitions (eachautomata transition allows some nodes to be skipped). Second, we show that it suffices to consider
attribute selector values (i.e. strings) of length linear in the size of the CSS automata. This is non-trivial
and uses a construction inspired by [45]. Third, we show that it suffices to consider trees whose sets ofnamespaces and element names are linear in the size of the CSS automaton. Our formula φ attempts toguess this automata run, the attribute selector values, element names, and namespaces. The global ID
constraint (i.e. all the guessed IDs are distinct) can be easily asserted in the formula. So far, boolean
variables are sufficient because the small model lemmas allow us to do bit-blasting. Where, then, do
the integer variables come into play? For each position i in the guessed path, we introduce an integer
variable ni to denote that the node at position i in the path is the ni th child. This is necessary if we wantto assert counting constraints like :nth-child(αn + β), which would be encoded in integer linear
arithmetic as ∃n : ni = αn + β.
Proof Idea of NP-hardness We now provide an intuition on how to prove NP-hardness in the above
theorems. First, observe that the intersection is computationally at least as hard as the non-emptinessproblem since we can set the second selector to be *. To prove NP-hardness of the non-emptiness,
we give a polynomial-time reduction from the NP-complete problem of non-universality of unions ofarithmetic progressions [65, Proof of Theorem 6.1]. Examples of arithmetic progressions are 2N +1 and 5N + 2, which are shorthands for the sets {1, 3, 5, . . .} and {2, 7, 12, . . .}, respectively. The
aforementioned non-universality problem allows an arbitrary number of arithmetic progressions as partof the input and we are interested in checking whether the union equals the entire set N of natural
numbers. As an example of the reduction, checking N ̸= 2N + 1 ∪ 5N + 2 is equivalent to the nonemptiness of:not(root):not(:nth-child(2n+2)):not(:nth-child(5n+3))
which can be paraphrased as checking the existence of a tree with a node that is neither the root, nor the21

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong2n + 2nd child, nor the 5n + 3rd child. Observe that we add 1 to the offset of the arithmetic progressions
since the selector :nth-child starts counting (the number of children) from 1, not from 0. A fullNP-hardness proof is available in Appendix B.2.

5.4

Extracting the edge order ≺ from a CSS file

Recall that our original goal is to compute a CSS-graph G = (S, P, E, ≺, wt) from a given CSS file.
The sets P , S, and E, and the function wt can be computed easily as explained in Section 4. We now
show how to compute ≺ using the algorithm for checking intersection of two selectors. We present an
intuitive ordering, before explaining how this may be relaxed while still preserving the semantics.
An initial definition of ≺ is simple to obtain: we want to order (s, p) ≺ (s′ , p′ ) whenever (s′ , p′ )appears later in the CSS file than (s, p), the selectors may overlap but are not distinguished by their
specificity, and p and p′ assign conflicting values to a given property name. More formally, we firstcompute the specificity of all the selectors in the CSS file. This can be easily computed in the standard
way [15]. Now, the relation ≺ can only relate two edges (s, p), (s′ , p′ ) ∈ E satisfying
1. s and s′ have the same specificity,
2. we have p ̸= p′ but the property names for p and p′ are the same (e.g. p = color:blue andp′ = color:red with property name color), and3. s intersects with s′ (i.e. [[s]] ∩ [[s′ ]] ̸= ∅).
If both (1) and (2) are satisfied, Condition (3) can be checked by means of SMT-solver via the reductionin Theorem 5.3. Supposing that Condition (3) holds, we simply compute the indices of the edges
in the file: m := index((s, p)) and m′ := index((s′ , p′ )). Recall index(e) was defined formally in
Section 4. We put (s, p) ≺ (s′ , p′ ) iff m < m′ . There are two minor technical details with the keyword!important and shorthand property names; see Appendix B.3.
The ordering given above unfortunately turns out to be too conservative. In the following, we givean example to demonstrate this, and propose a refinement to the ordering. Consider the CSS file.a { color:red; color:rgba(255,0,0,0.5) }.b { color:red; color:rgba(255,0,0,0.5) }In this file, both nodes matching .a and .b are assigned a semi-transparent red with solid red being
defined as a fallback when the semi-transparent red is not supported. If the edge order is calculated asabove, we obtain(.a, color:rgba(255,0,0,0.5)) ≺ (.b, color:red)(1)

which prevents the obvious rule-merging.a, .b { color:red; color:rgba(255,0,0,0.5) }The key observation is that the fact that we also have(.b, color:red) ≺ (.b, color:rgba(255,0,0,0.5))(2)renders any violations of (1) benign: such a violation would give precedence to the declaration color:rgba(255,0,0,0.5)
over color:red for nodes matching both .a and .b. However, because of (2) this should happen
anyway and we can omit (1) from ≺.
Formally, the ordering we need is as follows. If Conditions (1-3) hold, we compute m := index((s, p))
and m′ := index((s′ , p′ )) and put (s, p) ≺ (s′ , p′ ) iff
22

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong• m < m′ , and• (s′ , p) does not exist or index((s′ , p)) < m′ .
That is, we omit (s, p) ≺ (s′ , p′ ) if (s′ , p) appears later in the CSS file (i.e. index((s′ , p′ )) < index((s′ , p))).
Note, we are guaranteed in this latter case to include (s′ , p′ ) ≺ (s′ , p) since (s′ , p′ ) and (s′ , p) can easily
be seen to satisfy the conditions for introducing (s′ , p′ ) ≺ (s′ , p).

6More Details on Solving Selector Intersection Problem

In the previous section, we have given the intuition behind the efficient reduction from the CSS selector
intersection problem to quantifier-free theory over integer linear arithmetic, for which there is a highlyoptimised SMT-solver [18]. In this section, we present this reduction in full, which may be skipped ona first reading without affecting the flow of the paper.
This section is structured as follows. We begin by defining CSS automata. We then provide asemantic-preserving transformation from CSS selectors to CSS automata. Next we show the closureof CSS automata under intersection. The closure allows us to reduce the intersection problem of CSS
automata to the non-emptiness problem of CSS automata. Finally, we provide a reduction from nonemptiness of CSS automata to satisfiability over quantifier-free integer linear arithmetic. We will see thateach such transformation/reduction runs in polynomial-time, resulting in the complexity upper boundof NP, which is precise due to the NP-hardness of the problem from the previous section.

6.1

CSS Automata

CSS automata are a kind of finite automata which navigate the tree structure of a document tree. Transitions of the automata will contain one of four labels: ↓, →, →+ , and ◦. Intuitively, these transitions
perform the following operations. ↓ moves to the first child of the current node. → moves to the next
sibling of the current node. →+ moves an arbitrary number of siblings to the right. Finally, ◦ reads
the node matched by the automaton. Since CSS does not have loops, we require only self loops in our
automata, which are used to skip over nodes (e.g. .v ˜ .v ′ may pass over many nodes between thosematching .v and those matching .v ′ ). We do not allow → to label a loop – this is for the purposes of
the NP proof: it can be more usefully represented as →+ .
An astute reader may complain that →+ does not need to appear on a loop since it can already passover an arbitrary number of nodes. However, the product construction used for intersection becomeseasier if →+ appears only on loops. There is no analogue of →+ for ↓ because we do not need it:
the use of →+ is motivated by selectors such as :nth-child(αn + β) which count the number ofsiblings of a node. No CSS selector counts the number of descendants/ancestors.
()
Formal Definition of CSS Automata A CSS Automaton A is a tuple Q, ∆, q in , qf where Q is a
finite set of states, ∆ ⊆ Q × {↓, →, →+ , ◦} × NS EL × Q is a transition relation, q in ∈ Q is the initialstate, and qf ∈ Q is the final state. Moreover,
1. (only self-loops) there exists a partial order ≲ such that (q, d, σ, q ′ ) ∈ ∆ implies q ′ ≲ q,
2. (→+ loops and doesn’t check nodes) for all (q, →+ , σ, q ′ ) ∈ ∆ we have q = q ′ and σ = *,3. (→ doesn’t label loops) for all (q, d, σ, q) ∈ ∆ we have d ̸=→ and σ = *,4. (◦ checks last node only) for all (q, d, σ, q ′ ) ∈ ∆ we have q ′ = qf iff d = ◦, and23

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

5. (qf is a sink) for all (q, d, σ, q ′ ) ∈ ∆ we have q ̸= qf .
We now define the semantics of CSS automata, i.e., given an automaton A, which language L(A)they recognise. Intuitively, the set L(A) contains the set of pairs of document tree and node, whichdthe automaton A accepts. We will now define this more formally. Write q −→ q ′ to denote a transition
σ(q, d, σ, q ′ ) ∈ ∆. A document tree T = (D, λ) and node η ∈ D is accepted by a CSS automaton A if
there exists a sequence∗q0 , η0 , q1 , η1 , . . . , qℓ , ηℓ , qℓ+1 ∈ (Q × D) × {qf }such that q0 = q in is the initial state, η0 = ε is the root node, qℓ+1 = qf is the final state, ηℓ = η is thedmatched node, and for all i, there is some transition qi −→ qi+1 with ηi satisfying σ and if i ≤ ℓ,σ

1. if d =↓ then ηi+1 = ηi 1 (i.e., the leftmost child of ηi ),2. if d =→ then there is some η ′ and ι such that ηi = η ′ ι and ηi+1 = η ′ (ι + 1), and
3. if d =→+ then there is some η ′ , ι and ι′ such that ηi = η ′ ι and ηi+1 = η ′ ι′ and ι′ > ι.
Such a sequence is called an accepting run of length ℓ. The language L(A) recognised by A is the setof pairs (T, η) accepted by A.

6.2

Transforming CSS Selectors to CSS Automata

The following proposition shows that CSS automata are no less expressive than CSS selectors.
Proposition 6.1. For each CSS selector φ, we may construct in polynomial-time a CSS automaton Aφsuch that L(Aφ ) = [[φ]].
We show this proposition by giving a translation from a given CSS selector to a CSS automaton.
Before the formal definition, we consider the a simple example. A more complex example is shown
after the translation.
6.2.1

Simple Example

Consider the selector
p + .awhich selects a node that has a class a and is directly a right neighbour of a node with element p.
Figure 8 gives a CSS automaton representing the selector. The automaton begins with a loop that cannavigate down any branch of the tree using the ↓ and →+ transitions from ◦1 . Then, since it always
moves from the first child to the last, it will first see the node with the p. When reading this node, it will
move to the next child using → before matching the node with class a, leading to the accepting state.
6.2.2

Formal Translation

Given a CSS selector φ, we define Aφ as follows. We can write φ uniquely in the form
σ1 o1 σ2 o2 · · · on−1 σnwhere each σi is a node selector, and each oi ∈ {>>, >, +, ˜}. We will have a state ◦i corresponding toeach σi , oi . We defineAφ = (Q, E LE, ∆, ◦1 , qf )24

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

→

◦1

p

◦2

◦

qf

.a

→+ , ↓*

Figure 8: CSS Automaton for p + .a.

↓
◦i

σi

↓
σi

↓

•i
→+

→

◦i+1 ,

◦i

*

↓
σi

σi
•i

→, ↓

◦i+1 ,*→+ , ↓**(a) oi = >(b) oi = >>

→
→

◦i

σi

◦i+1 ,

◦i

→
σi

σi
•i
→+

→

◦i+1

*

*
(c) oi = +(d) oi = ˜Figure 9: Converting selectors to CSS automata.

where Q = {◦i , •i | 1 ≤ i ≤ n} ⊎ {qf } and we define the transition relation ∆ to contain the following
transitions. The initial and final transitions are used to navigate from the root of the tree to the nodematched by σ1 , and to read the final node matched by σn (and the selector as a whole) respectively.
↓,→+

◦

*

σn

That is, ◦1 −−−→ ◦1 and ◦n −−→ qf . We have further transitions for 1 ≤ i < n that are shownin Figure 9. The transitions connect ◦i to ◦i+1 depending on oi . Figure 9a shows the child operator.
The automaton moves to the first child of the current node and moves to the right zero or more steps.
Figure 9b shows the descendant operator. The automaton traverses the tree downward and rightward any
number of steps. The neighbour operator is handled in Figure 9c by simply moving to the next sibling.
Finally, the sibling operator is shown in Figure 9d.
We prove the correctness of this construction in Lemma C.1 (soundness) and Lemma C.2 (completeness) in Appendix C.1.
6.2.3

Complex Example

Figure 10 gives an example of a CSS automaton representing the more complex selector
div >> p ˜ .bwhich selects a node that has class b, is a right sibling of a node with element p and moreover is a
descendent of a div node. This automaton again begins at ◦1 and navigates until it finds the node withthe div element name. The automaton can read this node in two ways. The topmost transition covers
25

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

↓
◦1

↓

→

div

→, ↓

•1

p
◦2

*

div
→+ , ↓→+ , ↓

*

*

→
p

•2
→+

→
*

◦3

◦

qf

.b

*
Figure 10: CSS Automaton for div >> p ˜ .b

the case where the p node is directly below the div node. The lower transition allows the automaton tomatch the p node and then use a loop to navigate to the descendent node that will match p. Similarly,
from ◦2 the automaton can read a p node and choose between immediately matching the node with classb or navigating across several siblings (using the loop at state •2 ) before matching .b and accepting.

6.3

Closure Under Intersection

The problems of non-emptiness and intersection of CSS automata can be defined in precisely the same
way we defined them for CSS selectors. One key property of CSS automata, which is not enjoyed by
CSS selectors, is the closure of their languages under intersection. This allows us to treat the problem ofintersection of CSS automata (i.e. the non-emptiness of the intersection of two CSS automata languages)
as the non-emptiness problem (i.e. whether a given CSS automaton has an empty language).

Proposition 6.2. Given two CSS automata A1 and A2 , we may construct in polynomial-time an automaton A1 ∩ A2 such that L(A1 ) ∩ L(A2 ) = L(A1 ∩ A2 ).

The construction of the CSS automaton A1 ∩ A2 is by a variant of the standard product construction[71] for finite-state automata over finite words, which run the two given automata in parallel synchronised by the input word. Our construction runs the two CSS automata A1 and A2 in parallel synchronised by the path that they traverse. We first proceed with the formal definition and give an example
afterwards.

6.3.1

Formal Definition of Intersection

We first define the intersection of two node selectors. Recall node selectors are of the form τ Θ whereτ ∈ {*, (s|*), e, (s|e) | s ∈ NS ∧ e ∈ E LE}. The intersection of two node selectors τ1 Θ1 and τ2 Θ2should enforce all properties defined in Θ1 and Θ2 . In addition, both selectors should be able to agree
on the namespace and element name of the node, hence this part of the selector needs to be combined
26

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongmore carefully. Thus, letting Θ = Θ1 ∪ Θ2 . we defineτ2 Θ
τ1 = *





τ1 Θ
τ2 = *


(
)



τ
=
(s|
)
∨

2
*

τ2 Θ
τ1 = (s|*) ∧τ2 = (s|e)
(s|e)Θ

τ1 = (s|*) ∧ τ2 = eτ1 Θ1 ∩ τ2 Θ2 =
τ2 = (s|e) ∨





τ1 = (s|e) ∧ 
τ2 = e ∨


τ1 Θ



τ2 = (s|*)




τ2 Θ
τ
=
e
∧
(τ
=
(s|e)
∨ τ2 = e)

1
2




(s|e)Θ
τ1 = e ∧ τ2 = (s|*)
:not(*) otherwise.
We now define the automaton A1 ∩ A2 . The intersection automaton synchronises transitions thatmove in the same direction (by ↓, →, →+ ) or both agree to match the current node at the same time(with ◦). In addition, we observe that a →+ can be used by one automaton while the other uses →.
Given
(
)
(
)
A1 = Q1 , E LE, ∆1 , q1in , qf1
and A2 = Q2 , E LE, ∆2 , q2in , qf2
we define

(
(
) (
))
A1 ∩ A2 = Q1 × Q2 , E LE, ∆, q1in , q2in , qf1 , qf2

where (letting d range over {→, →+ , ↓, ◦}) we set ∆ =
{
}
d
d
d
′
′
′
′
(q1 , q2 ) −−−−→ (q1 , q2 ) q1 −→ q1 ∧ q2 −→ q2 ∪σ1 ∩σ2
σ1
σ2
{
}
→
→
→
+
′
′
(q1 , q2 ) −→ (q1 , q2 ) q1 −→ q1 ∧ q2 −−→ q2 ∪
σ1
σ1
*
}
{
→+
→
→
′
′
(q1 , q2 ) −→ (q1 , q2 ) q1 −−→ q1 ∧ q2 −→ q2 .
σ2

*

σ2

We verify that this transition relation satisfies the appropriate conditions:
1. (only self-loops) for a contradiction, a loop in ∆ that is not a self-loop can be projected to a loop
d

d′

σ

σ

of A1 or A2 that is also not a self-loop, e.g. if there exists (q1 , q2 ) −→ (q1′ , q2′ ) −→(q1 , q2 ) that is′

not a self-loop, then either q1 ̸= q1′ or q2 ̸= q2′ , and thus we have a loop from q1 to q1′ to q1 in A1
or similarly for A2 ,2. (→+ loops and doesn’t check nodes) →+ transitions are built from →+ transitions in A1 and A2 ,thus a violation in the intersection implies a violation in one of the underlying automata,
3. (→ doesn’t label loops) → transitions are built from at least one → transition in A1 or A2 , thus aviolation in the intersection implies a violation in one of the underlying automata,4. (◦ checks last node only) similarly, a violation of this constraint in the intersection implies aviolation in one of the underlying automata,5. (qf is a sink) again, a violation of this constraint in the intersection implies a violation in theunderlying automata.
27

CSS Minification via Constraint Solving→+ , ↓*(◦1 , ◦1 )

↓

↓

→

div

p

→+ , ↓→+**(◦1 , •1 )

div

p

→

M. Hague, A. W. Lin, and C.-H. Hong

p

→, ↓
*

→
p

(◦2 , ◦1 )(◦2 , •1 )→(◦1 , ◦2 )→(◦2 , ◦2 )

p

p

→

(◦1 , •2 )

→

p

p

(◦2 , •2 )(◦2 , ◦3 )◦(qf , qf )

.a.b
→
→

p

(◦1 , ◦3 )(◦2 , •2 )Figure 11: The intersection of the automaton in Figure 8 (in the first component) and the automaton in Figure 10(in the second component).

6.3.2

Example of Intersection

Recall the automaton in Figure 8 (equivalent to p + .a) and the automaton in Figure 10 (equivalent to
div >> p ˜ .b). The intersection of the two automata is given in Figure 11. Each state is a tuple (q1 , q2 )where the first component q1 represents the state of the automaton equivalent to p + .a and the second
component q2 the automaton equivalent to div >> p ˜ .b.
In this example, accepting runs of the automaton will use only the top row of states. The lower
states are reached when the two automata move out of sync and can no longer reach agreement on the
final node matched. Usually this is by the first automaton matching a node labelled p, after which it
must immediately accept the neighbouring node. This leaves the second automaton unable find a match.
Hence, the first automaton needs to stay in state ◦1 until the second has reached a near-final state. Note,the two automata need not match the same node with element name p.

6.4

Reducing Non-emptiness of CSS Automata to SMT-solving

We will now provide a polynomial-time reduction from the non-emptiness of a CSS automaton to satisfiability of quantifier-free theory over integer linear arithmetic. That is, given a CSS automaton A, ouralgorithm constructs a quantifier-free formula θA over integer linear arithmetic such that A recognises a
non-empty language iff θA is satisfiable. The encoding is quite involved and requires three small model
properties discussed earlier. Once we have these properties we can construct the required formula ofthe quantifier-free theory over linear arithmetic. We begin by discussing each of these properties inturn, and then provide the reduction. The reduction is presented in a number of stages. We show how
to handle attribute selectors separately before handling the encoding of CSS automata. The encodingof CSS automata is further broken down: we first describe the variables used in the encoding, then we
28

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongdescribe how to handle node selectors, finally we put it all together to encode
runs of) a CSS automaton.
(
For the remainder of the section, we fix a CSS automaton A = Q, ∆, q in , qf and show how toconstruct the formula θA in polynomial-time.
6.4.1

Bounded Run Length

The first property required is that the length of runs can be bounded. That is, if the language of A is not
empty, there is an accepting run over some tree whose length is smaller than the derived bound. We will
construct a formula that will capture all runs of length up to this bound. Thanks to the bound we knowthat if an accepting run exists, the formula will encode at least one, and hence be satisfiable.
)(
Proposition 6.3 (Bounded Runs). Given a CSS Automaton A = Q, ∆, q in , qf , if L(A) ̸= ∅, there
exists (T, η) ∈ L(A) with an accepting run of length |∆|.
This proposition is straightforward to obtain. We exploit that any loop in the automaton is a self loopthat only needs to be taken at most once. For loops labelled ↓, a CSS formula cannot track the depth
in the tree, so repeated uses of the loop will only introduce redundant nodes. For loops labelled →+ ,selectors such as :nth-child(αn + β) may enforce the existence of a number of intermediate
nodes. But, since →+ can cross several nodes, such loops also only needs to be taken once. Hence,each transition only needs to appear once in an accepting run. That is, if there is an accepting run of a
CSS automaton with n transitions, there is also an accepting run of length at most n.
6.4.2

Bounding Namespaces and Elements

It will also be necessary for us to argue that the number of namespaces and elements can be boundedlinearly in the size of the automaton. This is because our formula will need keep track of the number ofnodes of each type appearing in the tree. This is required for encoding, e.g., the pseudo-classes of theform :nth-of-type(αn + β). By bounding the number of types, our formula can use a bounded
number of variables to store this information.
We state the property below. The proof is straightforward and appears in Appendix C.3.1. Intuitively,
since only a finite number of nodes can be directly inspected by a CSS automaton, all others can berelabelled to a dummy type unless their type matches one of the inspected nodes.
()
Proposition 6.4 (Bounded Types). Given a CSS Automaton A = Q, ∆, q in , qf if there exists (T, η) ∈L(A) with T = (D, λ), then there exists some (T ′ , η) ∈ L(A) where T ′ = (D, λ′ ). Moreover, let⇃(E LE) be the set of element names and ⇃(NS) be the set of namespaces appearing in the image of λ′ .
Both the size of ⇃(E LE) and the size of ⇃(NS) are bounded linearly in the size of A.
6.4.3

Bounding Attribute Values

We will need to encode the satisfiability of conjunctions of attribute selectors. This is another potential
source of unboundedness because the values are strings of arbitrary length. We show that, in fact, if thelanguage of the automaton is not empty, there there is a solution whose attribute values are strings of alength less than a bound polynomial in the size of the automaton.
The proof of the following lemma is highly non-trivial and uses techniques inspired by results in
Linear Temporal Logic and automata theory. To preserve the flow of the article, we present the proof in
Appendix C.3.2.
()
Proposition 6.5 (Bounded Attributes). Given a CSS Automaton A = Q, ∆, q in , qf if there exists(T, η) ∈ L(A) with T = (D, λ), then there exists some bound N polynomial in the size of A and some(T ′ , η) ∈ L(A) where the length of all attribute values in T ′ is bound by N .
29

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

Given such a bound on the length of values, we can use quantifier-free Presburger formulas to“guess” these witnessing strings by using a variable for each character position in the string. Then, theletter in each position is encoded by a number. This process is discussed in the next section.
6.4.4

Encoding Attribute Selectors

Before discussing the full encoding, we first show how our formula can encode attribute selectors. Once
we have this encoding, we can invoke it as a sub-routine of our main encoding whenever we have tohandle attribute selectors. It is useful for readability reasons to present this in its own section.
The first key observation is that we can assume each positive attribute selector that does not specify
a namespace applies to a unique, fresh, namespace. Thus, these selectors do not interact with any otherpositive attribute selectors and we can handle them easily. Note, these fresh namespaces do not appearin ⇃(NS).
We present our encoding which works by identifying combinations of attribute selectors that must
apply to the same attribute value. That is, we discover how many attribute values are needed, and collect
together all selectors that apply to each selector. To that end, let op range over the set {=, ~=, |=, ^=, $=, *=}and let τ Θ be a node selector. For each s and a, let Θsa be the set of conditions in Θ of the form θ or:not(θ) where θ is of the form [s|a] or [s|a op v]. Recall we are encoding runs of a CSS automaton of length at most n. For a given position i in the run, we define AttsPres(τ Θ, i) to be theconjunction of the following constraints, where the encoding for AttsPress:a (Θ, i) is presented below.
Since a constraint of the form :not([a op v]) applies to all attributes a regardless of their namespace,
we define for convenience Neg(s, a) = {:not([s|a op v]) | :not([a op v]) ∈ Θ}.
• For each s and a with Θsa non-empty and containing at least one selector of the form [s|a] or[s|a op v], we enforce
AttsPress:a (Θsa ∪ Neg(s, a), i)
if :not([a]) ∈/ Θ and :not([s|a]) ∈/ Θ, else we assert false.
• For each [a] ∈ Θ, let s be fresh namespace. We assert
AttsPress:a ({[s|a]} ∪ Neg(s, a), i)and for each [a op v] ∈ Θ we assert
AttsPress:a ({[s|a op v]} ∪ Neg(s, a), i)
whenever, in both cases, :not([a]) ∈/ Θ. If :not([a]) ∈ Θ in both cases we assert false.
It remains to encode AttsPress:a (C, i) for some set of attribute selectors C all applying to s and a.
We can obtain a polynomially-sized global bound (N − 1) on the length of any satisfying value ofan attribute s:a at some position i of the run from Proposition 6.5 (Bounded Attributes)6 . Finally, we
increment the bound by one to allow space for a trailing null character.
s:aOnce we have a bound on the length of a satisfying value, we can introduce variables xs:ai,1 , . . . , xi,Nfor each character position of the satisfying value, and encode the constraints almost directly. That is,letting θ range over positive attribute selectors, we define7∧
AttsPress:a (C, i) =AttsPres(θ, ⃗x) ∧θ∈C ∧¬AttsPres(θ, ⃗x) ∧ Nulls(⃗x) .
:not(θ)∈C
6 Of course, we could obtain individual bounds for each s and a if we wanted to streamline the encoding.
7 Note, we allow negation in this formula. This is for convenience only as the formulas we negate can easily be transformed
into existential Presburger.

30

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongs:awhere ⃗x = xs:ai,1 , . . . , xi,N will be existentially quantified later in the encoding and whose values will
8
range over Γ ⊎ {0} where 0 is a null character used to pad the suffix of each word. We define
AttsPres(θ, ⃗x) for several θ, the rest can be defined in the same way (see Appendix C.3.3). Letting
v = a1 . . . am ,AttsPres([s|a], ⃗x)
AttsPres([s|a = v], ⃗x)==

AttsPres([s|a ^= v], ⃗x) =AttsPres([s|a *= v], ⃗x)

=

⊤∧
1≤i≤m
∧

s:a
s:a
xi,j
= aj ∧ xi,m+1
=0
s:a
xi,j
= aj
∧

1≤j≤m
∨

0≤j≤N −m−1 1≤j ′ ≤m

Finally, we enforce correct use of the null character∨
Nulls(⃗x) =∧xs:ai,j+j ′ = aj

s:a
xi,j
′ = 0 .

1≤j≤N j≤j ′ ≤N

6.4.5

Encoding Non-EmptinessWe are now ready to give the main encoding of the emptiness of a CSS automaton using the quantifierfree theory over integer linear arithmetic. This encoding makes use of a number of variables, which
we explain intuitively below. After describing the variables, we give the encoding in two parts: first we
explain how a single node selector can be translated into existential Presuburger arithmetic. Once wehave this translation, we give the final step of encoding a complete run of an automaton.
Variables Used in the Encoding Our encoding makes use of the following variables for 0 ≤ i ≤ n,
representing the node at the ith step of the run. We use the overline notation to indicate variables.
• q i , taking any value in Q, indicating the state of the automaton when reading the ith node in therun,• si , taking any value in ⇃(NS) indicating the element tag (with namespace) of the ith node read in
the run,• ei , taking any value in ⇃(E LE) indicating the element tag (with namespace) of the ith node readin the run,
• pi , for each pseudo-class p ∈ P \ {:root} indicating that the ith node has the pseudo-class p,• ni , taking a natural number indicating that the ith node is the ni th child of its parent, and• ns:ei , for all s ∈ ⇃(NS) and e ∈ ⇃(E LE ), taking a natural number variable indicating that there arens:e
i nodes of type s:e strictly preceding the current node in the sibling order, and• N i , taking a natural number indicating that the current node is the N i th to last child of its parent,ands:e• N i , for all s ∈ ⇃(NS) and e ∈ ⇃(E LE), taking a natural number variable indicating that there ares:eN i nodes of type s:e strictly following the current node in the sibling order, and
8 Strictly speaking, Presburger variables range over natural numbers. It is straightforward to range over a finite number ofvalues. That is, we can assume, w.l.o.g. that Γ ⊎ 0 ⊆ N and the quantification is suitably restricted.

31

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

• xs:ai,j as used in the previous section for encoding the character at the jth character position of theattribute value for s:a at position i in the run9 .
Note, we do not need a variable for :root since it necessarily holds uniquely at the 0th position of therun.
Encoding Node Selectors We define the encoding of node selectors below using the variables definedin the previous section. Note, this translation is not correct in isolation: global constraints such as “noID appears twice in the tree” will be enforced later. The encoding works by translating each part of theselector directly. For example, the constraint e simply checks that ei = e. Even in the more complex
cases of selectors such as :nth-child(αn + β) we are able to use a rather direct translation of
the semantics: ∃n.x = αn + β. For the case of :nth-of-type(αn + β) we have to consider all
possible namespaces s and element names e that the node could take, and use the nis:e variables to do
the required counting.
In our presentation we allow ourselves to negate existentially quantified formulas of the form ∃n.x =αn+β where x is a variable, and α and β are constants. Although this is not strictly allowed in existential
Presburger arithmetic, it is not difficult to encode correctly. For completeness, we provide the encodingof such negated formulas in Appendix C.3.4.
In the following, let NoAtts(Θ) be Θ less all selectors of the form [s|a], [s|a op v], [a], or[a op v], or :not([s|a]), :not([s|a op v]), :not([a]), or :not([a op v]).
Definition 6.6 (Pres(σ, i)). Given a node selector τ Θ, we define
Pres(τ, i)∧
(
)


∧


Pres(θ, i) ∧ 
Pres(τ Θ, i) =  θ∈NoAtts(Θ)
AttsPres(τ Θ, i)
where we define Pres(θ, i) as follows:
Pres(*, i) = ⊤Pres((s|*), i) = (si = s)
Pres(e, i) = (ei = e)
Pres((s|e), i) = (si = s ∧ ei = e)
Pres(:not(σ¬ ), i) = ¬Pres(σ¬ , i){⊤ i=0
Pres(:root, i) =⊥ otherwise∀p ∈ P \ {:root} . Pres(p, i) = piand, finally, for the remaining selectors, we havePres(:nth-child(αn + β), 0) =Pres(:nth-last-child(αn + β), 0) =Pres(:nth-of-type(αn + β), 0) =Pres(:nth-last-of-type(αn + β), 0) =Pres(:only-child, 0) =Pres(:only-of-type, 0) =9 Recall s is not necessarily in ⇃(NS) as it may be some fresh value.

32

⊥
⊥
⊥
⊥
⊥
⊥

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongand when i > 0
Pres(:nth-child(αn + β), i) =Pres(:nth-last-child(αn + β), i) =Pres(:nth-of-type(αn + β), i)=∃n.ni = αn + β∃n.N i =(αn + β)∨
si = s ∧ ei = e ∧∃n.nis:e + 1 = αn + βs∈⇃(NS)e∈⇃(E LE)

Pres(:nth-last-of-type(αn + β), i)∨=s∈⇃(NS)e∈⇃(E LE)

Pres(:only-child, i)=

Pres(:only-of-type, i)=(

si = s ∧ ei = e ∧s:e∃n.N i + 1 = αn + β)

ni = 1 ∧(N i = 1)∨
si = s ∧ ei = e ∧s:enis:e = 0 ∧ N i = 0s∈⇃(NS)e∈⇃(E LE)We are now ready to move on to complete the encoding.
Encoding Runs of CSS Automata Finally, now that we are able to encode attribute and node selectors, we can make use of these to encode accepting runs of a CSS automaton. Since we know that, if
there is an accepting run, then there is a run of length at most n where n is the number of transitions in∆, we encode the possibility of an accepting run using the variables discussed above for all 0 ≤ i ≤ n.
The shape of the translation is given below and elaborated on afterwards.
Definition 6.7. θA Given a CSS automaton A we define






q 0 = q inTran(i)∧∧ ∧ Consistent∧∨θA = 
q n = qf
q i = qf0≤i<nwhere Tran(i) and Consistent are defined below.
Intuitively, the first two conjuncts asserts that a final state is reached from an initial state. Next, we
use Tran(i) to encode a single step of the transition relation, or allows the run to finish early. Finally
Consistent asserts consistency constraints.
∨
We define as a disjunction over all possible (single-step) transitions Tran(i) =Tran(i, t) wheret∈∆Tran(i, t) is defined below by cases. There are four cases depending on whether the transition is labelled↓, →, →+ , or ◦. In most cases, we simply assert that the state changes as required by the transition, andthat the variables ni and ns:ei are updated consistently with the number of nodes read by the transition.
Although the encodings look complex, they are essentially simple bookkeeping.
To ease presentation, we write si :ei = s:e as shorthand for (si = s ∧ ei = e) and si :ei ̸= s:e as
shorthand for (si ̸= s ∨ ei ̸= e).
↓

1. When t = q −→ q ′ we define Tran(i, t) to beσ()(q i = q) ∧ q i+1 = q ′ ∧∧i) ∧¬:empty)( s:e i ∧ Pres(σ,(ni+1 = 1) ∧ni+1 = 0 .
s∈⇃(NS)e∈⇃(E LE)33

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong→

2. When t = q −→ q ′ we define Tran(i, t) to be false when i = 0 (since the root has no siblings)σand otherwise()′(q i = q) ∧ q i+1 =( q ∧ Pres(σ, i))∧
= N i − 1 ))∧( = ni + 1) ∧ N( i+1
 (ni+1s:e(s(i :ei = s:e) ⇒ n(i+1= nis:e +))
1 ∧
s:e


(si :ei ̸= s:e) ⇒( ns:e
∧ ))i+1 = ni

(
∧ 
s:e
s:e


∧  .
 (si+1 :ei+1 = s:e) ⇒ N i+1 = N i − 1s∈⇃(NS) 

(
( s:e
))
s:e
e∈⇃(E LE)
(si+1 :ei+1 ̸= s:e) ⇒ N i+1 = N i→+

3. When t = q −−→ q we define Tran(i, t) to be false when i = 0 and otherwise*()(q i = q) ∧) q i+1( =q ∧))∃δ. n
= ni + δ ∧ N i+1 = N i − δ )∧i+1 (
(si(:ei = s:e) ⇒
)
∧ 
s:e
s:e



( ni+1 = ni + δ s:e + 1 )(si(:ei ̸= s:e) ⇒


)
∧
s:e
s:e


=
+
n
n
δ
s:e
i+1
i
 (

)
∧

 .
∃δ s:e . (si+1:ei+1 = s:e) ⇒

)
(
s:e
s:e
s∈⇃(NS)∧ N i+1 = N i − δ s:e − 1e∈⇃(E LE)


(
)


(s
:e
=
̸
s:e)
⇒
i+1
i+1


( s:e
)
s:e
N i+1 = N i − δ s:e((◦

4. When t = q −→ q ′ we define Tran(i, t) to beσ()(q i = q) ∧ q i+1 = q ′ ∧ Pres(σ, i) .
To ensure that the run is over a consistent tree, we assert the consistency constraint
Consistent = Consistentn ∧ Consistenti ∧ Consistentp
where each conjunct is defined below.
s:e• The clause Consistentn asserts that the values of ni , N i , nis:e , and N i
∧
1≤i≤n

(
ni = 1 +

∑

)
ns:e
i

s:e∈E LE(∧∑Ni = 1 +are consistent. That is
)

s:e
Ni

.

s:e∈E LE• The clause Consistenti asserts that ID values are unique. It is the conjunction of the following
s:idclauses. For each s for which we have created variables of the form xi,j
we assert∧∨1≤i̸=i′ ≤n 1≤j≤N

34

s:id
xs:id
i,j ̸= xi′ ,j .

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

• Finally, Consistentp asserts the remaining consistency constraints on the pseudo-classes. We
define Consistentp =()
¬( :linki ∧ :visitedi ∧ ) )
(
∧
∧ 
∧ 
 0≤j̸=i≤n ¬ :targeti ∧ :targetj
 .
(
)
0≤i≤n
¬ :enabledi ∧ :disabledi
These conditions assert the mutual exclusivity of :link and :visited, that at most one nodein the document can be the target node, that nodes are not both enabled and disabled.
6.4.6

Correctness of the Encoding

We have now completed the definition of the reduction from the emptiness problem of CSS automata
to the satisfiability of existential Presburger arithmetic. What remains is to show that this reduction isfaithful: that is, the CSS automaton has an empty language if and only if the formula is satisfiable. The
proof is quite routine, and presented in Lemma C.8 and Lemma C.9 in Appendix C.3.5.
Lemma 6.8 (Correctness of θA ). For a CSS automaton A, we have
L(A) ̸= ∅ ⇔ θA is satisfiable.
We are thus able to decide the emptiness problem, and therefore the emptiness of intersection problem, for CSS automata by reducing the problem to satisfiability of existential Presburger arithmetic andusing a fast solver such as Z3 [18] to resolve the satisfiability.

7

Rule-Merging to Max-SAT

In this section, we provide a reduction from the rule-merging problem to partial weighted MaxSAT. The
input will be a valid covering C = {B i }m
i=1 of a CSS graph G. We aim to find a rule B = (X, Y ) and aposition j that minimises the weight of C[B → j]↓ .
There is a fairly straightforward encoding of the rule-merging problem into Max-SAT using for eachnode w ∈ S∪P a boolean variable w which is true iff the node is included in the new rule. Unfortunately,
early experiments showed that such an encoding does not perform well in practice, causing prohibitively
long run times even on small examples. The failure of the naive encoding may be due to the search spacethat includes a large number of possible pairs (X, Y ) that turn out to be invalid rules (e.g. include edges
not in the CSS-graph G). Hence, we will use a different Max-SAT encoding that, by means of syntax,
further restricts the search space of valid rule-merging opportunities.
The crux of our new encoding is to explicitly say in the Max-SAT formula φ that the rule B in a
merging opportunity (B, j) is a “valid” sub-biclique of one of the maximal bicliques B = (X, Y ) —maximal with respect to subset-of relations of X and Y components of bicliques — in the CSS-graph
G. By insisting B is contained within a maximal biclique of the CSS-graph, we automatically ensurethat B does not contain edges that are not in G.
The formula φ will try to guess a maximal biclique B and which nodes to omit from B. Since thenumber of maximal bicliques in a bipartite graph is exponential (in the number of nodes) in the worst
case, one concern with this idea is that the constraint φ might become prohibitively large. As we shallsee, this turns out not to be the case in practice. Intuitively, based on our experience, the number of rules
in a real-world CSS file is at most a few thousand. Second, the number of maximal bicliques in a CSSgraph that corresponds to a real-world CSS file also is typically of a similar size to the number of rules,
and, furthermore, can be enumerated using the algorithm from [36] (which runs in time polynomial in
35

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong.a { color:blue; color:green }.b { color:green; color:blue }Figure 12: A CSS file with an unorderable sub-biclique.

the size of the input and the size of the output). To be more precise, the benchmarks in our experiments
had between 31 and 2907 rules, and the mean number of rules was 730. The mean ratio of the numberof maximal bicliques to the number of rules was 1.25, and the maximum was 2.05. As we shall see inSection 8, Z3 may solve the constraints via this encoding quite efficiently.
In the rest of the section, we will describe our encoding in detail. For convenience, our encoding also
allows bounded integer variables. There are standard ways to encode these in binary as booleans (e.g.
see [53]) by bit-blasting (using a logarithmic number of boolean variables).

7.1

Orderable Bicliques

Our description above of the crux of our encoding (by restricting to containment in a maximal biclique)is a simplification. This is because not all sub-bicliques of a maximal biclique correspond to a valid rule
B in a merging opportunity (B, j) with respect to the covering C. [A biclique (X ′ , Y ′ ) is a sub-bicliqueof a biclique (X, Y ) if X ′ ⊆ X and Y ′ ⊆ Y .] To ensure that our constraint φ chooses only valid
rules, it needs to ensure that the sub-biclique that is chosen is “orderable”. More precisely, a biclique
B = (X, Y ) is orderable at position j if it can be turned into a rule B = (X, Y ) (i.e. turning the set Y
of declarations into a sequence Y by assigning an order) that can be inserted at position j in C without
violating the validity of the resulting covering with respect to the order ≺ (from the CSS-graph G). If
there are m rules in C, there are m + 1 positions (call these positions 0, . . . , m) where Y may be inserted
into C. We show below that the position j is crucial to whether B is orderable.
Unorderable bicliques rarely arise in practice (in our benchmarks, the mean percentage of maximal
bicliques that were unorderable at some position was 0.39%), but they have to be accounted for if ouranalysis is to find the optimal rule-merging opportunity. A biclique B = (X, Y ) is unorderable when
they have the same property name (or two related property names, e.g., shorthands) occuring multiple
times with different values in Y . One reason having a CSS rule with the same property name occuringmultiple times with different values is to provide “fallback options” especially because old browsers
may not support certain values in some property names, e.g., the rule.c { color:#ccc; color:rgba(0, 0, 0, 0.5); }says that if rgba() is not supported (e.g. in IE8 or older browsers), then use #ccc. Using this idea, we
can construct the simple example of an unorderable biclique in the CSS file in Figure 12. The ordering
constraints we can derive from this file include(.a, color:blue) ≺ (.a, color:green)
and(.b, color:green) ≺ (.b, color:blue) .
The biclique B({.a, .b}, {color:blue, color:green})
is easily seen to be orderable at position 0 and 1. This is because the final rule in Figure 12 will ensure
the ordering (.b, color:green) ≺ (.b, color:blue) is satisfied, and since B will appear before
this final rule, only (.a, color:blue) ≺ (.a, color:green) needs to be maintained by B (in fact,at position 0, neither of the orderings need to be respected by B). However, at position 2, which is at the36

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongend of the file in Figure 12, both orderings will have to be respected by B. Unfortunately, one of theseorderings will be violated regardless of how one may assign an ordering to blue and green. This
contrived example was made only for illustration, however, our technique should still be able to handle
even contrived examples.
We mention that both checking orderability and ordering a given biclique can be done efficiently.
Proposition 7.1. Given a biclique B, a covering C (with m rules) of a CSS-graph G, and a numberj ∈ {0, . . . , m}, checking whether B is orderable at position j in C can be done in polynomial time.
Moreover, if B is orderable an ordering can be calculated in polynomial time.
The proof of the proposition is easy and is relegated into Appendix A.1.
Maximal Orderable Bicliques
Our Max-SAT encoding φ needs to ensure that we only pick a pair (B, j) such that B is an orderable
biclique at position j in the given covering C, i.e., B corresponds to a rule that can be inserted at position
j in C. Although the check of orderability can be declaratively expressed as a constraint in φ, we foundthat this results in Max-SAT formulas that are rather difficult to solve by existing Max-SAT solvers.
For this reason, we propose to express the check of orderability in a different way. Intuitively, for eachj ∈ {0, . . . , m}, we enumerate all orderable bicliques B = (X, Y ) that are also maximal, i.e., it is not a(strict) sub-biclique of a different orderable biclique. Since “orderability is inherited by sub-bicliques”(as the following lemma, whose proof is immediate from the definition, states), the constraint φ needs
to simply choose a sub-biclique of a maximal orderable biclique that appears in our enumeration.
Lemma 7.2. Every sub-biclique B ′ = (X, Y ) of an orderable biclique B = (X, Y ) is orderable.
The above enumeration of maximal orderable bicliques can be described as a pair ({Mi }µi=1 , F)
whereµ• {Mi }i=1
is an enumeration of all bicliques that are orderable and maximal at some position j,and• F forbids certain bicliques at each position. I.e. it is a function from [1, m] to the set of bicliquesin {Mi }µi=1 that are unorderable at position j.
Observe that the set of orderable bicliques at position j in C is a subset of the set of orderable bicliquesat position j + 1 in C. This may be formally expressed as: F(j) ⊆ F (j + 1) for all j ∈ [1, m).
In the majority (54%) of examples that we have from real-world CSS, the function F maps all valuesof [1, m] to ∅, i.e., all maximal bicliques are orderable at all positions. The mean percentage of maximal
bicliques that were unorderable at some position was 0.39%, with a maximum of 5.84%.
In our description of the Max-SAT encoding below, we assume that the pair ({Mi }µi=1 , F) has been
computed for the input C.

7.2

The Max-SAT Encoding

We present the full reduction of the rule-merging problem to Max-SAT. In particular, the constraints we
produce are(ΠH , ΠS )where ΠH and ΠS are, respectively, hard and soft constraints. First, we describe the variables used inour encoding. Note, our encoding will rely on the assumption that covering C has already been trimmed.
Recall, the notion of trimming is defined in Section 4 and is the process of removing redundant nodes
from a covering. A node is redundant in a rule if all of its incident edges also appear later in the covering.
37

CSS Minification via Constraint Solving

7.2.1

M. Hague, A. W. Lin, and C.-H. Hong

Representing the rule-merging opportunity

We need to represent a merging opportunity (B, j). We use a bounded integer variable j (with range
0 ≤ j ≤ m) to encode j.
For B we select a biclique in {Mi }µi=1 and allow some nodes to be removed (i.e. to produce subbicliques of the Mi ). We use a bounded integer variable iM (with range [1, µ]) to select Mi . Next,
we need to choose a sub-biclique of Mi , which can be achieved by choosing nodes Mi to be removed.
To minimise the number of variables used, we number the nodes contained in each biclique in some(arbitrary) way, i.e., for each i ∈ [1, µ] and biclique Mi = (X, Y ), we define a bijection ρi : X ∪ Y →[1, |X ∪ Y |]. Let χ be the maximum number of nodes in a biclique Mi in the enumeration {Mi }µi=1 ,i.e., the maximal integer k such that ρi (w) = k for some w ∈ S ∪ P and 1 ≤ i ≤ µ.
We introduce boolean variables x1 , . . . , xχ . Once the maximal orderable biclique Mi is picked, fora node w with ρi (w) = k, the variable xk is used to indicate that w is to be excluded from selected Mi(i.e. xk is true iff w is to be excluded from Mi ). More precisely, for an edge e = (s, p) in Mi , we definea predicate HasEdge(e) to be
HasEdge((s, p)) =∨iM = i ∧ ¬xρi (s) ∧ ¬xρi (p) .

1≤i≤µNote, when Mi = (X, Y ) and w ∈/ X ∪ Y we let xρi (w) denote the formula “true”.
7.2.2

Hard Constraints

We defineΠH = {φvld , φord }where φvld and φord are described below.
We need to ensure the rule-merging opportunity is valid, i.e., it has not been forbidden at the chosen
position and inserting it into the covering does not violate the edge order ≺. For the former, we define
F 1st , which is used to discover which of the Mi first become unorderable at position j. That is Mi ∈F 1st (j) if j is the smallest integer such that Mi ∈ F (j).

φvld =∧

()
 j >= j ⇒

∧

(


)
iM ̸= i  .

Mi ∈F 1st (j)1≤j≤m

We also need to ensure the edge ordering is respected by the rule-merging opportunity, for which
we define φord . If e1 ≺ e2 , and e1 = (s1 , p1 ) is in the rule B in the guessed merging opportunity(B, j), then we need to assert e1 ≺ e2 is respected. It is respected either if e2 = (s2 , p2 ) appears after
the position where j is to be inserted in C, or e2 is also contained in the new rule B (in which case theordering can still be respected since B is orderable). That is,
φord = 

∧

(

)



HasEdge((s1 , p1 )) ⇒ j < index((s2 , p2 )) ∨ HasEdge((s2 , p2 ))  .

(s1 ,p1 )≺(s2 ,p2 )This is because only the last occurrence of an edge in a covering matters (recall the definition of index
of an edge in Section 4). Also note that our use of bicliques ensures that we do not introduce pairs (s, p)that are not edges in E.
38

CSS Minification via Constraint Solving

7.2.3

M. Hague, A. W. Lin, and C.-H. HongSoft Constraints

The soft constraints will calculate the weight of C[B → j]↓ . Since we want to minimise this weight,
the optimal solution to the Max-SAT problem will give an optimal rule-merging opportunity. Our soft
constraints areSelsΠS = Π B∪ ΠProps
S ∪ ΠS
S
Sels
where ΠBand ΠProps
counts the weight of the remainder (notS counts the weight of the B, and ΠS
S
including B) of the stylesheet by counting the remaining selectors and properties respectively after
trimming. These are defined below.
To count the weight of B, we count the weight of the non-excluded nodes of Mi = (Xi , Yi ). We
have
{ i
}
ΠB
S = (φw , wt(w)) 1 ≤ i ≤ µ ∧ w ∈ Xi ∪ Yi

where
φiw =

((

)
)
iM = i ⇒ xρi (w) .

Note that φiw is true iff, whenever Mi is picked, the node w is omitted from Mi in the guessed B.
Furthermore, the cost of not omitting w from Mi is wt(w).
Next, we count the remaining weight of C[B → j] (i.e. excluding the weight of B). Assume that C
has already been trimmed, i.e., C↓ = C. The intuition is that a node v can be removed from B i in C if
all edges e incident to v appear in a later rule in C, i.e., index(e) > i. In particular, let B i = (Xi , Y i ) in
{B i }mi=1 . To count the weight of the untrimmed selectors we use the clauses
{
}
ΠSels
= (ψsi , wt(s)) 1 ≤ i ≤ m ∧ s ∈ Xi
S
where






ψsi = i ≤ j ∧

∧index((s,p))=ip∈YHasEdge((s, p)) .


The idea is that ψsi will be satisfied whenever s can be removed from B i . We assume C has already been
trimmed, so s can only become removable because of the application of rule-merging. This explains
the first conjunct which asserts that nodes can only be removed from rules appearing before j. Next, s
can be removed after rule-merging if none of its incident edges (s, p) are the final occurrence of (s, p)
in C[B → j]. The crucial edges in this check are those such that index((s, p)) = i, which means B icontains the final occurrence of (s, p) in C. For these edges, if HasEdge((s, p)) holds, then the new rule
contains (s, p) and B i will no longer contain the final occurrence of (s, p) after rule-merging.
Similarly, to count the weight of the properties that cannot be removed we have{}ΠProps= (ψpi , wt(p)) 1 ≤ i ≤ m ∧ p ∈ Y i
S
where



ψpi = i ≤ j ∧∧
HasEdge((s, p))
 .

index((s,p))=is∈X

39CSS Minification via Constraint Solving

7.3

M. Hague, A. W. Lin, and C.-H. Hong

Generated Rule-Merging Opportunity

The merging opportunity (B, j) is built from an optimal satisfying assignment to (ΠH , ΠS ). First,
j is the value assigned to j. Then B = (X, Y ) where, letting iM be the value of iM , and letting
MiM = (X ′ , Y ′ ),• s ∈ X iff s ∈ X ′ and xρiM (s) is assigned the value false, andm′• Y = {pi }mi=1 , where {pi }i=1 is obtained by assigning an ordering to Y such that (B, j) is a valid
merging opportunity.

That the ordering of Y ′ above exists is guaranteed by the fact that MiM is orderable at j, and Lemma
7.2. We can compute the ordering in polynomial time via Proposition 7.1. We argue the following
proposition in Appendix A.3.
Proposition 7.3. The merging opportunity (B, j) generated from the maximal solution to (ΠH , ΠS ) is
the optimal merging opportunity of C.

8

Experimental Results

We implemented a tool S AT CSS (in Python 2.7) for CSS minification via rule-merging which can befound in our supplementary material. The tool is also available as source code and in a working disk
image via the following URLs.
https://github.com/matthewhague/sat-css-tool
http://www.cs.rhul.ac.uk/home/hague/sat-css-tool.img.txz
It constructs the edge order following Section 5 and discovers a merging opportunity following Section 7. We use Z3 [18] as the back end SMT and Max-SAT solver. As an additional contribution, ourtool can also generate instances in the extended DIMACS format [3] allowing us to use any Max-SAT
solvers. This output may also provide a source of industrially inspired examples for Max-SAT competition benchmarks.
Our benchmarks comprise 72 CSS files coming from three different sources(see Appendix D.2 for a complete listing):
304●• We collected CSS files from each of the top 20 websites on a global ranking list [1].

250
200
150

• CSS files were taken from a further 12 websites selected from the top 2065 websites from the listing above.

100
50
0

• Finally, CSS files were taken from 11 smaller websites such as DBLP.
These were examples used during the development of the tool.
Figure 13: Box plot ofThis selection gives us a wide range of different types of websites, including the file sizes in kilolarge scale industrial websites and those developed by smaller teams. Note, sev- bytes
eral websites contained more than one CSS file and in this case we took a selection of CSS files from the site. Hence, we collected more examples than thenumber of websites used. Figure 13 gives the file-size distribution of the CSS
files we collected.
In the following, we describe the optimisations implemented during the development of S AT CSS.
We then describe the particulars of the experimental setup and provide the results in Figure 15.
40

CSS Minification via Constraint Solving

8.1

M. Hague, A. W. Lin, and C.-H. Hong

Optimisations

We give an overview of the optimisations we used when implementing S AT CSS. In section 8.4 weprovide a detailed evaluation of the proposed optimisations.
• We introduce variables xk only for nodes appearing in the edge order, rather than for all nodes
in a biclique. This is enough to be able to define sub-bicliques of any Mi that can appear at any
position in the covering, but means that the smallest rule-merging opportunity cannot always beconstructed. However, this reduces the search space and leads to an improvement to run times.
For example, given a biclique.a { color: red; background: blue }where the property color: red appears in some pair of the edge ordering, but the property
background: blue does not, we introduce a variable xk which is true whenever color: redis excluded from the biclique, but do not introduce a similar variable for background: blue.
Since background: blue does not appear in the edge order, its presence can never cause aviolation of the edge ordering. This is not the case for color: red, hence we still need theallow the possibility of removing it to satisfy the edge order.
• For a rule-merging application to reduce the size of the file, it must remove at least two nodes
from the covering. Hence, for each Mi let jli be the index of the second rule in C containing someedge in Mi (not necessarily the same edge), and jhi be the index of the last rule containing someedge in Mi Without loss of generality we assert()
iM = i ⇒ j ≥ jli ∧ j ≤ jhi .
µ• We performed the following optimisation when calculating ({Mi }i=1 , F). The majority (58.4%)of benchmarks all maximal bicliques are orderable at all positions, and the mean percentage
of maximal bicliques that were unorderable at some position was 0.39%, with a maximum of
5.84%. However, there are one or two of the largest examples of our experiments where thisenumeration took a minute or so. Since the number of maximal bicliques that are unorderable atsome position is so small, we decided in our implementation to simply remove all such bicliquesfrom the analysis. In this case {Mi }µi=1 is an enumeration of all maximal bicliques that areorderable at all positions j, and F maps all values of [1, m] to ∅. This means that we may not
be able find the optimal rule-merging opportunity as not all bicliques are available, but since theamount of time required to find a rule-merging opportunity is reduced, we are able to find moremerging opportunities to apply.
• Finally, we allowed a multi-threaded partitioned search. This works as follows. The search spaceis divided across n threads, and each thread partitions its search space into m partitions. During
iteration j, thread k allows only those Mi where i = k ∗ m + (j mod m). If the fastest threadfinds a merging opportunity in t seconds, we wait up to 0.1t seconds for further instances. We
take the best merging opportunity of those that have completed. A thread reports “no merging
opportunities found” only if none of its partitions contain a merging opportunity.
For the experiments we implemented a simple heuristic to determine the number of threads andpartitions to use. We describe this heuristic here, but first note that better results could likely beobtained with systematic parameter tuning rather than our ad-hoc settings. The heuristic used wasto count the number of nodes in the CSS file; that is, the total number of selectors and property
declarations (this total includes repetitions of the same node – we do not identify repetitions of41

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongthe same node). The tool creates enough partitions to give up to 750 nodes per partition. If only
two partitions are needed, only one thread is used. Otherwise S AT CSS first creates new threads– up to the total number of CPUs on the machine. Once this limit is reached, each thread ispartitioned further until the following holds: number of threads ∗partitions per threads ∗750 ≤number of nodes.
For the edge ordering:• We do not support attribute selectors in full, but perform simple satisfiability checks on the mostcommonly occurring types of constraints. These cover all constraints in our benchmarks. However, we do support shorthand properties.
• Instead of doing a full Existential Presburger encoding, we do a backwards emptiness check of
the CSS automata. This backwards search collects smaller Existential Presburger constraints
describing the relationship between siblings in the tree, and checks they are satisfiable before
moving to a parent node. Global constraints such as ID constraints are also collected and checkedat the root of the tree. This algorithm is described in Appendix D.1.

8.2

Results

The experiments were run on a Dell Latitude e6320 laptop with 4Gb of RAM and four 2.7GHz Intel
i7-2620M cores. The Python interpreter used was PyPy 5.6 [54] and the backend version of Z3 was 4.5.
Each experiment was run up to a timeout of 30 minutes. In the case where CSS files used media queries(which our techniques do not yet support), we used stripmq [29] with default arguments to remove themedia queries from CSS files. Also, we removed whitespaces, comments, and invalid CSS from all the
CSS files before they were processed by the minifiers and our tool.
We used a timeout of 30 minutes because minification only needs to be applied once before deployment of the website. We note that the tool finds many merging opportunities during this period and aminified stylesheet can be produced after each application of rule-merging. This means the user will beable to trade time against the amount of size reduction made. Moreover, applications of rule-merging
tend to show a “long-tail” where the first applications found provide larger savings and the later applications show diminishing returns (see Figure 14). The returns are diminishing because our MaxSAT
encoding always searches for the rule merging opportunity with the largest saving.

8.3

Main Results

5

Saving %10

15

Table 1 and Figure 15 summarise the results. We compared our tool with six popular minifiers in current
usage [60]. There are two groups of results: the first set show the results when either our tool or oneof the minifiers is used alone on each benchmark; the second show the results when the CSS files arerun first through a minifier and then through our tool. This second batch of results shows a significant
improvement over running single tools in isolation. Thus, our tool complements and improves existing
minification algorithms and our techniques may be incorporated into a suite of minification techniques.
Table 1 shows the savings, after whitespaces and comments are removed, obtained by S AT CSS and the six minifiers when they are used alone and together. The table
presents the savings in seven percentile ranks that include
the minimal (0th), the median (50th), and the maximal values (100th). The upper half of the table shows the savings
obtained in bytes, while the lower half shows the savings
as percentages of the original file sizes. The first seven

0

42

0

500

1000
Time (s)1500

Figure 14: Savings against time for S AT CSS
on each benchmark

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

Tool
Percentile

satcsscsso

cssnanocleancss

minifyyui

cssminsatcss +csso

satcss +cssnanosatcss +cleancsssatcss +minifysatcss +yuisatcss +cssmin

0th
20th
40th
50th
60th
80th
100th

0
320
1011
2013
3065
4820
81693

-70
258
877
1527
2955
5656
86367

9
100
462
1042
1556
3822
76238

9
199
738
1354
2081
5449
69573

0
5
28
72
153
355
3501

0
13
35
92
157
326
3464

0
3
24
61
117
212
3224

37
467
1942
4025
5007
8268
100734

32
444
1353
3022
4370
7202
97710

45
562
1733
4253
4677
8595
90710

22
362
1241
2518
3264
5108
78245

24
366
1082
2290
3279
4765
82101

24
369
1158
2736
3304
5127
77827

0th
20th
40th
50th
60th
80th
100th

0.00
1.79
2.90
3.79
4.62
8.12
26.44

-0.56
1.45
2.54
3.29
4.40
6.13
27.95

0.02
0.75
1.47
1.84
2.42
5.18
24.67

0.10
1.21
2.55
3.03
3.64
6.04
25.68

0.00
0.02
0.10
0.15
0.22
0.56
6.44

0.00
0.04
0.17
0.21
0.26
0.64
6.38

0.00
0.01
0.09
0.18
0.21
0.49
3.56

0.14
2.96
4.90
5.78
6.50
10.11
32.60

0.12
2.65
3.94
4.90
5.64
10.98
31.62

0.33
3.60
5.05
6.10
7.45
10.42
29.54

0.09
2.00
3.47
4.03
4.68
8.21
25.59

0.09
2.04
3.41
4.10
4.70
8.09
26.57

0.09
2.04
3.41
4.15
4.68
8.39
25.66

Table 1: Percentile ranks of the savings in bytes (above) and in percentages (below)

columns in the table show the savings when either our toolor one of the minifiers is used alone; the rest of the columns
show the results when the CSS files are processed first by
a minifier and then by our tool. Figure 15 shows the samedata in visual form. It can be seen that S AT CSS tends toachieve greater savings than each of the six minifiers on ourbenchmarks. Furthermore, even greater savings can be obtained when S AT CSS is used in conjunction with any of thesix minification tools. More precisely, when run individually, S AT CSS achieves savings with a third quartile of 6.90% and a median value of 3.79%, while thesix minifiers achieve savings with third quantiles and medians up to 5.45% and 3.29%, respectively.
When we run S AT CSS after running any one of these minifiers, the third quartile of the savings canbe increased to 8.26% and the median to 4.70%. The additional gains obtained by S AT CSS on top of
the six minifiers (as a percentage of the original file size) have a third quartile of 5.03% and a medianvalue of 2.80%. Moreover, the ratios of the percentage of savings made by S AT CSS to the percentage
of savings made by the six minifiers have third quartiles of at least 136% and medians of at least 48%.
These figures clearly indicate a substantial proportion of extra space savings made by S AT CSS. We
comment in the next section on how our work may be integrated with existing tools.
In Figure 14 we plot for each benchmark, the savings made as time progresses. Each line represents
one benchmark. Our algorithm repeatedly searches for and applies merging opportunities. Once one
opportunity has been found, the search begins again for another. Hence, the longer S AT CSS is run, themore opportunities can be found, and the more space saved. Since we search for the optimal merging
opportunities first, we can observe a long-tail, with the majority of the savings being made early in therun. Hence, SatCSS could be stopped early while still obtaining a majority of the benefits. We further
note that in 43 cases, S AT CSS terminated once no more merging opportunities could be found. In theremaining 29 cases, the timeout was reached. If the timeout were extended, further savings may befound.
Finally, we remark on the validation of our tool. First, our model is built upon formal principles
using techniques that are proven to maintain the CSS semantics. Moreover, our tool verifies that theoutput CSS is semantically equivalent to the input CSS. Thus we are confident that our techniques arealso correct in practice. A reliable method for truly comparing whether the rendering of webpages
using the original CSS and the minified CSS is identical is a matter for future work, for which the recent
Visual Logic of Panchekha et al. [49] may prove useful. In lieu of a systematic validation, for each of ourexperiment inputs, we have visually verified that the rendering remains unchanged by the minification.
Such a visual inspection can, of course, only be considered a sanity-check.
43

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong100734 97710

81693 86367 76238
69573
●
●
●

●

●

90710
●

●

78245 82101 77827
●

●

●

16000
14000
12000

Bytes

10000
8000

3501

3464

●

●

yui

4000

minify

6000
3224
●

2000

●

satcss + yui

satcss + cssmin

●

25.6

26.6

25.7

29.5
●

●

●

●

satcss + yui

31.6

●

satcss + minify

32.6

satcss + cleancss

satcss + cssnano

25.7

satcss + csso

24.7

satcss + minify●●

cssmin28

cleancss

csso

26.4

cssnanosatcss

0

●

20

16

Percent

12

8
6.4

6.4

●

●

3.6

4

●

satcss + cssmin

satcss + cleancss

satcss + cssnano

satcss + csso

cssminyui

minifycleancss

cssnanocsso

satcss0

Figure 15: Box plots of the savings in bytes (above) and in percentages (below)

44

CSS Minification via Constraint Solving

8.4

M. Hague, A. W. Lin, and C.-H. Hong

Evaluations of Optimisations

For each of our optimisations, we ran S AT CSS on the unminified 72 benchmarks with the optimisation
disabled. The results are shown in Figure 16 and Figure 17. In Figure 17, the “satcss” column shows theperformance of S AT CSS implemented as described above. As described above, of the 72 benchmarks,
S AT CSS completed within the timeout (no more merging-opportunities could be found) in 43 cases, andwas stopped early due to the timeout in the remaining 29. The comparison with the effect of disabling
optimisations is shown in Table 2.
Figure 16 shows the time taken by S AT CSS to construct the edge order for each benchmark using
the optimised emptiness of intersection algorithm presented in Appendix D.1 and the non-optimised encoding presented in Section 6. The timeout was kept at 30 minutes. The optimised algorithm completed
the edge order construction on all benchmarks, while the timeout was reached in 19 cases by the unoptimised algorithm.
A clear advantage can be seen for the optimised approach.
1775.1

Next we compared the straightforward encoding of the rulemerging problem into Max-SAT discussed at the start of Sec1000
900
tion 7 with the biclique encoding which was the main topic
800
of Section 7. S AT CSS using the straightforward encoding ap700
600
pears as “nobicliques” in Figure 17. With the straightforward
500
400
encoding, the tool completed within the timeout in 45 cases, and
300
216.4
reached the timeout in the remaining 27. It can been seen that
200
100
there is a clear benefit to the biclique encoding.
0
We also consider the optimisation that introduces variables
xk only for nodes appearing in the edge order, rather than for
all nodes in a biclique. Disabling this optimisation appears as“fullexc” in Figure 17. With this optimisation disabled, the toolcompleted within the timeout in 36 cases, and reached the time- Figure 16: Box plots of the time takenout in the remaining 36. We can see a modest gain from this to construct the CSS edge order with the
optimised and unoptimised emptiness of
simple optimisation.
intersection tests
We then study the effect of removing all unorderable biµcliques. The “unlimbicliques” column in Figure 17 shows the effect of allowing ({Mi }i=1 , F) to be
calculated in full. That is, unorderable bicliques are split into orderable sub-bicliques. With full bicliqueenumeration, the tool completed within the timeout in 42 cases, and reached the timeout in the remaining 30. This had only a small effect on performance, which is expected. The purpose of this limiting
biclique generation in S AT CSS is to prevent the rare examples of unorderable bicliques from having alarge effect on performance in some cases.
The next optimisation in Figure 17, “nothread”, shows the performance ofOptimisation
Terminated
S AT CSS with multi-threading and partitioning disabled. That is, the searchsatcss43
space is not split up across several Max-SAT encodings. Without multi- nobicliques
4536
threading or partitioning, the tool completed within the timeout in 40 cases, fullexc
unlimbicliques42
and reached the timeout in the remaining 32. There is a noticeable degrada- nothread
40
50
tion in performance when this optimisation is disabled. The final column in noord
Figure 17 studies the following hypothetical scenario. The reader may wonder Table 2: The number
whether CSS developers may be able to improve performance by specifying of examples terminating
invariants of the documents to which the CSS will be applied. For example, with no more discovered
the developer may specify that a node with class a will never also have class b. merging opportunities inIn this case pairs such as (.a, .b) can be removed from the edge-order. Thus, standard mode and with
document-specific knowledge may improve performance by reducing the num- certain optimisations disabled
ber of ordering constraints that need to be maintained. The column “noord”
Time (s)●unoptimised

optimised●

45

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

119483
●

81693

68733

●

●

26000
24000
21317

22000

●

20000
18000
Bytes

16000
13509

14000

●

12000
10000
8000
6000
4000
1098

2000

●

noord

nothread

unlimbicliques

fullexc

nobicliques

satcss

0

38.7

22.2

25.5

25.6

●

●

nothread●

unlimbicliques

●

26.4
●

20

16

14.7

Percent

●

12

8

4

noord

fullexc

nobicliques

satcss0

Figure 17: The savings in bytes (above) and in percentages (below) with certain optimisations disabled46

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongshows the performance of S AT CSS when the edge-ordering is empty, i.e., there is no edge ordering.
Without the edge ordering, the tool completed within the timeout in 50 cases, and reached the timeout
in the remaining 22. This represents a best-case scenario if document invariants were considered. Thus,
if we were to extend S AT CSS to also take a set of invariants, we could see a large improvement in thesavings found. However, we also note that these savings do not dwarf the performance of S AT CSS
without invariants.

9

Related WorkCSS minification started to receive attention in the web programming community around the year 2000.
To the best of our knowledge, the first major tools that could perform CSS minification were Yahoo! YUI
Compressor [59] and Microsoft Ajax Minifier, both of which were developed around 2004–2006. Thisis followed by the development of many other CSS minifiers including (in no particular order) cssmin[8], clean-css [51], csso [19], cssnano [13], and minify [16]. Such minifiers mostly apply
syntactic transformations including removing whitespace characters, comments, and replacing stringsby their abbreviations (e.g. #f60 by #ff6600). More and more advanced optimisations are also being
developed. For example, cssnano provides a limited support of our rule-merging transformations,wherein only adjacent rules may be merged. The lack of techniques for handling the order dependencies of CSS rules [62] was most likely one main reason why a more general notion of rule-merging
transformations (e.g. that can merge rules that are far away in the file) is not supported by CSS minifiers.
In our experiments, we ran S AT CSS after running the existing minifiers described above. It is
likely that the order of execution is important: the rewrites applied by existing minifiers will put the
CSS into a more normalised format, which will improve the possibility of selectors sharing the samedeclarations. Moreover, these minifiers implement ad-hoc techniques, such as the limited rule-merging
transformations of cssnano described above. After an application of our tool it is possible that someof these ad-hoc techniques may become applicable, leading to further savings. Thus, we posit that our
techniques could be combined with the techniques of existing minifiers in a combined minification loop,
which is run until a fixed point or timeout is reached.
Although the importance of CSS minification is understood in industry, the problem received little
attention in academia until very recently. Below we will mention the small number of existing work on
formalisation of CSS selectors and CSS minification, and other relevant work.
The lack of theories for reasoning about CSS selectors was first mentioned in the paper [25], wherein
the authors developed a tree logic for algorithmically reasoning about CSS selectors, i.e., by developing
algorithms for deciding satisfiability of formulas in the logic. This formalisation does not capture thewhole class of CSS3 selectors; as remarked in their follow-up paper [11], the logic captures 70% of
the selectors in their benchmarks from real-world CSS files. In particular, they do not fully support
attribute selectors (e.g. [l*="bob"]). Our paper provides a full formalisation of CSS3 selectors. In
addition, their tree logic can express properties that are not expressible in CSS. Upon a closer inspection,
their logic is at least as expressive as µ-calculus, which was a well-known logic in database theory forformalising query languages over XML documents, e.g., see [37, 47] for two wonderful surveys. As
such, the complexity of satisfiability for their tree logic is EXPTIME-hard. Our formalisation captures
no more than the expressive power of CSS3 selectors, which helps us obtain the much lower complexity
NP and enables the use of highly-optimised SMT-solvers. There is a plethora of other work on logics
and automata on unranked trees (with and without data), e.g., see [40, 6, 27, 67, 68, 66, 41, 31, 5, 48,
23, 38, 24, 21, 57, 17, 26] and the surveys [37, 47, 9]. However, none of these formalisms can capture
certain aspects of CSS selectors (e.g. string constraints on attribute values), even though they are much
more powerful than CSS selectors in other aspects (e.g. navigational).
There are a handful of research results on CSS minification that appeared in recent years. Loosely
47

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongspeaking, these optimisations can be categorised into two: (a) document-independent, and (b) documentdependent. Document-independent optimisations are program transformations that are performed completely independently of the web documents (XML, HTML, etc.). On the other hand, documentdependent optimisations are performed with respect to a (possibly infinite) set of documents. Existing
CSS minifiers only perform document-independent optimisations since they are meant to preserve thesemantics of the CSS file regardless of the DOMs to which the CSS file is applied. Our work in thispaper falls within this category too. Such optimisations are often the most sensible option in practiceincluding (1) the case of generic stylesheets as part of web templates (e.g. WordPress), and (2) the casewhen the DOMs are generated by a program. Case (2) requires some explanation. A typical case of
DOMs being generated by programs occurs in HTML5 web pages. An HTML5 application comes witha finite set of HTML documents, JavaScript code, and CSS files. The presence of JavaScript meansthat potentially infinitely many possible DOM-trees could be generated and displayed by the browser.
Therefore, a CSS minification should not affect the rendering of any such tree by the browser. Although a document-dependent optimisation (that take these infinitely many trees into account) seems
appropriate, this is far from realistic given the long-standing difficulty of performing sound static analysis for JavaScript especially in the presence of DOM-trees [56, 63, 2, 34, 33, 28]. This would makean interesting long-term research direction with many more advances on static analysis for JavaScript.
However, the problem is further compounded by the multitude of frameworks deployed on the serverside for HTML creation (e.g. PHP, Java Server Pages, etc.), for which individual tools will need to
be developed. Until then, a practical minifier for HTML5 applications will have to make do with
document-independent optimisations for CSS files.
The authors of [43] developed a document-dependent dynamic analysis technique for detecting andremoving unused CSS selectors in a CSS file that is part of an HTML5 application. A similar tool,
called UnCSS [39], was also later developed. This is done by instrumenting the HTML5 application
and removing CSS selectors that have not been used by the end of the instrumentation. The drawbackof this technique is that it cannot test all possible behaviours of an HTML5 application and may may
accidentally delete selectors that can in reality be used by the application. It was noted in [28] that suchtools may accidentally delete selectors, wherein the HTML5 application has event listeners that require
user interactions. The same paper [28] develops a static analysis technique for overapproximating the setof generated DOM-trees by using tree rewriting for abstracting the dynamics of an HTML5 application.
The technique, however, covers only a very small subset of JavaScript, and is difficult to extend without
first overcoming the hard problem of static analysis of JavaScript.
The authors of [11] applied their earlier techniques [25] to develop a document-independent CSS
minification technique that removes “redundant” property declarations, and merges two rules with semantically equivalent selectors. The optimisations that they considered are orthogonal to and can beused in conjunction with the optimisation that we consider in this paper. More precisely, they developed
an algorithm for checking selector subsumption (given two selectors S1 and S2 , whether the selector S1
is subsumed by the selector S2 , written S1 ⊆ S2 ). A redundant property declaration p in a rule R1 witha selector S1 can, then, be detected by finding a rule R2 that also contains the declaration p and has aselector S2 with a higher specificity than S1 and that S1 ⊆ S2 . As another example, whenever we canshow that the selectors S1 and S2 of two rules R1 and R2 to be semantically equivalent (i.e. S1 ⊆ S2
and S2 ⊆ S1 ), we may merge R1 with R2 under certain conditions. The authors of [11] provided sufficient conditions for performing this merge by relating the specificities of S1 and S2 with the specificitiesof other related selectors in the file (but not accounting for the order of appearances of these rules in thefile). In general, a CSS rule might have multiple selectors (a.k.a. selector group), each with a different
specificity, and it is not clear from the presentation of the paper [11] how their optimisations extend to
the general case.
48

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

The authors of [42] developed a document-dependent10 CSS minification method with an advanced
type of rule merging as one of their optimisations. This is an ambitious work utilising a number oftechniques from areas such as data mining and constraint satisfaction. Although their work differs fromours because of its document-dependence, the use of rule-merging is closely related to our own, hence
we will describe in detail some key differences with our approach. The techniques presented in thispaper can be viewed as a substantial generalisation of their rule merging optimisation. Loosely speaking,in terms of our graph-theoretic framework, their technique first enumerates all maximal bicliques with atleast two selectors. This is done with the help of an association rule mining algorithm (from data mining)with a set of property declarations viewed as an itemset. Second, for each such maximal biclique B,
a value n is computed that reflects how much saving will be obtained if B could somehow be inserted
into the file and every occurrence of each property declaration in B is erased from the rest of the CSS
file. Note that n is independent of where B is inserted into the CSS file. Third, for each such maximal
biclique B (ranked according to their values in a non-increasing order), a solver for the (finite-domain)
constraint satisfaction problem is invoked to check whether B can be placed in the file (with every
occurrence of each property declaration in B is erased from the rest of the CSS file) while preserving
the order dependency. If this check fails, the solver will also be invoked to check if one can insert subbicliques of B (with a maximal set S of selectors with |S| ≥ 2) in the file. Possible positions in thefile to place each selector of B are encoded as variables constrained by the edge order dependency thatis relativised to the provided HTML documents. To test whether two edges should be ordered in thisrelativised edge order, the selectors are not subject to a full intersection test, but instead a relativisedintersection test that checks whether there is some node in the given finite set of html documents thatis matched by both selectors. Their techniques do not work when the HTML documents are not given,
which we handle in this paper. Another major difference to our paper is that their algorithm sequentiallygoes through every maximal biclique B (ranked according to their values) and checks if it can be inserted
into the file, which is computationally too prohibitive especially when the (unrelativised) edge order ≺is used. Our algorithm, instead, fully relegates the search of an appropriate B and the position in the file
to place it to a highly-optimised Max-SAT solver, which scales to real-world CSS files. In addition, their
type of rule merging is also more restricted than ours for two other reasons. First, the new rule inserted
into the file has to contain a maximal set of selectors. This prohibits many rule-merging opportunities
and in fact does not subsume the merging adjacent rule optimisation of cssnano [13] in general. For
example, consider the CSS file.class1 { color:blue }.class2 { color:blue }.class3 { color:red }.class4 { color:blue }Notice that we cannot group together the first, second, and fourth rules since this would change thecolour of a node associated with the classes class2 and class3, or with the classes .class3 andclass4. On the other hand, the first two rules can be merged resulting in the new file.class1, .class2 { color:blue }.class3 { color:red }.class4 { color:blue }However, this is not permitted by their merging rule since .class1,.class2{color:blue} does
not contain a maximal set of selectors. Second, given a maximal biclique B, their merging operationerases every occurrence of the declarations of B everywhere else in the file. This further rules out certain
rule-merging opportunities. For example, consider the CSS file
10 More precisely, dependent on a given finite set of HTML documents

49

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong.class1 { color:blue; font-size: large }.class2 { color:blue; font-size: large }.class4 { font-size: large }.class3 { color:red }.class4 { color:blue }and observe the following maximal biclique in the file.
.class1, .class2, .class4 { color:blue; font-size: large }Unfortunately, this is not a valid opportunity using their merging rule since this CSS file is not equivalentto.class1, .class2, .class4 { color:blue; font-size: large }.class3 { color:red }nor to the following file.
.class3 { color:red }.class1, .class2, .class4 { color:blue; font-size: large }In this paper, we permit duplicate declarations, and would insert this maximal biclique just before thefourth rule in the file (and perform trim) resulting in the following equivalent file.
.class1, .class2, .class4 { color:blue; font-size: large }.class3 { color:red }.class4 { color: blue }Finally, each maximal biclique in the enumeration of [42] does not allow two property declarations
with the same property name. As we explained in Section 7, CSS rules satisfying this property are
rather common since they support fallback options. Handling such bicliques (which we do in thispaper) requires extra technicalities, e.g., the notion of orderable bicliques, and adding an order to thedeclarations in a biclique.
We also mention that there have been works [44, 50, 32] on solving web page layout using constraint
solvers. These works are orthogonal to this paper. For example, [50] provides a mechanised formalisation of the semantics of CSS for web page layout (in quantifier-free linear arithmetic), which allows
them to use an SMT-solver to automatically reason about layout. Our work provides a full formalisationof CSS selectors, which is not especially relevant for layout. Conversely, the layout semantics of various
property declarations is not relevant in our CSS minification problem.
Finally, we also mention the potential application of rule-merging to CSS refactoring. This was
already argued in [42], wherein the metric of minimal file size is equated with minimal redundancies.
More research is required to discover other classes of CSS transformations and metrics that are moremeaningful in the context of improving the design of stylesheets. Constraint-based refactoring has also
been studied in the broader context of programming languages, e.g., see [64, 69]. It would be interesting
to study how refactoring for CSS can be cast into the framework of constraint-based refactoring aspreviously studied (e.g. in [64]).

10 Conclusion and Future Work
We have presented a new CSS minification technique via merging similar rules. Our techniques canhandle stylesheets composed of CSS rules which contain a set of CSS Level 3 selectors and list of property declarations. This technique exploits the fact that new rules may be introduced that render other50

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongparts of the document redundant. After removing the redundant parts, the overall file size may be reduced. Such a solution has required the development of a complete formalisation of CSS selectors andtheir intersection problem as well as a formalisation of the dependency ordering present in a stylesheet.
This intersection problem was solved by means of an efficient encoding to quantifier-free integer linear arithmetic, for which there are highly-optimised SMT solvers. Moreover, we have formalised our
CSS rule-merging problem and presented a solution to this problem using an efficient encoding into
MaxSAT formulas. These techniques have been implemented in our tool S AT CSS which we have comprehensively compared with state-of-the-art minification tools. Our results show clear benefits of ourapproach.
Both our formalisation and our tool strictly follow the W3C specifications. In practice, web developers may not always follow these guidelines, and implement convenient abuses that do not trouble
existing web browsers. One particular example is the use of ID values that are not necessarily unique.
In this example case, it would be possible to treat ID values similarly to classes, and relax our analysis appropriately. In general, one may wish to adapt our constraints to handle other common abuses.
However, this is beyond the scope of the current work.
CSS preprocessors such as Less [58] and Sass [14] — which extend the CSS language with usefulfeatures such as variables and partial rules — are commonly used in web development. Since Less andSass code is compiled into CSS before deployment, our techniques are still applicable.
There are many technologies involved in website development and deployment. These technologies
provide a variety of options for further research, some of which we briefly discuss here.
First, we may expand the scope of the CSS files we target. For example, we may expand our definition of CSS selectors to include features proposed in the CSS Selectors Level 4 working draft [20] (i.e.
still not stable). These features include extensions of the negation operator to allow arbitrary selectors
to be negated. It would be interesting to systematically investigate the impact of these features on thecomplexity of the intersection problem. We believe that such a systematic study would be informativein determining the future standards of CSS Selectors.
Another related technology is that of media queries that allow portions of a CSS file to only beapplied if the host device has certain properties, such as a minimum screen size. This would involve
defining semantics of media queries (not part of selectors), and extending our rule-merging problem toinclude media queries and rules grouped under media queries.
Second, we could also consider additional techniques for stylesheet optimisation. Currently we takea greedy approach where we search for the “best” merging opportunity at each iteration. Techniquessuch as simulated annealing allow a proportion of non-greedy steps to be applied (i.e. choose a merging
opportunity that does not provide the largest reduction in file size). This allows the optimisation process
to explore a larger search space, potentially leading to improved final results. Another approach might
be to search for multiple simultaneous rule-merging opportunities.
Finally, our current optimisation metric is the raw file size. We could also attempt to provide an
encoding that seeks to find the best file size reduction after gzip compression. [Gzip is now supported
by many web hosts and most modern browsers (though not including old IE browsers).] One simple
technique that could help bring down the compressed file size is to sort the selectors and declarations ineach rule after the minification process is done [35].

Acknowledgements
We are grateful for the support that we received from the Engineering and Physical Sciences ResearchCouncil [EP/K009907/1], Google (Faculty Research Award), and European Research Council (grant
agreement no. 759969). We also thank Davood Mazinanian for answering questions about his work.
51

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

References[1] Alexa Internet. Alexa top 500 global sites. https://www.alexa.com/topsites, 2017. Referred in
April 2017.
[2] E. Andreasen and A. Møller. Determinacy in static analysis for jQuery. In OOPSLA, pages 17–31, 2014.
[3] Josep Argelich, Chu Min Li, Felip Manyà, and Jordi Planes. Max-sat’16 competition. http://maxsat.
ia.udl.cat/, 2016. Referred in April 2017.
[4] Tab Atkins Jr., Elika J. Etemad, and Florian Rivoal. Css snapshot 2017. https://www.w3.org/TR/
css-2017, 2017. Referred in August 2017.
[5] Michael Benedikt, Wenfei Fan, and Floris Geerts. XPath satisfiability in the presence of dtds. In Proceedingsof the Twenty-fourth ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems, June
13-15, 2005, Baltimore, Maryland, USA, pages 25–36, 2005.
[6] Michael Benedikt, Wenfei Fan, and Gabriel M. Kuper. Structural properties of XPath fragments. In Database
Theory - ICDT 2003, 9th International Conference, Siena, Italy, January 8-10, 2003, Proceedings, pages
79–95, 2003.
[7] Nikolaj Bjørner and Nina Narodytska. Maximum satisfiability using cores and correction sets. In Proceedingsof the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires,
Argentina, July 25-31, 2015, pages 246–252, 2015.
[8] Johan Bleuzen. cssmin. https://www.npmjs.com/package/cssmin, 2017. Referred August 2017.
[9] Mikołaj Bojańczyk. Automata for data words and data trees. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications, RTA 2010, July 11-13, 2010, Edinburgh, Scottland, UK,pages 1–4, 2010.
[10] Bert Bos. Cascading style sheets level 2 revision 2 (css 2.2) specification. https://www.w3.org/TR/
CSS22/, 2016. Referred August 2017.
[11] Martí Bosch, Pierre Genevès, and Nabil Layaïda. Reasoning with style. In Proceedings of the Twenty-FourthInternational Joint Conference on Artificial Intelligence, IJCAI 2015, Buenos Aires, Argentina, July 25-31,
2015, pages 2227–2233, 2015.
[12] Aaron R. Bradley and Zohar Manna. The Calculus of Computation: Decision Procedures with Applications
to Verification. Springer-Verlag New York, Inc., Secaucus, NJ, USA, 2007.
[13] Ben Briggs and Contributors. cssnano. http://cssnano.co, 2015. Referred in August 2017.
[14] Hampton Catlin, Natalie Weizenbaum, Chris Eppstein, and Contributors. Sass. http://sass-lang.
com/, 2006. Referred in August 2017.
[15] T. Çelik, E. J. Etemad, D. Glazman, I. Hickson, P. Linss, and J. Williams. Selectors level 3: W3c recommendation 29 september 2011. http://www.w3.org/TR/2011/REC-css3-selectors-20110929/,
2011. Referred in August 2017.
[16] Steve Clay and Contributors. minify. https://github.com/mrclay/minify, 2017. Referred inAugust 2017.
[17] Claire David, Leonid Libkin, and Tony Tan. Efficient reasoning about data trees via integer linear programming. ACM Trans. Database Syst., 37(3):19:1–19:28, 2012.
[18] L. Mendonça de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.
[19] Roman Dvornov and Contributors. csso. https://github.com/css/csso, 2017. Referred in August
2017.
[20] Elika J. Etemad and Tab Atkins Jr. Selectors level 4: W3c working draft 2 may 2013. http://www.w3.
org/TR/2013/WD-selectors4-20130502/, 2013.
[21] Diego Figueira. Reasoning on words and trees with data: On decidable automata on data words and data
trees in relation to satisfiability of LTL and XPath. PhD thesis, Ecole Normale Superieure de Cachan, 2010.
[22] Ferenc Gécseg and Magnus Steinby. Handbook of formal languages, vol. 3. chapter Tree Languages, pages
1–68. Springer-Verlag New York, Inc., New York, NY, USA, 1997.
[23] Floris Geerts and Wenfei Fan. Satisfiability of XPath queries with sibling axes. In Database Programming

52

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

Languages, 10th International Symposium, DBPL 2005, Trondheim, Norway, August 28-29, 2005, Revised
Selected Papers, pages 122–137, 2005.
[24] Pierre Genevès and Nabil Layaïda. A system for the static analysis of XPath. ACM Trans. Inf. Syst., 24(4):475–
502, 2006.
[25] Pierre Genevès, Nabil Layaïda, and Vincent Quint. On the analysis of cascading style sheets. In Proceedingsof the 21st World Wide Web Conference 2012, WWW 2012, Lyon, France, April 16-20, 2012, pages 809–818,
2012.
[26] Pierre Genevès, Nabil Layaïda, Alan Schmitt, and Nils Gesbert. Efficiently deciding µ-calculus with converse
over finite trees. ACM Trans. Comput. Log., 16(2):16:1–16:41, 2015.
[27] Georg Gottlob and Christoph Koch. Monadic queries over tree-structured data. In 17th IEEE Symposiumon Logic in Computer Science (LICS 2002), 22-25 July 2002, Copenhagen, Denmark, Proceedings, pages
189–202, 2002.
[28] Matthew Hague, Anthony Widjaja Lin, and C.-H. Luke Ong. Detecting redundant CSS rules in HTML5
applications: a tree rewriting approach. In Proceedings of the 2015 ACM SIGPLAN International Conference
on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2015, part of SPLASH
2015, Pittsburgh, PA, USA, October 25-30, 2015, pages 1–19, 2015.
[29] Jake Hickenlooper. stripmq. https://www.npmjs.com/package/stripmq, 2014. Referred in August 2017.
[30] Ian Hickson, Robin Berjon, Steve Faulkner, Travis Leithead, Erika Doyle Navara, Edward O’Connor, andSilvia Pfeiffer. Html5. https://www.w3.org/TR/html5/, 2014. Referred August 2017.
[31] Jan Hidders. Satisfiability of XPath expressions. In Database Programming Languages, 9th International
Workshop, DBPL 2003, Potsdam, Germany, September 6-8, 2003, Revised Papers, pages 21–36, 2003.
[32] Thibaud Hottelier and Rastislav Bodik. Synthesis of layout engines from relational constraints. In Proceedingsof the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages,
and Applications, OOPSLA 2015, pages 74–88, New York, NY, USA, 2015. ACM.
[33] S. H. Jensen, M. Madsen, and A. Møller. Modeling the HTML DOM and browser API in static analysis of
JavaScript web applications. In SIGSOFT/FSE, pages 59–69, 2011.
[34] S. H. Jensen, A. Møller, and P. Thiemann. Type Analysis for JavaScript. In SAS, pages 238–255, 2009.
[35] Meitar Moscovitz Joseph R. Lewis. AdvancED CSS. APress, 2010.
[36] Enver Kayaaslan. On enumerating all maximal bicliques of bipartite graphs. In 9th Cologne-Twente Workshop
on Graphs and Combinatorial Optimization, Cologne, Germany, May 25-27, 2010. Extended Abstracts, pages
105–108, 2010.
[37] Leonid Libkin. Logics for unranked trees: An overview. Logical Methods in Computer Science, 2(3), 2006.
[38] Leonid Libkin and Cristina Sirangelo. Reasoning about XML with temporal logics and automata. J. Applied
Logic, 8(2):210–232, 2010.
[39] Glacomo Martino and Contributors. Uncss. https://github.com/giakki/uncss, 2013. Referred
April 2017.
[40] Maarten Marx. Conditional xpath. ACM Trans. Database Syst., 30(4):929–959, 2005.
[41] Maarten Marx and Maarten de Rijke. Semantic characterizations of navigational xpath. SIGMOD Record,34(2):41–46, 2005.
[42] Davood Mazinanian, Nikolaos Tsantalis, and Ali Mesbah. Discovering refactoring opportunities in cascadingstyle sheets. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software
Engineering, (FSE-22), Hong Kong, China, November 16 - 22, 2014, pages 496–506, 2014.
[43] Ali Mesbah and Shabnam Mirshokraie. Automated analysis of CSS rules to support style maintenance. In
34th International Conference on Software Engineering, ICSE 2012, June 2-9, 2012, Zurich, Switzerland,
pages 408–418, 2012.
[44] Leo A. Meyerovich and Rastislav Bodík. Fast and parallel webpage layout. In Proceedings of the 19thInternational Conference on World Wide Web, WWW 2010, Raleigh, North Carolina, USA, April 26-30, 2010,
pages 711–720, 2010.

53

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong[45] A. Muscholl and I. Walukiewicz. An np-complete fragment of LTL. Int. J. Found. Comput. Sci., 16(4):743–
753, 2005.
[46] Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided maxsat resolution. In
Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City,
Québec, Canada., pages 2717–2723, 2014.
[47] Frank Neven. Automata theory for xml researchers. SIGMOD Rec., 31(3):39–46, September 2002.
[48] Frank Neven and Thomas Schwentick. On the complexity of xpath containment in the presence of disjunction,
dtds, and variables. Logical Methods in Computer Science, 2(3), 2006.
[49] Pavel Panchekha, Adam T. Geller, Michael D. Ernst, Zachary Tatlock, and Shoaib Kamil. Verifying thatweb pages have accessible layout. In Proceedings of the 39th ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18-22, 2018, pages 1–14,
2018.
[50] Pavel Panchekha and Emina Torlak. Automated reasoning for web page layout. In Proceedings of the 2016
ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2016, part of SPLASH 2016, Amsterdam, The Netherlands, October 30 - November 4,
2016, pages 181–194, 2016.
[51] Jakub Pawlowicz. clean-css. https://github.com/jakubpawlowicz/clean-css, 2017. Referred in August 2017.
[52] René Peeters. The maximum edge biclique problem is np-complete. Discrete Applied Mathematics,
131(3):651–654, 2003.
[53] Justyna Petke. Bridging Constraint Satisfaction and Boolean Satisfiability. Artificial Intelligence: Foundations, Theory, and Algorithms. Springer, 2015.
[54] Armin Rigo and Contributors. Pypy. http://pypy.org/, 2007. Referred in August 2017.
[55] B. Scarpellini. Complexity of subcases of presburger arithmetic. Trans. of AMS, 284(1):203–218, 1984.
[56] M. Schäfer, M. Sridharan, J. Dolby, and F. Tip. Dynamic determinacy analysis. In PLDI, pages 165–174,
2013.
[57] Helmut Seidl, Thomas Schwentick, Anca Muscholl, and Peter Habermehl. Counting in trees for free. In
Automata, Languages and Programming: 31st International Colloquium, ICALP 2004, Turku, Finland, July
12-16, 2004. Proceedings, pages 1136–1149, 2004.
[58] Alexis Sellier and Contributors. Less. http://lesscss.org/, 2009. Referred in August 2017.
[59] Thomas Sha and Contributors. Yui compressor. http://yui.github.io/yuicompressor/, 2014. Referred August
2017.
[60] Slant.
Eight best css minifiers as of 2017.
https://www.slant.co/topics/261/~best-css-minifiers, 2017. Referred in April 2017.
[61] Jennifer Slegg. Google mobile first index: Page speed included as a ranking factor. The SEM Post, March
2017.
[62] Steve Souders. High Performance Web Sites: Essential Knowledge for Front-End Engineers. O’Reilly Media,
2007.
[63] M. Sridharan, J. Dolby, S. Chandra, M. Schäfer, and F. Tip. Correlation tracking for points-to analysis of
JavaScript. In ECOOP, pages 435–458, 2012.
[64] Friedrich Steimann. Constraint-based refactoring. ACM Trans. Program. Lang. Syst., 40(1):2:1–2:40, 2018.
[65] Larry J. Stockmeyer and Albert R. Meyer. Word problems requiring exponential time: Preliminary report.
In Proceedings of the 5th Annual ACM Symposium on Theory of Computing, April 30 - May 2, 1973, Austin,
Texas, USA, pages 1–9, 1973.
[66] Balder ten Cate, Tadeusz Litak, and Maarten Marx. Complete axiomatizations for XPath fragments. J. Applied
Logic, 8(2):153–172, 2010.
[67] Balder ten Cate and Maarten Marx. Navigational XPath: calculus and algebra. SIGMOD Record, 36(2):19–26,
2007.

54

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong[68] Balder ten Cate and Maarten Marx. Axiomatizing the logical core of XPath 2.0. Theory Comput. Syst.,
44(4):561–589, 2009.
[69] Frank Tip, Robert M. Fuhrer, Adam Kiezun, Michael D. Ernst, Ittai Balaban, and Bjorn De Sutter. Refactoring
using type constraints. ACM Trans. Program. Lang. Syst., 33(3):9:1–9:47, 2011.
[70] Unicode, Inc.
The unicode standard, version 9.0.
http://www.unicode.org/versions/Unicode9.0.0, 2016. Referred in August 2017.
[71] Moshe Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency Structure versus Automata (8th Banff Higher Order Workshop, August 27 - September 3, 1995, Proceedings),
pages 238–266, 1995.
[72] Mihalis Yannakakis. Node- and edge-deletion np-complete problems. In Proceedings of the 10th Annual ACM
Symposium on Theory of Computing, May 1-3, 1978, San Diego, California, USA, pages 253–264, 1978.

Appendix
A Additional Material for Max-SAT Encoding
Recall, given a valid covering C = {B i }m
i=1 of a CSS graph G, we aim to find a rule B = (X, Y ) and aposition j that minimises the weight of C[B → j]↓ .
In this section we give material omitted from Section 7. We begin with a definition of orderability
that will be useful for the remainder of the section. Then we will discuss how to produce the pair({Mi }µi=1 , F). Finally we will show that our encoding is correct.

A.1

Orderable Bicliques

To insert a biclique B = (X, Y ) into the covering, we need to make sure the order of its edges respects
the edge order. We can only order the edges by ordering the properties in the biclique. More precisely,
if we insert the biclique at position j, we need all edges in B that do not appear later in the file (i.e.
in {B i }m
i=j+1 ) to respect the edge order. This is because it is only the last occurrence of an edge that
influences the semantics of the stylesheet. Thus, let
EjB = {e ∈ B | index(e) ≤ j} .
The edge ordering implies a required ordering of EjB , which implies an ordering on the properties in Y .
This ordering is defined as follows. For all p1 , p2 ∈ Y we haveB∗
p 1 ≪Bj p2 ⇔ ∃(s1 , p1 ), (s2 , p2 ) ∈ Ej . (s1 , p1 ) ≺ (s2 , p2 ) .

That is, we require p1 to appear before p2 if there are two edges (s1 , p1 ) and (s2 , p2 ) in B that must beordered according to the transitive closure of ≺. A biclique is orderable iff its properties can be orderedin such a way to respect ≪B
j .
Definition A.1 (Orderable Bicliques). The biclique B is orderable at j if ≪B
j is acyclic. That is, there(sdoes not exist a sequence (s1 , p1 ), . . . , (sn , pn ) such that (si , pi ) ≪M
i+1 , pi+1 ) for all 1 ≤ i < njand (s1 , p1 ) = (sn , pn ).
This can be easily checked in polynomial time. Moreover, if a biclique is orderable at a given
position, a suitable ordering can be found by computing ≪Bj , also in polynomial time. Thus, this proves
Proposition 7.1.
55

CSS Minification via Constraint Solving

A.2

M. Hague, A. W. Lin, and C.-H. Hong

Enumerating Maximal Rules

Fix a covering C = {B i }m
i=1 of a CSS graph G = (S, P, E, ≺, wt). We show how to efficiently create
the pair ({Mi }µi=1 , F). In fact, we will create the pair ({Mi }µi=1 , F 1st ) where F 1st (j) is set of Mi forwhich j is the smallest position such that Mi is unorderable at position j. Computing F from this isstraightforward (though unnecessary since our encoding uses F 1st directly).
Our algorithm begins with an enumeration of the maximal bicliques that are orderable at position
0, and iterates up to position m, extending the enumeration at each step and recording in F 1st which
maximal bicliques become unorderable at each position. In fact, we will construct a pair (M, F 1st )where M is a set of bicliques rather than a sequence. To construct a sequence we apply any ordering to
the elements of M.
A.2.1

Initialisation

At position 0, all maximal bicliques (X, Y ) with X × Y ⊆ E are orderable. This is because all edges
appearing in (X, Y ) also appear in {B i }m
i=1 , hence, the semantics of C[B → 0] will be decided by edges
already in C, and thus the ordering of the properties does not matter. Hence, we begin with a set of all
maximal bicliques M0 . That is, all bicliques (X, Y ) such that X × Y ⊆ E where there is no (X ′ , Y ′ )with X ′ × Y ′ ⊆ E and X × Y ⊂ X ′ × Y ′ . Algorithms for generating such an enumeration are known.
For example, we use the algorithm from Kayaaslan [36].
For an initial value F01st of F 1st , we can simply take the empty function ∅.
A.2.2

Iteration

1stAssume we have generated (Mj , Fj1st ). We show how to generate the extension (Mj+1 , Fj+1).
The idea is to find all elements of Mj that are not orderable at position j + 1. Let χ be this set. We
first define
1st
Fj+1= Fj1st ∪ {(j + 1, χ)} .

Then, for each biclique M ∈ χ, we search for smaller bicliques contained within M that are maximal
µj+1
µj+1
1st
and orderable at position j + 1. This results in the extension {Mi }i=1
giving us ({Mi }i=1
, Fj+1).
Thus, the problem reduces to finding bicliques contained within some M that are maximal andorderable at position j + 1. We describe a simple algorithm for this in the next section.
A.2.3

Algorithm for (M, F 1st )We write Orderable(M, j) to assert that a biclique M is orderable at position j. For now, assume wehave the subroutine OrderableSub(M, j) which returns a set M′ of all orderable maximal bicliques at
position j contained within M . We use the following algorithm to generate (M, F 1st ).
M := M0
F 1st := ∅for j := 1 to m do
χ := ∅
for all M ∈ M do
if ¬Orderable(M, j) then
χ := χ ∪ {M }M := M ∪ OrderableSub(M, j)
end ifend forF 1st := F 1st ∪ {(j + 1, χ)}
56

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongend forreturn (M, F 1st )Note, we can improve the algorithm by restricting the nested for all loop over elements M ∈ M to
only those M that are not orderable at m. This is because an ordering at position m is also an ordering
at position j <= m. Hence, these bicliques will never be unorderable and do not need to be checked
repeatedly.
A.2.4

Generating Orderable Sub-Bicliques

We now give an algorithm for implementing the subroutine OrderableSub(M, j). Naively we can simply generate all sub-bicliques M ′ of M and check Orderable(M ′ , j). However, to avoid the potentiallyhigh cost of such an iteration, we first determine which selectors and properties contribute to ≪M
j . Removing nodes outside of these sets will not affect the orderability, hence we do not need to try removing
them. Then we first attempt only removing one node from this set, computing all sub-bicliques that have
one fewer element and are orderable. Then, for all nodes for which this fails, we attempt to remove two
nodes, and so on. Note, if removing node w renders M orderable, we do not need to test any bicliques
obtained by removing w and some other node w′ , since this will not result in a maximal biclique.
Hence, we define the sets of candidate selectors and properties that may be removed to restore
orderability. These are all selectors and nodes that contribute to ≪M
j . That is{}∆ = s1 , s2 , p1 , p2 ∃(s1 , p1 ), (s2 , p2 ) ∈ EjM . (s1 , p1 ) ≺∗ (s2 , p2 ) .
We define OrderableSub(M, j) = OrderableSub(M, j, ∆) where OrderableSub(M, j, ∆) generates
a set Ω of orderable sub-bicliques and is defined below. When M = (X, Y ) we will abuse notation andwrite M \ {w} for (X \ {w} , Y ) when w is a selector, and (X, Y \ {w}) when w is a property. Whendefining the algorithm, we will collect all orderable bicliques in a set Ω. We will further collect in ∆′the set of all nodes which fail to create an orderable biclique when removed by themselves. We define
OrderableSub(M, j, ∆) recursively, where the recursive call attempts the removal of an increasing
number of nodes. It isΩ := ∅∆′ := ∅
for all w ∈ ∆ do
M ′ := M \ {w}if Orderable(M ′ , j) then
Ω := Ω ∪ {M ′ }else∆′ := ∆′ ∪ {w}end ifend forfor all w ∈ ∆′ doΩ := Ω ∪ OrderableSub(M \ {w} , j, ∆′ \ {w})end forreturn Ω

A.3

Correctness of the Encoding

We argue Proposition 7.3 which claims that the encoding (ΠH , ΠS ) is correct. To prove this we need toestablish three facts.
57

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

1. If (B, j) is a valid merging opportunity of C and B = (B, ◁) , then (B, j) is a solution to thehard constraints.
2. If (B, j) is generated from a solution to the hard constraints, it is a valid merging opportunity.
3. The weight of a solution generating (B, j) is the size of C[B → j]↓ .
We argue these properties below.
1. Take a valid merging opportunity (B, j) and let B = (B, ◁). We construct a solution to the hardconstraints. First, we assign j = j. Next, since the merging opportunity is valid, we know B
contains only edges in E. That is, it is contained within a maximal biclique. Furthermore, sinceC[B → j] is valid, we know that B is orderable at position j. Thus, it is a sub biclique of some
Mi in ({Mi }µi=1 , F 1st ), and, moreover, it is not the case that Mi ∈ F 1st (j ′ ) for some j ′ ≤ j.
Thus, we assign iM = i and we know that


∧
∧
(
)
(
)
 j >= j ⇒iM ̸= i 1≤j≤m+1

Mi ∈F 1st (j)is satisfied.
Additionally, for all w appearing in B but not in Mi , we set xρi (w) to false, otherwise we set it totrue. Thus HasEdge((s, p)) holds only if (s, p) is an edge in B.
Next, we argue∧(s1 ,p1 )≺(s2 ,p2 )HasEdge((s
,
p
))
⇒
1
1
) 
(
j ≤ index((s2 , p2 )) ∨ HasEdge((s2 , p2 ))is satisfied. This follows from C[B → j] being valid. To see this, take some (s1 , p1 ) ≺ (s2 , p2 ).
If (s1 , p1 ) does not appear in B, then there is nothing to prove. If it does, we know (s2 , p2 ) must
appear later in the file. There are two cases. If j ≤ index((s2 , p2 )) then the clause is satisfied.
Otherwise we must have (s2 , p2 ) in B or edge order would be violated. Thus the clause also holds
in this case.
2. We need to prove that if the hard constraints are satisfied, then then generated merging opportunity(B, j) is valid. Let B = (B, ◁). For C[B → j] to be valid, we first have to show that B
introduces no new edges to the stylesheet. This is immediate since B is a sub biclique of some
Mi in ({Mi }µi=1 , F 1st ), which can only contain edges in E.
Next, we need to argue that we can create the ordering ◁ for the properties in B. First note that
Mi is orderable at position j. In particular, for any (s1 , p1 ) ≺∗ (s2 , p2 ) with (s1 , p1 ) and (s2 , p2 )i
p2 . Since all edges in B also appear in Mi , the existence ofappearing in Mi , we have p1 ≪Mjan ordering is immediate.
Finally, we need to argue that C[B → j] respects the edge order. Suppose (s1 , p2 ) ≺ (s2 , p2 ). To
violate this ordering, we need to introduce a copy of (s1 , p1 ) after the last copy of (s2 , p2 ). Thus,
we must have (s1 , p1 ) in B. However, from
∧
HasEdge((s
,
p
))
⇒
1 1
) 
(

j ≤ index((s2 , p2 )) ∨ HasEdge((s2 , p2 ))(s1 ,p1 )≺(s2 ,p2 )58

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

we are left with two cases. In the first j ≤ index((s2 , p2 )) and the edge order is maintained.
In the second, we also have (s2 , p2 ) in B. However, the edge order is maintained because B isorderable. Thus we are done.
3. Finally, we argue that the weight of a satisfying assignment accurately reflects the size of C[B → j]↓ .
This is fairly straightforward. The size of C[B → j]↓ . comprises two parts: the size of B, and thesize of C after the trim operation. It is immediate to see that the size of B is equal to the size ofall of its nodes. In particular, this is the size of all nodes of Mi that appear in B. That is, have notbeen excluded. Thus the clause with weight wt(w)()
iM = i ⇒ xρi (w) .
for each w appearing in Mi accurately computes the size of B.
For the size of C after the trim operation, we first use the assumption that C has already been
trimmed before applying the merging opportunity. Thus, any further nodes removed in C[B → j]↓from a rule B i′ must be removed because some edge e in B also appears in B i′ and, moreover, it
was the case i′ = index(e) and i′ ≤ j. In particular, we can only remove a node w from B i′ if
all edges e incident to w with i′ = index(e) have e appearing in B (else there will still be someedge preventing w from being trimmed after applying the merging opportunity). Thus, for eachselector node s, we know it is not removed if the clause with weigth wt(s)∧i≤j∧HasEdge((s, p))index((s,p))=ip∈Y

is not satisfied. Similarly for property nodes p. Thus, these clauses accurately count the size ofthe covering after trimming.

B

Additional Material for Section 5

B.1

Handling Pseudo-Elements

CSS selectors can also finish with a pseudo-element. For example φ ::before. These match nodes
that are not formally part of a document tree. In the case of φ ::before the selector matches aphantom node appearing before the node matched by φ. These can be used to insert content into thetree for stylistic purposes. For example.a::before { content:">" }places a “>” symbol before the rendering of any node with class a.
We divide CSS selectors into five different types depending on the pseudo-element appearing at theend of the selector. We are interested here in the nodes matched by a selector. The pseudo-elements::first-line, ::first-letter, ::before, and ::after essentially match nodes inserted
into the DOM tree. The CCS3 specification outlines how these nodes should be created. For our
purposes we only need to know that the five syntactic cases in the above grammar can never match thesame inserted node, and the selectors ::first-letter and ::first-line require that the nodematched by φ is not empty.
Since we are interested here in the non-emptiness and non-emptiness-of-intersection problems, wewill omit pseudo-elements in the remainder of this article, under the assumptions that
59

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong• selectors of the form φ ::first-line or φ ::first-letter are replaced by a selector
φ :not(:empty), and• selectors of the form φ, φ ::before, or φ ::after are replaced by φ, and• we never take the intersection of two selectors φ and φ′ such that it’s not the case that either– φ and φ′ were derived from selectors containing no pseudo-elements, or– φ and φ′ were derived from selectors ending with the same pseudo-element.
In this way, we can test non-emptiness of a selector by testing its replacement. For non-emptiness-ofintersection, we know if two selectors end with different pseudo-elements (or one does not contain apseudo-element, and one does), their intersection is necessarily empty. Thus, to check non-emptinessof-intersection, we immediately return “empty” for any two selectors ending with different pseudoelements. To check two selectors ending with the same pseudo-element, the problem reduces to testing
the intersection of their replacements.

B.2

NP-hardness of Theorem 5.2

Lemma B.1. Given a CSS selector φ, deciding ∃T, η . T, η |= φ is NP-hard.
Proof. We give a polynomial-time reduction from the NP-complete problem of non-universality ofunions of arithmetic progressions [65, Proof of Theorem 6.1]. To define this, we first fix some notation. Given a pair (α, β) ∈ N × N, we define [[(α, β)]] to be the set of natural numbers of the form
αn + β for n ∈ N. That is, [[(α, β)]] represents an arithmetic progression, where α represents theperiod ∪and β represents the offset. Let E ⊆ N × N be a finite subset of pairs (α, β). We define[[E]] = (α,β)∈E [[(α, β)]]. The NP-complete problem is: given E (where numbers may be represented
in unary or in binary representation), is [[E]] ̸= N? Observe that this problem is equivalent to checking
whether [[E +1]] ̸= N>0 where E +1 is defined by adding 1 to the offset β of each arithmetic progression(α, β) in E. By complementation,
this last problem is equivalent to checking whether N>0 \[[E+1]] ̸= ∅.
∩Since N>0 \ [[E + 1]] = (α,β)∈E [[α, β + 1]], the problem can be seen to be equivalent to testing thenon-emptiness of* {:not(:nth-child(αn + (β + 1))) | (α, β) ∈ E} .
Thus, non-emptiness is NP-hard.

B.3

Handling !important and shorthand property names

Our approach handles the !important keyword and shorthand property names. In this section we explain
the steps we take to account for them.
B.3.1

The !important Keyword

First, the keyword !important in property declaration as is used in the rulediv { color:red !important }can be used to override the cascading behaviour of CSS, e.g., in our example, if a node is matchedby div, as well as a later rule R that assigns a different color, then assign red to color (unless R
also has the keyword !important next to its color property declaration). To handle this, we can60

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongextend the notion of specificity of a selector to the notion of specificity of a pair (s, p) of selector andproperty declaration, after which we may proceed as before (i.e. relating only two edges with the same
specificity). Recall from [15] that the specificity of a selector is a 3-tuple (a, b, c) ∈ N × N × N wherea, b, and c can be obtained by calculating the sum of the number of IDs, classes, tag names, etc. in theselector. Since the lexicographic order is used to rank the elements of S := N × N × N, the specificity
of a pair (s, p) can now be defined to be (i, a, b, c), where (a, b, c) is the specificity of s, and i = 1
if !important can be found in p (otherwise, i = 0). In particular, this also handles the case wheremultiple occurrences of !important is found in the CSS file.
B.3.2

Shorthand Property Names

Shorthand property names [10] can be used to simultaneously set the values of related property names.
For example, border: 5px solid red is equivalent toborder-width: 5px; border-style: solid; border-color:red
In particular, this implies that (s, p) and (s, p′ ) can be related in ≺ if p defines border, while the otherproperty p′ defines border-width. One way to achieve this is to simply list all pairs of comparable
property names, which can be done since only around 100 property names are currently officially related.
[Incidentally, a close enough approximation is that one property name is a prefix of the other property
name (e.g., border is a prefix of border-style), but this is not complete (e.g. font can be used
to define line-height)]

C Additional Material for Section 6
C.1

Correctness of Aφ in Proposition 6.1

We show both soundness and completeness of Aφ .
Lemma C.1. For each CSS selector φ and tree T , we have(T, η) ∈ L(Aφ ) ⇒ T, η |= φ .
Proof. Suppose (T, η) ∈ L(Aφ ). By construction of Aφ we know that the accepting run must passthrough all states ◦1 , . . . , ◦n where φ = σ1 o1 · · · on−1 σn . Notice, in order to exit each state ◦i atransition labelled by σi must be taken. Let ηi be the node read by this transition, which necessarily
satisfies σi . Observe ηn = η. We proceed by induction. We have η1 satisfies σ1 . Hence, assume ηisatisfies σ1 o1 · · · oi−1 σi . We show ηi+1 satisfies σ1 o1 · · · oi σi+1 .
We case split on oi .
• When oi = >> we need to show ηi+1 is a descendant of ηi . By construction of Aφ the run reaches↓

ηi+1 in one of two ways. If it is via a single transition ◦i −→ ◦i+1 then ηi+1 is immediately aσi↓descendant of ηi . Otherwise the first transition is ◦i −→ •i . The reached node is necessarily aσidescendant of ηi . To reach ηi+1 a path is followed applying →+ and ↓ arbitrarily, which cannot
reach a node that is not a descendant of ηi . Finally, the transition to ηi+1 is via → or ↓ and henceηi+1 must also be a descendant of ηi .
• When oi = > we need to show ηi+1 is a descendant of ηi . By construction of Aφ the run reaches↓

ηi+1 in one of two ways. If it is via a single transition ◦i −→ ◦i+1 then ηi+1 is immediately aσi61CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong↓child of ηi . Otherwise the first transition is ◦i −→ •i . The reached node is necessarily a child of
σi

ηi . To reach ηi+1 only transitions labelled →+ and → can be followed. Hence, the node reachedmust also be a child of ηi .
• When oi = + we need to show ηi+1 is the next neighbour of ηi . Since the only path is a single
transition labelled → the result is immediate.
• When oi = ˜ we need to show ηi+1 is a sibling of ηi . By construction of Aφ the run reaches ηi+1→
in one of two ways. If it is via a single transition ◦i −→ ◦i+1 then ηi+1 is immediately a sibling ofσi→

ηi . Otherwise the first transition is ◦i −→ •i . The reached node is necessarily a sibling of ηi . To
σireach ηi+1 only transitions labelled →+ and → can be followed. Hence, the node reached mustalso be a sibling of ηi .
Thus, by induction, ηn = η satisfies σ1 o1 · · · on−1 σn = φ.
Lemma C.2. For each CSS selector φ and tree T , we haveT, η |= φ ⇒ (T, η) ∈ L(Aφ )Proof. Assume T, η |= φ. Thus, since φ = σ1 o1 · · · on−1 σn , we have a sequence of nodes η1 , . . . , ηnsuch that for each i we have T, ηi |= σ1 o1 · · · oi−1 σi . Note ηn = η. We build a run of Aφ from σ1
to ◦i by induction. When i = 1 we have the run constructed by taking the loops on the initial state ◦1labelled ↓ and →+ to navigate to η1 . Assume we have a run to ◦i . We build a run to ◦i+1 we consideroi .
• When oi = >> we know ηi+1 is a descendant of ηi . We consider the construction of Aφ . If ηi+1↓

is the first child of ηi , we construct the run to ◦i+1 via the transition ◦i −→ ◦i+1 , noting that we
σi↓know ηi satisfies σi . Otherwise we take ◦i −→ •i and arrive at either an ancestor or sibling of
σi

ηi+1 . In the case of a neighbour, we can take the transition labelled → to reach ηi+1 . For an
indirect sibling we can take the transition labelled →+ followed by the transition labelled →. For
an ancestor, we take the transition labelled ↓ and arrive at another sibling or ancestor of ηi+1 thatis closer. We continue in this way until we reach ηi+1 as needed.
• When oi = > we know ηi+1 is a child of ηi . We consider the construction of Aφ . If ηi+1 is the↓first child of ηi , we construct the run to ◦i+1 via the transition ◦i −→ ◦i+1 , noting that we knowσi↓

ηi satisfies σi . Otherwise we take ◦i −→ •i and arrive at a preceding sibling of ηi+1 . We canσitake the transition labelled →+ to reach the preceding neighbour of ηi+1 if required, and then thetransition labelled → to reach ηi+1 as required.
• When oi = + we know ηi+1 is the neighbour of ηi . We consider the construction of Aφ and take→the only available transition ◦i −→ ◦i+1 , noting that we know ηi satisfies σi . Thus, we reach ηi+1
σi

as required.
• When oi = ˜ we know ηi+1 is a sibling of ηi . We consider the construction of Aφ . If ηi+1 is the↓neighbour of ηi , we construct the run to ◦i+1 via the transition ◦i −→ ◦i+1 , noting that we know→σi

ηi satisfies σi . Otherwise we take ◦i −→ •i and arrive at a preceding sibling of ηi+1 . We canσi62CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hongtake the transition labelled →+ to reach the preceding neighbour of ηi+1 is required, and then thetransition labelled → to reach ηi+1 as required.
Thus, by induction, we construct a run to ηn ending in state ◦n . We transform this to an accepting run◦
by taking the transition ◦n −−→ qf , using the fact that ηn satisfies σn .
σnC.2

Proof of Proposition 6.2

We show that(T, η) ∈ L(A1 ) ∧ (T, η) ∈ L(A2 ) ⇔ (T, η) ∈ L(A1 ∩ A2 ) .
We begin by observing that that all runs of a CSS automaton showing acceptance of a node η in T
must follow a sequence of nodes η1 , . . . , ηn such that• η1 is the root of T , and• when ηj = η ′ ι then either ηj+1 = η ′ (ι + 1) or ηj+1 = ηj 1 for all j, and• ηn = ηthat defines the path taken by the automaton. Each node is “read” by some transition on each run. Notea transition labelled →+ may read sequence nodes that is a factor of the path above. However, sincethese transitions are loops that do not check the nodes, without loss of generality we can assume each→+ in fact reads only a single node. That is, →+ behaves like →. Recall, →+ was only introduced toensure the existence of “short” runs.
Because of the above, any two runs accepting η in T must follow the same sequence of nodes andbe of the same length.
We have (T, η) ∈ L(A1 ) ∧ (T, η) ∈ L(A2 ) iff there are accepting runs
di

di

σ1

σn

1
n
i
q1i −→· · · −−→
qn+1ii

of Ai over T reaching node η for both i ∈ {1, 2}. We argue these two runs exist iff we have a run( 1 2 ) d1)
dn ( 12
qn+1 , qn+1
q1 , q1 −→ · · · −−→
σ1

σn

(
)
of A1 ∩ A2 where each dj and σj depends on d1j , d2j .
• When (↓, ↓) we have dj =↓ and σj = σj1 ∩ σj2 .
• When (→, →) we have dj =→ and σj = σj1 ∩ σj2 .
• When (→, →+ ) we have dj =→ and σj = σj1 .
• When (→+ , →) we have dj =→ and σj = σj2 .
• When (→+ , →+ ) we have dj =→+ and σj = *.
• When (◦, ◦) we have dj = ◦ and σj = σj1 ∩ σj2 .
• The cases (↓, →+ ), (↓, →), (↓, ◦), (→, ↓), (→, ◦), (→+ , ↓), (→+ , ◦), (◦, ↓), (◦, →), and (◦, →+ )are not possible.
63

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

The existence of the transitions comes from the definition of A1 ∩ A2 . We have to argue that ηj satisfies
both σji iff it also satisfies σj . By observing σ ∩ * = * ∩ σ = σ we always have σj = σj1 ∩ σj2 .
Let σji = τi Θi and σj = τ Θ. It is immediate that ηj satisfies Θ = Θ1 ∪ Θ2 iff it satisfies both Θi .
To complete the proof we need to show ηj satisfies τ iff it satisfies both τi . Note, we must havesome s and e such that τ, τ1 , τ2 ∈ {*, (s|*), (s|e), e} else the type selectors cannot be satisfied(either τ = :not(*) or τ1 and τ2 assert conflicting namespaces or elements).
If some τi = * the property follows by definition. Otherwise, if τ = τ2 then in all cases the
conjunction of τ1 and τ2 is equivalent to τ2 and we are done. The situation is similar when τ = τ1 .
Otherwise τ = (s|e) and τ1 = (s|*) and τ2 = e or vice versa, and it is easy to see τ is equivalent to
the intersection of τ1 and τ2 . Thus, we are done.

C.3

Proofs for Non-Emptiness of CSS Automata

C.3.1

Bounding Namespaces and Elements

We show Proposition 6.4 (Bounded Types). We need to define the finite sets ⇃(E LE) and ⇃(s). To thisend, we writed1. E LEA to denote the set of namespaced elements s:e such that there is some transition q −→ q′ ∈ ∆σwith σ = (s|e)Θ for some s, e, and Θ,d2. SA is the set of transitions q −→ q ′ ∈ ∆ with σ ̸= * and |A|σ denotes the cardinality of SA .
σ{}
Let τ1 , . . . , τ|A|σ be a set of fresh namespaced elements and{}⇃(E LEA ) = E LEA ⊎ τ1 , . . . , τ|A|σ ⊎ {⊥}{}where there is a bijection θ : SA → τ1 , . . . , τ|A|σ such that for each t ∈ SA we have θ(t) = τ and1. τ = s:e if σ can only match elements s:e,
2. τ = s:e for some fresh element e if σ can only match elements of the form s:e′ for all elements
e′ , and3. τ = s:e for some fresh namespace s if σ can only match elements of the form s′ :e for all namespaces s′ , and4. τ = s:e for fresh s and fresh e if σ places no restrictions on the element type.
Thus, we can define bounded sets of namespaces and elements⇃(E LE) = {e | ∃s . s:e ∈ ⇃(E LEA )}⇃(NS) = {s | ∃e . s:e ∈ ⇃(E LEA )} .
It remains to show ⇃(E LEA ) is sufficient. That is, if some tree T is accepted A, we can define anothertree T ′ that also is accepted by A but only uses types in ⇃(E LEA ).
We take (T, η) ∈ L(A) with T = (D, λ) and we define T ′ = (D, λ′ ) satisfying the proposition. Let
q0 , η0 , q1 , η1 , . . . , qℓ , ηℓ , qℓ+1
be the accepting run of A, by the sequence of transitions t0 , . {. . , tℓ . As noted} above, we can assume
each transition in ∆ appears only once in this sequence. Let σ1 , . . . , σ|A|σ be the set of selectors
appearing in A. We perform the following modifications to λ to obtain λ′ .
64

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

We obtain λ′ from λ by changing the element labelling. We first consider all 0 ≤ i ≤ ℓ such that ηiis labelled by some element s:e ∈ E LEA . Let Nodes s:e be the set of nodes labelled by s:e in λ. In λ′we label all nodes in Nodes s:e by s:e. That is, we do not relabel nodes labelled by s:e. Let Nodes be
the union of all such Nodes s:e .
Next we consider all 0 ≤ i ≤ ℓ such that ηi ∈/ Nodes (i.e. was not labelled in the previous case) anddti = q i −→ qi+1 with σ ̸= *. Let s:e ∈/ E LEA be the element labelling of ηi in λ. Moreover, take τ suchσthat θ(ti ) = τ . In λ′ we label all nodes in Nodes s:e (i.e. labelled by s:e) in λ by τ . That is, we globally
replace s:e by τ . Let Nodes ′ be Nodes union all such Nodes e .
Finally, we label all nodes not in Nodes ′ with the null element ⊥.
To see that
q0 , η0 , q1 , η1 , . . . , qℓ , ηℓ , qℓ+1d

via t0 , . . . , tℓ is an accepting run of (D, λ′ ) we only need to show that for each ti = qi −→ qi+1 thatσηi satisfies σ. This can be shown by induction over σ. Most atomic cases are straightforward (e.g.
the truth of :hover is not affected by our transformations). The case of e, (s|*), or (s|e) appearing positively follows since in these cases the labelling remained the same or changed to someτ consistent with the selector. When such selectors appear negatively, the result follows since weonly changed elements and namespaces to fresh ones. The truth of attribute selectors remains unchanged since we did not change the attribute labelling. The cases of :nth-child(αn + β) and:nth-last-child(αn + β) follow since we did not change the number of nodes. For the selectors :nth-of-type(αn + β) and :nth-last-of-type(αn + β) there are two cases. If
we did not change the element label s:e of ηi , then we also did not change the label of its siblings.
Moreover, we did not add any s:e labels elsewhere in the tree. Hence the truth of the formulas remains
the same. If we did change the label from s:e to τ for some τ then observe that we also relabelled allother nodes in the tree labelled by s:e. In particular, all siblings of ηi . Moreover, since θ is a bijectionand each transition appears only once in the run, we did not label any node not labelled s:e with τ .
Hence the truth of the formulas also remains the same. Similar arguments hold for :only-child and:only-of-type.
Thus, (D, λ′ ) is accepted, and only uses elements in ⇃(E LEA ) as required.

C.3.2

Proof of Polynomial Bound on Attribute Value Lengths

We prove Proposition 6.5 (Bounded Attributes). That is we argue the existence of a polynomial boundfor the solutions to any finite set C of constraints of the form [s|a op v] or :not([s|a op v]), forsome fixed s and a. We say that C is a set of constraints over s and a.
In fact, the situation is a little more complicated because it may be the case that a is id. In thiscase we need to be able to enforce a global uniqueness constraint on the attribute values. Thus, forconstraints on an ID attribute, we need a bound that is large enough to allow to all constraints on
the same ID appearing throughout the automaton to be satisfied by unique values. Thus, for a given
automaton, we might ask for a bound N such that if there exists unique ID values for each transition,then there exist values of length bounded by N .
However, the bound on the length must still work when we account for the fact that not all transitionsin the automaton will be used during a run. Consider the following illustrative example.
65

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong→q in[s|id = v]
↓

q

◦

qf

*

[s|id = v]

In this case we have two transitions with ID constraints, and hence two sets of constraints C1 = C2 ={[s|id = v]}. Since these two sets of constraints cannot be satisfied simultaneously with uniquevalues, even the bound N = 0 will satisfy our naive formulation of the required property (since theproperty had the existence of a solution as an antecedent). However, it is easy to see that any run of theautomaton does not use both sets of constraints, and that the bound N = |v| should suffice. Hence, we
formulate the property of our bound to hold for all sub-collections of the collection of sets of constraints
appearing in the automaton.
Lemma C.3 (Bounded Attribute Values). Given a collection of constraints C1 , . . . , Cn over some sand a, there exists a bound N polynomial in the size of C1 , . . . , Cn such that for any subsequence
Ci1 , . . . , Cim if there is a sequence of words v1 , . . . , vm such that all vj are unique and vj satisfies theconstraints in Cij , then there is a sequence of words such that the length of each vj is bounded by N ,all vj are unique, and vj satisfies the constraints in Cij ,The proof uses ideas from Muscholl and Walukiewicz’s NP fragment of LTL [45]. We first, foreach set of constraints C, construct a deterministic finite word automaton A that accepts only words
satisfying all constraints in C. This automaton has a polynomial number of states and can easily be seen
to have a short solution by a standard pumping argument. Given automata A1 , . . . , An with at mostNs states and Nc constraints in each set of constraints, we can again use pumping to show there is asequence of distinct words v1 , . . . , vn such that each vi is accepted by Ai and the length of vi is at mostn · Ns · Nc .
The Automata We define a type of word automata based on a model by Muscholl and Walukiewicz
to show and NP upper bound for a variant of LTL. These automata read words and keep track of whichconstraints in C have been satisfied or violated. They accept once all positive constraints have beensatisfied and no negative constraints have been observed.
In the following, let Prefs(C) be the set of words v ′ such that v ′ is a prefix of some v with[s|a op v] ∈ C or :not([s|a op v]) ∈ C. Moreover, let ˆ and $ be characters not in Γ thatwill mark the beginning and end of the word respectively. Additionally, let ε denote the empty word.
Finally, we write v ⪯ v ′ if v is a factor of v ′ , i.e., v ′ = v1 vv2 for some v1 and v2 .
Definition C.4 (AC ). Given a set C of constraints over s and a, we define AC = (Q, ∆, C) where• Q is the set of all words a1 va2 such that– v ∈ Prefs(C), and– a1 , a2 ∈ Γ ∪ {ε, ˆ, $}.
a• ∆ ⊆ Q × (Γ ∪ {ˆ, $}) × Q is the set of transitions v −→ v ′ where v ′ is the longest suffix of vasuch that v ′ ∈ Q.
66

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

Observe that the size of the automaton AC is polynomial in the size of C.
A run of AC over a word with beginning and end marked a1 . . . an ∈ ˆΓ∗ $ is
a

a

a

1
2
n
(v0 , S0 , V0 ) −→(v1 , S1 , V1 ) −→· · · −−→
(vn , Sn , Vn )aivi and Si , Vi ⊆ C track the satisfied and violated
where v0 = ε and for all 1 ≤ i ≤ n we have vi−1 −→constraints respectively. That is S0 = V0 = ∅, and for all 1 ≤ i ≤ n we have (noting ˆv ⪯ vi implies
ˆv is a prefix of vi , and similar for v$) Si =Si−1 ∪ {[s|a = v] ∈ C | ˆv$ = vi } ∪{[s|a ~= v] ∈ C | ∃a1 ∈ {ˆ, } , a2 ∈ { , $} . a1 va2 ⪯ vi } ∪{[s|a |= v] ∈ C | ∃a2 ∈ {$, -} . ˆva2 ⪯ vi } ∪{[s|a ^= v] ∈ C | ˆv ⪯ vi } ∪ {[s|a $= v] ∈ C | v$ ⪯ vi } ∪{[s|a *= v] ∈ C | v ⪯ vi }and Vi =Vi−1 ∪ {:not([s|a = v]) ∈ C | ˆv$ = vi } ∪}{a ∈ {ˆ, } ,. a1 va2 ⪯ vi ∪:not([s|a ~= v]) ∈ C ∃ 1
a2 ∈ { , $}{:not([s|a |= v]) ∈ C | ∃a2 ∈ {$, -} . ˆva2 ⪯ vi } ∪{:not([s|a ^= v]) ∈ C | ˆv ⪯ vi } ∪{:not([s|a $= v]) ∈ C | v$ ⪯ vi } ∪{:not([s|a *= v]) ∈ C | v ⪯ vi } .

Such a run is accepting if Sn = {[s|a op v] | [s|a op v] ∈ C} and Vn = ∅. That is, all positive
constraints have been satisfied and no negative constraints have been violated.
Short Solutions We show the existence of short solutions via the following lemma. The proof of thislemma is a simple pumping argument which appears below. Intuitively, if a satisfying word is shorter
than Ns · Nc we do not change it. If it is longer than Ns · Nc any accepting run of the automaton on thisword must contain a repeated (v, S, V ). We can thus pump down this word to ensure that it is shorter
than Ns · Nc . Then, to ensure it is unique, we pump it up to some unique length of at most n · Ns · Nc .
Lemma C.5 (Short Attribute Values). Given a sequence of sets of constraint automata AC1 , . . . , ACneach with at most Ns states and at most Nc constraints in each Ci , if there is a sequence of pairwise
unique words v1 , . . . , vn such that for all 1 ≤ i ≤ n there is an accepting run of ACi over vi , then there
exists such a sequence where the length of each vi is at most n · Ns · Nc .
To obtain Lemma C.3 (Bounded Attribute Values) we observe that for any subsequence Ci1 , . . . , Cim
we have m · Ns′ · Nc′ ≤ n · Ns · Nc since m ≤ n and the max number of states Ns′ and constraints Nc′ inthe subsequence have Ns′ ≤ Ns and Nc′ ≤ Nc .
We give the proof of Lemma C.5. That is, given a sequence of sets of constraint automata AC1 , . . . , ACneach with at most Ns states and at most Nc constraints in each Ci , if there is a sequence of pairwise
unique words v1 , . . . , vn such that for all 1 ≤ i ≤ n there is an accepting run of ACi over vi , then there
exists such a sequence where the length of each vi is at most n · Ns · Nc .
To prove the lemma, take a sequence v1 , . . . , vn such that each vi is unique and accepted by ACi .
We proceed by induction, constructing v1′ , . . . , vi′ such that each vj′ is unique, accepted by ACj , and oflength ℓ such that either• ℓ ≤ Ns · Nc and vj′ = vj , or
• i · Ns · Nc ≤ ℓ ≤ (i + 1) · Ns · Nc .
67

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

When i = 0 the result is vacuous. For the induction there are two cases.
When the length ℓ of vi is such that ℓ ≤ Ns · Nc we set vi′ = vi . We know vi′ is unique amongst′
v1 , . . . , vi′ since for all j < i either vj′ is longer than vi′ or is equal to vj and thus distinct from vi .
When ℓ > Ns · Nc we use a pumping argument to pick some vi′ of length ℓ′ such that i · Ns · Nc ≤′ℓ ≤ (i + 1) · Ns · Nc . This ensures that vi′ is unique since it is the only word whose length lies within
the bound. We take the accepting run
a

a

a

1
2
n
(u0 , S0 , V0 ) −→(u1 , S1 , V1 ) −→· · · −−→(uℓ , Sn , Vℓ )of vi and observe that the values of Sj and Vj are increasing by definition. That is Sj ⊆ Sj+1 andVj ⊆ Vj+1 . By a standard down pumping argument, we can construct a short accepting run containing
only distinct configurations of length bound by Ns · Nc . We construct this run by removing all cycles
from the original run. This maintains the acceptance condition. Next we obtain an accepted word oflength i · Ns · Nc ≤ ℓ′ ≤ (i + 1) · Ns · Nc . Since ℓ > Ns · Nc we know there exists at least one
configuration (u, S, V ) in the short run that appeared twice in the original run. Thus there is a run of theautomaton from (u, S, V ) back to (u, S, V ) which can be bounded by Ns · Nc by the same downward
pumping argument as before. Thus, we insert this run into the short run the required number of times toobtain an accepted word vi′ of the required length.
Thus, by induction, we are able to obtain the required short words v1′ , . . . , vn′ as needed.

C.3.3

Missing definitions for AttsPres(θ, ⃗x)s:a= aj ∧  xi,j
s:a

∧ 


xi,m+1 = 0





 



∨
1≤j≤m


s:a


x
=
i,m+1




∨


 
s:a


x
=
∧


∧ i,j−1
s:a
∨




x
=
a
∧
′
j
i,j+j

 

1≤j ′ ≤m)(1≤j≤N −m−1s:axs:ai,j+m+1 = 0 ∨ xi,j+m+1) =
(
∧
s:a
s:a
xs:a
i,j = aj ∧ xi,m+1 = 0 ∨ xi,m+1 = 1≤j≤m
∧
(
)
xs:a
∨
i,j+j ′ = aj ∧′

AttsPres([s|a ~= v], ⃗x)=

AttsPres([s|a |= v], ⃗x)=

AttsPres([s|a $= v], ⃗x) =0≤j≤N −m−1

C.3.4



1≤j ≤ms:axi,j+m+1=0

Negating Positional Formulas

We need to negate selectors like :nth-child(αn + β), For completeness, we give the definitionof the negation below.
We decompose β according to the period α. I.e. β = αβ1 + β2 , where β1 and β2 are the uniqueintegers such that |β2 | < |α| and β1 α < 0 implies β2 ≤ 0 and β1 α > 0 implies β2 ≥ 0.
Definition C.6 (NoMatch(x, α, β)). Given constants α, β, β1 , and β2 as above, we define the formula68

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

NoMatch(x, α, β) to be(0 ≥ α ∧ x < β) ∨ (0 ≤ α ∧ x > β) ∨′
β 2 < |α| ∧
)


 (

 β α < 0 ⇒ β ′ ≤ 0 ∧ 
1


 (
2
)
′ 


∃n . ∃β 2 .  β α > 0 ⇒ β ′ ≥ 0 ∧ 
1



2



′



β 2 ̸= β2 ∧′x = αn + αβ1 + β 2
In the following, whenever we negate a formula of the form ¬ (∃n.x = αn + β) we will use theformula NoMatch(x, α, β). One can verify that the resulting formula is existential Presburger. We
show that our negation of periodic constraints is correct.
Proposition C.7 (Correctness of NoMatch(x, α, β)). Given constants α and β, we have¬ (∃n.x = αn + β) ⇔ NoMatch(x, α, β) .
Proof. We first consider α = 0. Since there is no β2′ with |β2′ | < 0 we have to prove¬ (x = β) ⇔ (x < β) ∨ (x > β)which is immediate.
In all other cases, the conditions on β2 and β2′ ensure that we always have 0 < |β2 − β2′ | < |α|.
If ∃n.x = αn + αβ1 + β2 then if α > 0 it is easy to verify that we don’t have x < β (since n = 0
gives x = β as the smallest value of x) and similarly when α < 0 we don’t have x < β. To disprove
the final disjunct of of NoMatch(x, α, β) we observe there can be no n′ s.t. x = αn′ + αβ1 + β2′ sincex = αn + αβ1 + β2 and 0 < |β2 − β2′ | < |α|.
In the other direction, we have three cases depending on the satisfied disjunct of NoMatch(x, α, β).
Consider α > 0 and x < β. In this case there is no n such that x = αn + αβ1 + β2 = αn + β sincen = 0 gives the smallest value of x, which is β. The case is similar for the second disjunct with α < 0.
The final disjunct gives some n′ such that x = αn′ + αβ1 + β2′ with 0 < |β2 − β2′ | < |α|. Hence,
there can be no n with x = αn + αβ1 + β2 .
C.3.5

Correctness of Presburger Encoding

We prove soundness and completeness of the Presburger encoding of CSS automata non-emptiness inthe two lemmas below.
Lemma C.8. For a CSS automaton A, we have
L(A) ̸= ∅ ⇒ θA is satisfiable.
Proof. We take a run of A and construct a satisfying assignment to the variables in θA . That is take a
document tree T = (D, λ), node η ∈ D, and sequence∗q0 , η0 , q1 , η1 , . . . , qℓ , ηℓ , qℓ+1 ∈ (Q × D) × {qf }that is an accepting run. We know from Proposition 6.4 (Bounded Types) that T can only use namespaces from ⇃(NS) and elements from ⇃(E LE). Let t0 , . . . , tℓ be the sequence of transitions used in
the accepting run. We assume (w.l.o.g.) that no transition is used twice. We construct a satisfying
assignment to the variables as follows.
69

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

• q i = qi for all i ≤ ℓ + 1 and q i = qf for all i > ℓ + 1.
• si = λS (ηi ) for all i ≤ ℓ + 1 (si can take any value for other values of i).
• ei = λE (ηi ) for all i ≤ ℓ + 1 (ei can take any value for other values of i).
• pi = (p ∈ λP (ηi )), for each pseudo-class p ∈ P \ {:root} and i ≤ ℓ + 1 (these variables cantake any value for i > ℓ + 1).
• ni = ι, when ηi = η ′ ι for some η ′ and ι and 1 ≤ i ≤ ℓ + 1, otherwise ni can take any value.
• ns:e= j, where j is the number of nodes of type s:e preceding ηi in the sibling order. That isiηi = η ′ ι for some η ′ and ι andι′ < ι ∧ η ′ ι′ ∈ D ∧ j=η ′ ι′ λS (η ′ ι′ ) = λS (η) ∧.

λE (η ′ ι′ ) = λE (η)
When i = 0 or i > ℓ + 1 we can assign any value to ns:ei .
• N i = N − ι where i ≤ ℓ + 1 and η = η ′ ι for some η ′ and ι and N is the smallest number suchthat η ′ N ∈/ D. For i = 0 or i > ℓ + 1 the variable N i can take any value.
s:e• N i = j, where j is the number of nodes of type s:e suceeding ηi in the sibling order. That isηi = η ′ ι for some η ′ and ι andι′ > ι ∧ η ′ ι′ ∈ D ∧ .
j=η ′ ι′ λS (η ′ ι′ ) = λS (η) ∧
λE (η ′ ι′ ) = λE (η)
s:eWhen i = 0 or i > ℓ + 1 we can assign any value to N i .
• Assignments to xs:ai,j are discussed below.
It remains to prove that the given assignment satisfies the formula.
Recallin∧q 0 = q ∧ q n = qf ∧(Tran(i) ∨ q i = qf ) ∧ 
θ =
 .
A

0≤i<n

Consistent
The first two conjuncts follow immediately from our assignment to q i and that the chosen run was
accepting. Next we look at the third conjunct and simultaneously prove Consistentn . When i ≥ ℓ + 1
we assigned qf to q i and can choose any assignment that satisfies Consistentn . Otherwise we show wesatisfy Tran(i) by showing we satisfy Tran(i, ti ). We also show Consistentn is satsfied by induction,noting it is immediate for i = 0 and that for i = 1 we must have either the first orlast case which do notdepend on the induction hypothesis. Consider the form of ti .
↓1. When ti = qi −→ qi+1 we immediately confirm the values of q i , q i+1 , ni+1 , ns:e
i+1 satisfy theσ/ λP (ηi ). We defer the argument
constraint. Similarly for ¬:emptyi since we know :empty ∈for Pres(σ, i) until after the case split. That Consistentn is satisfied can also be seen directly.
70

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong→

2. When ti = qi −→ qi+1 we know ηi = η ′ ι and ηi+1 = η ′ (ι + 1) for some η ′ and ι. We canσs:eeasily check the values of q i , q i+1 , ni+1 , N i , ns:e
i+1 , and N i+1 satisfy the constraint. We defer
the argument for Pres(σ, i) until after the case split. To show Consistentn we observe ni+1 isincreased by 1 and only one ns:e
i+1 is increased by 1, the others being increased by 0. Similarly for
N i and ns:e
.
Hence
the
resultfollows from induction.
i+1→+

3. When ti = qi −−→ qi+1 we know ηi = η ′ ι and ηi+1 = η ′ (ι′ ) for some η ′ , ι, and ι < ι′ . We*s:ecan easily check the values of q i , q i+1 , ni+1 , N i , ns:e
i+1 , and N i+1 satisfy the constraint. We defer
the argument for Pres(σ, i) until after the case split. To satisfy the constraints over the position
variables, we observe that values for δ and δ s:e can be chosen easily for the specified assignment.
Combined with induction this shows Consistentn as required.
◦

4. When ti = qi −→ qi+1σ

We can easily check the values of q i and q i+1 . We defer the argument for Pres(σ, i) until after
the case split. By induction we immediately obtain Consistentn .
We show Pres(σ, i) is satisfied for each ηi and σ labelling ti . Take a node η and σ = τ Θ from thissequence. Note η satisfies σ since thw run is accepting. Recall
Pres(τ, i)∧
(
)


∧


Pres(τ Θ, i) = 
Pres(θ, i) ∧  .
 θ∈NoAtts(Θ)
AttsPres(τ Θ, i)
From the type information of η we immediately satisfy Pres(τ, i).
For a positive θ ∈ Θ there are several cases. If θ = :root then we know we are in η0 and theencoding is ⊤. If θ is some other pseudo class p then the encoding of θ is pi and we assigned true tothis variable. For :nth-child(αn + β) and :nth-last-child(αn + β) satisfaction of theencoding follows immediately from η satisfying θ and our assignment to ni and N i . We satisfy the encodings of :nth-of-type(αn + β), :nth-last-of-type(αn + β), :only-child, and:only-of-type similarly. The latter follow since an only child is position 1 from the start and end,
and an only of type node has 0 strict predecessors or successors of the same type.
For a negative θ ∈ Θ there are several cases. If θ = :not(:root) then we know we are notin η0 and the encoding is ⊤. If θ is the negation of some other pseudo class p then the encoding of
θ is ¬pi and we assigned false to this variable. For the selectors :not(:nth-child(αn + β))
and the opposite selector :not(:nth-last-child(αn + β)) satisfaction of the encoding follows immediately from η satisfying θ, our assignment to ni and N i as well as Proposition C.7 (Correctness of NoMatch(x, α, β)). We satisfy encodings of :not(:nth-of-type(αn + β)) andof :not(:nth-last-of-type(αn + β)) in a likewise fashion. For the remaining cases of:not(:only-child), and :not(:only-of-type) the property follows since, for the former
the node must either not be position 1 from the start or end, and for the latter a not only of type node has
more than 0 strict predecessors or successors of the same type.
Next, to satisfy AttsPres(τ Θ, i) we have to satisfy a number of conjuncts. First, if we have a word
a1 . . . an we assign it to the variables xs:ai,j (where η is the ith in the run and j ranges over all words:apositions within the cimputed bound) ny assigning xs:ai,j = aj when j ≤ n and xi,j = 0 otherwise.
In all cases below, it is straightforward to observe that it a word (within the computed length
bound) satisfies [s|a op v] or :not([s|a op v]) then the encoding AttsPress:a ([s|a op v], i) or
71

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

¬AttsPress:a ([s|a op v], i) is satisfied by our variable assignment. Similarly Nulls(⃗x) is straightforwardly satisfied. Hence, if a word satisfies C then our assignment to the variables means AttsPress:a (C, i)
is also satisfied.
There are a number of cases of conjuncts for attribute selectors. The simplest is for sets Θsa where
we see immediately that all constraints are satisfied for λA (η)(s, a) and hence we assign this value tothe appropriate variables and the conjuct is satisfied also. For each [a] and [a op v] ∈ Θ we havein the document some namespace s such that λA (η)(s, a) satisfies the attribute selector and all negative
selectors applying to all namespaces. Let s′ be the fresh name space assigned to the selector during theencoding and C be the full set of constraints belonging to the conjunct (i.e. including negative ones).
We assign to the variable xs:ai,j the jth character of λA (η)(s, a) (where η is the ith in the run) and satisfy
the conjuct as above. Note here that a single value of s:a is assigned to several s′ :a. This is benign withrespect to the global uniqueness required by ID attributes because each copy has a different namespace.
Finally, we have to satisfy the consistency constraints. We showed Consistentn above. The remaining consistency constraints are easily seen to be satisfied: Consistenti because each ID is uniquecausing at least one pair of characters to differ in every value; Consistentp since it encodes basic consistency constraints on the appearence of pseudo elements in the tree.
Thus, we have satisfied the encoded formula, completing the first direction of the proof.
Lemma C.9. For a CSS automaton A, we haveθA is satisfiable. ⇒ L(A) ̸= ∅Proof. Take a satisfying assignment ρ to the free variables of θA . We construct a tree and node (T, η)as well as a run of A accepting (T, η).
We begin by taking the sequence of states q0 , . . . , qℓ+1 which is the prefix of the assignment to
q 0 , . . . , q n where qℓ is the first occurrence of qf . We will construct a series of transitions t0 , . . . , tℓ withditi = qi −→qi+1 for all 0 ≤ i ≤ ℓ. We will define each di and σi , as well as construct T and η byσiinduction. We construct the tree inductively, then show σi is satisfied for each i.
At first let T0 contain only a root node. Thus η0 is necessarily this root. Throughout the proof welabel each ηi as follows.
• λS (ηi ) = ρ(si ) (i.e. we assign the value given to si in the satisfying assignment).
• λE (ηi ) = ρ(ei ).
(){p | p ∈ P \ {:root} ∧ ρ(pi ) = ⊤} ∪• λP (ηi ) =.
{:root | i = 0}
)
(
)
(
s:a
is the word obtained by stripping all ofρ xs:a. . . xs:a
• λA (ηi )(s, a) = ρ xs:ai,1i,1 . . .(xi,N ) wherei,N( s:a )
s:athe null characters from ρ xi,1 . . . ρ xi,N .
We pick ti as the transition corresponding to a satisfied disjunct of Tran(i) (of which there is at leastdiqi . We proceed by a case split on di . Note only
one since qi ̸= qf when i ≤ ℓ). Thus, take ti = qi −→cases di =↓ and di = ◦ may apply when i = 0.

σi

• When di =↓ we build Ti+1 as follows. First we add the leaf node ηi+1 = ηi 1. Then, if i > 0,
we add siblings appearing afterηi)with types required by the last of type information. That is, we
( s:e
( )
∑
siblings appearing after ηi . In particular, for each s and e we
add ρ N i − 1 =ρ Nis:e∈E LE( s:e )add ρ N i
new nodes. Letting ηi = ηι each of these new nodes η ′ will have the form ηι′ with
ι′ > ι. We set λS (η ′ ) = s, λE (η ′ ) = e, λP (η ′ ) = ∅, λA (η ′ ) = ∅.
72

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

• When di =→ we build Ti+1 by adding a single node to Ti . When ηi = ηι we add ηi+1 =η (ι + 1) with the labelling as above.
( )• When di =→+ we build Ti+1 as follows. We add ρ δ = (ρ(ni+1 ) − ρ(ni )) new nodes of theform ηι′ where ηi = ηι and ρ(ni ) = ι < ι′ ≤ ρ(ni ).( Let )ηi+1 be ηρ(ni ) labelled as above. For
the remaining new nodes, for each s and e, we label ρ δ s:e of the new nodes η ′ with λS (η ′ ) = s,
λE (η ′ ) = e, λP (η ′ ) = ∅, λA (η ′ ) = ∅. Note Consistentn ensures we have enough new nodes topartition like this.
• When di = ◦ and i = 0 we have completed building the tree. If i > 0, we add siblings appearing
after ηi with types required by the last of type information exactly as in the case of d =↓ above.
The tree and node we require are the tree and node obtained after reaching some di = ◦, for which wenecessairily have i = ℓ since ◦ must be and can only be used to reach qf . In constructing this tree wehave almost demonstrated an accepting run of A. To complete the proof we need to argue that all σi aresatisfied by ηi and that the obtained is valid. Let τ Θ = σi .
To check τ we observe that Pres(τ, i) constrains si and ei to values, which when assigned to ηi asabove mean ηi directly satisfies τ .
Now, take some θ ∈ Θ. In each case we argue that Pres(τ, i) ensures the needed properties. Note
this is straightforward for the attribute selectors due to the directness of the Presburger encoding. Consider the remaining selectors.
First assume θ is positive. If it is :root then we must have i = 0 and ηi is the root node as required.
For other pseudo classes p we asserted pi hence we have p ∈ λP (ηi ). The encoding of the remaining
positive constraints can only be satisfied when i > 0. That is, ηi is not the root node.
For :nth-child(αn + β) observe we constructed T such that ηi = ηρ(ni ) for some η. From
the defined encoding of Pres(:nth-child(αn + β), i) we directly obtain that ηi satisfies the selector :nth-child(αn + β). Similarly for :nth-last-child(αn + β) as we always pad
the end of the sibling order to ensure the correct number of succeeding siblings.
For :nth-of-type(αn + β) and :nth-last-of-type(αn + β) selectors, by similararguments to the previous selectors, we have ensured that there are enough preceeding or succeeding
nodes (along with the directness of their Presburger encoding) to ensure these selectors are satisfied by
ηi in T .
( )For :only-child we know there are no other children since ρ(ni ) = ρ N i = 1. Finally fors:ethe( selector) :only-of-type we know there are no other children of the same type since ρ(ni ) =
s:e

ρ Ni
= 0 where ηi has type s:e.
When θ is negative there are several cases. If it is :not(:root) then we must have i > 0 and ηi is
not the root node. For other pseudo classes p we asserted ¬pi hence we have p ∈/ λP (ηi ). The encodingof the remaining positive constraints are always satisfied on the root node. That is, i = 0. When ηi is
not the root node we have i > 0.
For :not(:nth-child(αn + β)) observe we constructed T such that ηi = ηρ(ni ) for someη. From the definition of Pres(:not(:nth-child(αn + β)), i) we obtain that ηi does not satisfy
the required selector :nth-child(αn + β) via Proposition C.7 (Correctness of NoMatch(x, α, β)).
Similarly for the last child selector:not(:nth-last-child(αn + β)) .
For :not(:nth-of-type(αn + β)) and :not(:nth-last-of-type(αn + β)), bysimilar arguments to the previous selectors, we have ensured that there are enough preceeding or succeeding nodes (along with their Presburger encodings and Proposition C.7 (Correctness of NoMatch(x, α, β)))to ensure these selectors are satisfied by ηi in T .
73

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong( )For :not(:only-child) we know there are some other children since ρ(ni ) > 1 or ρ N i >1. Finally for :not(:only-of-type)we know there are other children of the same type since( s:e )
ρ(ns:e
)
>
0
or
ρ
N
>
0
where
η
has
type
s:e.
i
i
i
Thus we have an accepting run of A over some (T, η). However, we finally have to argue that T isa valid document tree. This is enforced by Consistenti and Consistentp .
First, Consistenti ensures all IDs satisfying the Presburger encoding are unique. Since we transferred these values directly to T our tree also has unique IDs.
Next, we have to ensure properties such as no node is both active and inactive. These are all directly
taken care of by Consistentp . Thus, we are done.

D Additional Material for the Experiments Section
D.1 Optimised CSS Automata Emptiness Check
The reduction presented in Section 5 proves membership in NP. However, the formula constructed isquite large even for the intersection of two relatively small selectors. Moreover, selectors generally dono assert complex properties, so for most transitions, the full power of existential Presburger arithmetic
is not needed. Hence, only a small part of each formula requires complex reasoning, while the remainderof the problem is better and easily solved with direct knowledge of the automata.
In this section we present an alternative algorithm. In essence it is a backwards reachability algorithm for deciding non-emptiness of a CSS automaton. Instead of constructing a single large query that
requires a non-trivial solve time, the backwards reachability algorithm only makes small queries to the
SAT solver to enforce constraints that are not simply enforced by a standard automaton algorithm.
The idea is that the automaton collects constraints on the node positions required to satisfy the nthchild (sibling) constraints as it performs its backwards search. It also tracks extra information to ensure
it does not get stuck in a loop, at most one node is labelled :target, and all ids are unique. Eachtime the automaton takes a transition labelled ↓ it checks whether the current set of sibling constraints
is satisfiable. If so, the automaton can move up to the parent node and begin with a fresh set of sibling
constraints. If not, the automaton cannot execute the transition. Once the initial state has been reached,it just remains to check whether the id constraints are satisfiable. If they are, a witness to non-emptinesshas been found.
The algorithm is a worklist algorithm, where the worklist consists of tuples of the form(q, broot , bsib , btarg , Ts, Cid , Cpos , i)
where
• q is the state reached so far,• broot is a boolean indicating whether the current node has to be the root,• bsib is a boolean indicating whether the current node has to have siblings,• btarg is a boolean indicating whether a node marked :target has been seen on the run so far,
• Ts is the set of transitions seen on the current state (recall all loops are self-loops, so cycle detection can be implemented using Ts),• Cid is the set of constraints on id attributes in the run so far,
74

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

• Cpos is the set of constraints on node positions on the current level of the tree (that is, for theassertion of nth-child constraints),• i is the index position in the run (akin to the use of indices in the Presburger encoding).
The initial worklist contains a single element(qf , ⊥, ⊥, ⊥, ∅, ∅, ∅, n)
where n is the number of transitions of the CSS automaton. Note, the final element of the tuple will
always range between 1 and n since we decrement this counter whenever we take a new transition, andeach transition may only be visited once.
In the following, we partition sets of node selector elements into sets containing pseudo-classes,
attribute selectors, and positional selectors. That is, given a node selector τ Θ we write• Atts(Θ) for the elements of Θ of the form θ or :not(θ) where θ is of the form [s|a] or[s|a op v],• Pos(Θ) for the elements of Θ of the form θ or :not(θ) where θ is of the form:nth-child(αn + β),:nth-last-child(αn + β),:nth-of-type(αn + β),:nth-last-of-type(αn + β)
, :only-child, or:only-of-type,• Pseudo(Θ) for the elements of Θ of the form θ or :not(θ) where θ is of the form
:link, :visited, :hover, :active, :focus, :target,:enabled, :disabled, :checked, :root, or :empty .
If the worklist is empty, we terminate, and return that the automaton is empty.
If it is not empty, we take an arbitrary element(q ′ , broot , bsib , btarg , Ts, Cid , Cpos , i)and for each transition

t=q−
→ q′
d

σ

with σ = τ Θ we add to the worklist
( ′
)
′
′
q, broot , b′sib , b′targ , Ts′ , Cid, Cpos, i′where i′ = i−1 is a fresh index, and when certain conditions are satisfied. We detail these conditions andthe definition of the new tuple below. We begin with general conditions and definitions, then describe
those specific to the value of d.
In all cases, we can only add a new tuple if
1. t ∈/ Ts,
2. AttsPres(τ Θ, i′ ) is satisfiable,
75

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong3. Pseudo(Θ) is satisfiable – that is, we do not have p ∈ Θ and :not(p) ∈ Θ for some pseudo-classp, and, moreover, we do not have
• :link ∈ Θ and :visited ∈ Θ, or• :enabled ∈ Θ and :disabled ∈ Θ, or• :root ∈ Θ and bsib = ⊤.
In all cases, we define⊤′• broot = broot⊥:root ∈ Θd=◦otherwise,



⊤
′
• bsib = bsib⊥d ∈ {→, →+ }d=◦otherwise,• b′targ = btarg ∨ (:target ∈ Θ),{′• Ts =

Ts ∪ {t}∅q = q′
otherwise,′′′′′is the set of all clauses AttsPress:id (C, i′ ) appearing in AttsPres(τ Θ, i′ )where Cid
= Cid ∪Cid
• Cid
for some s and C.

Next, we give the conditions and definitions dependent on d. To do so we need to define the set of
positional constraints derived from Pos(Θ). We use a slightly different encoding to the previous section.
We use a variable ni encoding that the node is the ni th child of the parent, and nis:a counting the numberof nodes of type s:a to the left of the current node (exclusive). To encode “last of” constraints, we use
the variable N to encode the total number of siblings of the current node (inclusive), and N s:a to encode
the total number of siblings of the given type (inclusive).
That is, when b′root = ⊤ let′′• Cpos= {⊥} if b′sib = ⊤,′′• Cpos= {⊥} if there is some θ ∈ Pos(Θ) that is not of the form :not(θ’) for some θ′ , and′′• Cpos= {⊤} otherwise,76

CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong′′and when b′root = ⊥ let Cpos={∃n . ni′ = αn + β | :nth-child(αn + β) ∈ Θ} ∪}{{∃n . N − ni′ − 1 = αn + β :nth-last-child(αn + β)} ∈Θ ∪
si′ :ei′ = s:e ⇒s ∈ ⇃(NS) ∧ e ∈ ⇃(E LE) ∧
∪
s:e
.
n
=
αn
+
β
:nth-of-type(αn+ β) ∈ Θ∃n′i{}si′ :ei′ = s:e ⇒s ∈ ⇃(NS) ∧ e ∈ ⇃(E LE) ∧∪:nth-last-of-type(αn + β) ∈ Θ∃n . N s:e − ns:ei′ − 1 = αn + β+ β)) ∈ Θ} ∪{NoMatch(n{( i′ , α, β) | :not(:nth-child(αn)}′
NoMatch
N
−
n
−
1,
α,
β
:not(:nth-last-child(αn
+ β))
i
{
} ∈Θ ∪
si′ :ei′ = s:e ⇒s ∈ ⇃(NS) ∧ e ∈ ⇃(E LE) ∧∪s:e
NoMatch(n,α,β):not(:nth-of-type(αn+ β)) ∈ Θi′{}s(i′ :ei′ = s:e ⇒s ∈ ⇃(NS) ∧ e ∈ ⇃(E LE) ∧)∪:not(:nth-last-of-type(αn + β)) ∈ Θ
NoMatch N s:e − ns:ei′ − 1, α, β



} 
{
∑
N > ni′ ∪ ni′ =
ns:e
∪
′
i


s∈⇃(NS)e∈⇃(E LE)}{s:e
′ :ei′ = s:e ⇒ N s:e > n ′
s
s
∈
⇃(NS)
∧
e
∈
⇃(E
LE ) ∪
ii{}si′ :ei′ ̸= s:e ⇒ N s:e ≥ ns:es ∈ ⇃(NS) ∧ e ∈ ⇃(E LE) .
i′
Then we have the following.
• When d = ◦, we set
′
Cpos

′′
= Cpos ∪ Cpos∪{ni′ = ni } ∪ {si′ :ei′ = si :ei } ∪
s:e
{ns:e
i′ = ni | s ∈ ⇃(NS) ∧ e ∈ ⇃(E LE )} .

• When d =↓,– we require Cpos is satisfiable, ¬broot , and :empty ∈
/ Θ,
′′
′
.
= Cpos– we set Cpos

• When d =→,– we require ¬broot and :root ∈/ Θ,– we set′
Cpos′′= Cpos ∪ Cpos
∪ {ni = ni′ + 1} ∪s:e{si′ :ei′ = s:e ⇒ ns:e
i = ni′ + 1 | s ∈ ⇃(NS) ∧ e ∈ ⇃(E LE )} ∪s:e{si′ :ei′ ̸= s:e ⇒ ni = ns:ei′ | s ∈ ⇃(NS) ∧ e ∈ ⇃(E LE )} .

• When d =→+– we require ¬broot and :root ∈/ Θ,77CSS Minification via Constraint Solving

M. Hague, A. W. Lin, and C.-H. Hong

– we set′
Cpos′′= Cpos ∪ Cpos∪n i = n i′ + δ ∧ δ ≥ 1 ∧


(
)



s:e
s:e
∧




n
=
n
+
δ
∧
s:e


i
i




∧
 (
 s∈⇃(NS) (si′ :ei′ = s:e) ⇒ δ s:e ≥ 1)∃δ, δ s:e s∈⇃(NS) .  e∈⇃(E LE)
 .

∑


e∈⇃(E LE) 



δ=
δ s:e








s∈⇃(NS)e∈⇃(E LE)

Moreover, if we were able to add the tuple to the worklist, and we have
• q = q in ,′• Cposis satisfiable, and• The ID constraints are satisfiable,
then the algorithm terminates, reporting that the automaton is non-empty. To check the ID constraints
are satisfiable, we test satisfiability of the following formula. Let N be the bound on the length of ID
values, as derived in the previous section. We assert∧∧∨
θ∧
xis:id̸= xis:id
.
1 ,j
2 ,j
′
θ∈Cid

s∈NS
1≤j≤N
1≤i1 ,i2 ≤nThat is, we assert all ID conditions are satisfied, and all IDs are unique.

D.2 Sources of the CSS files used in our experiments
We have collected 72 CSS files from 41 global websites for our experiments. These websites cover the
20 most popular sites listed on Alexa [1], which are Google, YouTube, Facebook, Baidu, Wikipedia,
Yahoo!, Reddit, Google India, Tencent QQ, Taobao, Amazon, Tmall, Twitter, Google Japan, Sohu,
Windows Live, VK, Instagram, Sina, and 360 Safeguard. Note that we have excluded Google India
and Google Japan from our collection as we found the two sites share the same CSS files with Google.
We have further collected CSS files from 12 well-known websites ranked between 21 and 100 on thesame list, including LinkedIn, Yahoo! Japan, Netflix, Imgur, eBay, WordPress, MSN, Bing, Tumblr,
Microsoft, IMDb, and GitHub. Our examples also contain CSS files from several smaller websites,
including Arch Linux, arXiv, CNN, DBLP, Google News, Londonist, The Guardian, New York Times,
NetworkX, OpenStreetMap, and W3Schools. These examples were used in the testing and developmentof our tool.

78