# Requirements are All You Need: From Requirements to Code with LLMs

Bingyang Wei  Department of Computer Science
Texas Christian University
Fort Worth, USA
<EMAIL_ADDRESS>
###### Abstract

The pervasive use of textual formats in the documentation of software
requirements presents a great opportunity for applying large language models
(LLMs) to software engineering tasks. High-quality software requirements not
only enhance the manual software development process but also position
organizations to fully harness the potential of the emerging LLMs technology.
This paper introduces a tailored LLM for automating the generation of code
snippets from well-structured requirements documents. This LLM is augmented
with knowledge, heuristics, and instructions that are pertinent to the
software development process, requirements analysis, object-oriented design,
and test-driven development, effectively emulating the expertise of a seasoned
software engineer. We introduce a “Progressive Prompting” method that allows
software engineers to engage with this LLM in a stepwise manner. Through this
approach, the LLM incrementally tackles software development tasks by
interpreting the provided requirements to extract functional requirements,
using these to create object-oriented models, and subsequently generating unit
tests and code based on the object-oriented designs. We demonstrate the LLM’s
proficiency in comprehending intricate user requirements and producing robust
design and code solutions through a case study focused on the development of a
web project. This study underscores the potential of integrating LLMs into the
software development workflow to significantly enhance both efficiency and
quality. The tailored LLM is available at
https://chat.openai.com/g/g-bahoiKzkB-software-engineer-gpt.

###### Index Terms:

Requirements Engineering, Large Language Models (LLMs), ChatGPT, Code
Generation, Use Cases, Software Specification, Automated Software Engineering

##  I Introduction

In the realm of Software Engineering, Requirements Engineering (RE) is
pivotal, serving as the foundation upon which all subsequent development
stages are built. Requirements are traditionally documented in natural
language [1], varying from structured formats like use cases to informal
descriptions. The textual nature of requirements inspires researchers to apply
natural language processing technologies for various requirements engineering
tasks [2]. The advent of large language models (LLMs) such as ChatGPT offers a
promising avenue for assisting requirements engineering processes. These
language models, powered by deep learning algorithms and a gigantic training
corpus, exhibit an unprecedented ability to understand, analyze, and generate
natural language.

Despite the promising capabilities of LLMs, their application in translating
natural language requirements into executable software code remains largely
unexplored. This gap in application presents a unique opportunity to
revolutionize the way software is developed. In this research preview, we
present an initial attempt to use LLMs to assist software engineers by
progressively refining use cases to functional requirements, design models,
test cases, and eventually implementation code.

Our work is built on two assumptions. First, detailed requirements are
provided to the LLMs as input. Second, software engineers’ collaboration with
LLMs is critical.

LLMs need detailed requirements as input. The recent hype in generative AI
makes people have unrealistic expectations for LLMs. People envision that
providing a brief description of a software project will enable LLMs to
automatically generate a fully functional software system. However, LLMs are
not mind readers. A critical aspect of leveraging LLMs is the quality of the
input. In the context of software development, that input would be the
requirements. The potential of the LLMs to generate effective code hinges on
the details and clarity of the requirements documents. Well-crafted
requirements are not just a necessity but a catalyst in fully harnessing the
capabilities of LLMs. High-quality requirements provide a detailed and clear
set of instructions. LLMs, with their advanced natural language processing
capabilities, can interpret these instructions accurately, leading to more
precise and effective code generation. This will make the software more
aligned with the stakeholders’ intent.

The second assumption is that LLMs need software engineers’ collaboration to
be effective. Instead of letting an LLM take full control, they should behave
like a consultant for the software engineers. The LLMs and the software
engineers ought to collaboratively find out the design details that will be
used in the implementation of the software system. By automating parts of the
analysis, design, and coding process, LLMs allow software engineers to focus
on more complex and creative aspects of software development.

The contributions of this paper are as follows:

  * •

We introduced a tailored LLM for generating source code based on the provided
software requirements. The LLM is fine-tuned on the knowledge, instructions,
and heuristics pertinent to the software development process, requirements
analysis, object-oriented design, and test-driven development. The LLM is
available at https://chat.openai.com/g/g-bahoiKzkB-software-engineer-gpt.

  * •

Our innovative integration of stepwise refinement of requirements into the
LLM’s design process significantly enhances its robustness and accuracy.

The structure of this paper is organized in the following manner: Section II
examines the existing literature on generating code with LLMs. Section III
presents a detailed description of our research method, outlining the
systematic approach we have developed to enhance the application of LLMs in
software engineering. Section IV elaborates on the design specifics of our
custom-developed LLM. Following that, Section V offers a case study that
exemplifies the model’s capability in comprehending requirements and producing
code that is both syntactically and semantically accurate. Section VI explores
the implications of LLMs within the field of software engineering and outlines
the directions for future research. Finally, Section VII concludes the paper.

##  II Related Work

Belzner and his colleagues presented an insightful analysis of the potential
benefits and challenges of adopting LLMs in software engineering [3]. Their
discussion spanned across areas such as requirements engineering, system
design, code and test generation, code quality reviews, and software process
management. The authors elucidated their position through a case study on the
development of a “search and rescue” simulation for autonomous planning agents
by interacting with a base ChatGPT model and a Google Bard model. They started
with a one-line textual requirement, and after a series of conversations, the
LLM generated simple test cases for the simulation. Hong and his colleagues
[4] proposed an LLM-based multi-agent framework, MetaGPT, that considers the
context of a software development process and assigns different roles (product
manager, architect, engineer) to several agents. Their approach decomposed the
complex task of developing software into manageable subtasks that require
collaboration among agents. The open-source project, gpt-
eningeer111https://github.com/gpt-engineer-org/gpt-engineer, allows a user to
specify some high-level requirements like “Create a multiplayer snake game in
the browser using a Python back end with MVC components”, the LLM analyzes the
requirements, asks for clarification, and then builds it.

The work referenced prior suggests a misconception that mere brief
descriptions can compel an LLM to “magically” generate a fully operational
software system. We challenge the notion of the so-called “one-line
requirement” method in LLM-driven software development. The case studies cited
to illustrate this approach often involve elementary and well-documented
examples, such as the creation of a snake game. The simplicity of these
examples and the widespread availability of their source codes online may
mislead some to overestimate the efficacy of succinct requirement statements.
While “one-line requirement” might suffice for tasks that are detailed and
low-level, e.g., “Create a web page to measure user reaction time by clicking
a button”—which may directly leverage technical descriptions likely present in
training datasets, their effectiveness diminishes with the complexity and
uniqueness of software projects not represented in the LLM’s training data.
This paper aims to explore the boundaries of LLM capabilities in software
development under such conditions.

A pivotal factor in employing LLMs for software development is the quality of
input requirements. The model’s success in accurately interpreting and
translating these requirements significantly depends on their clarity and
specificity. However, this critical aspect is often overlooked in existing
literature. Our position is that human involvement in crafting requirements is
irreplaceable by LLMs. While these models can assist in the process, their
outputs must be meticulously reviewed and validated by human stakeholders. We
advocate against the reliance on “one-line requirement” methodologies for LLM-
based software development. Instead, we emphasize the importance of dedicating
time and effort to articulate high-quality, detailed requirements and to
thoroughly consider potential scenarios. Our version of LLM is optimized to
comprehend structured and comprehensive inputs, rather than simplistic, one-
liner prompts.

The only piece of related work that aligns with our perspective is the open-
source initiative, GPT-
Synthesizer222https://github.com/RoboCoachTechnologies/GPT-Synthesizer. This
tool stands out by assisting users in comprehending their project’s needs and
exploring design options through a well-organized interview process. Tailored
for individuals unsure of how to initiate or define their software projects,
the GPT Synthesizer proves to be a crucial aid.

##  III Research Method

The review of existing literature reveals a significant gap in the application
of LLMs for the direct generation of executable software code from natural
language requirements. To bridge this gap, our research introduces a novel
method that not only enhances the LLM’s understanding of software requirements
but also iteratively refines its output to ensure that the generated code
meets the semantic expectations. This methodological innovation is vital for
advancing the use of LLMs in software development, particularly in
environments where accuracy and alignment with business goals are paramount.

###  III-A Research Objectives

Our research aims to develop and evaluate a tailored LLM that can effectively
translate detailed software requirements into high-quality, functional code.
The primary objective of this research is to demonstrate the feasibility of
using LLMs for end-to-end software development tasks, thereby minimizing human
intervention in the coding process while ensuring that the outputs are
practically viable and aligned with user intentions.

###  III-B Research Design

This research follows a phased approach:

  * •

Phase 1: Model Selection and Customization. We begin by selecting ChatGPT as
the foundational LLM due to its advanced capabilities in understanding and
generating natural language. The LLM is then customized to suit the specific
needs of software development, integrating software engineering knowledge and
instructions that enhance its ability to process and translate software
requirements into functional code.

  * •

Phase 2: Data Preparation. Software requirements will be collected with the
intent to represent the diversity of real-world software development projects
as accurately as possible. These will include both industry-standard
specifications and hypothetical scenarios designed to test the model’s
capabilities across different scenarios.

  * •

Phase 3: Evaluation and Refinement. The tailored LLM’s effectiveness will be
evaluated through a series of controlled tests, analyzing both the code
quality and its alignment with the input requirements. The evaluation phase
will involve comparing the LLM-generated code with expert-written code to
assess accuracy, adherence to requirements, and practical usability. Both
qualitative and quantitative measures will be employed to provide a thorough
evaluation of the tailored LLM’s performance. Feedback from these evaluations
will be used to further refine the model.

###  III-C Iterative Refinement Process

An iterative refinement process is integral to the methodology. After each
evaluation phase, detailed feedback will be analyzed to identify any
shortcomings of the tailored LLM. This feedback informs subsequent refinements
to the model, enhancing the tailored LLM’s ability to generate more accurate
and relevant code outputs.

##  IV A Tailored LLM for Software Engineering

In this section, we explore the design of our tailored LLM crafted to support
software engineers in generating code from high-level requirements. To depict
the process of engagement with our customized LLM, we employ a UML activity
diagram, which outlines the workflow for interaction between the software
engineers and the LLM (Fig. 1).

Figure 1: A human software engineer’s interaction with the tailored GPT model.

###  IV-A Software Requirements Documents

Without a foundation of high-quality requirements as input, even the most
performant LLM can be rendered useless. Instead of typing a few informal
itemized requirements to an LLM, we require the software development team to
upload to the LLM structured requirements in the format of project glossary
(Google Docs), vision and scope (Google Docs), and use cases (Google Docs).

  * •

Project Glossary: This document contains definitions of all key terms used
within the project, ensuring clarity and consistency across all project
communications and artifacts.

  * •

Vision and Scope: This outlines the overall objectives, the scope of the
project, and the roles of different stakeholders, providing a comprehensive
overview of the project’s goals and expected outcomes.

  * •

Use Cases: This document includes detailed descriptions of each use case,
illustrating specific functionality that the software is expected to perform.
These are particularly valuable for understanding the interactions between the
system and its users, as well as between different components of the system.

The time and effort invested in writing high-quality software requirements
pays off significantly, especially in the era of LLMs.

###  IV-B A Progressive Prompting Approach

Inspired by the stepwise refinement technique in program development, we adopt
a progressive prompting approach to interact with the LLMs. In Fig. 1, the
interaction starts with the software engineer uploading detailed requirements
documents to the LLM. Instead of instructing the LLM to rush to the final
artifact i.e., the test cases and code, we give the LLM “time to think” by
asking the LLM to follow a waterfall software development process and come up
with intermediate artifacts along the way. In particular, the software
engineer prompts the LLM to first refine requirements into detailed functional
requirements. Then, the LLM is prompted to devise an object-oriented design
based on the functional requirements. The purpose of the design is to discover
objects, assign responsibilities to them, and model their interactions.
Finally, based on the functional requirements and the design produced in the
previous steps, the LLM is prompted to generate test cases and code.

This progressive prompting approach is in line with both the waterfall
software development process and the requirements abstraction hierarchy (Fig.
2). By breaking down the complex software development task into smaller and
more specific subtasks, this approach generates a “chain of thought” [5],
making the LLM more efficient and effective in performing complex tasks in
software development. The intermediate artifacts like functional requirements
and object-oriented design are valuable to the software development team since
they allow the human engineers to understand and verify the LLM’s chain of
thought and provide feedback. Those artifacts also help verify in case of
hallucination. This will also have the benefit of requirement traceability
[6].

Figure 2: A requirement hierarchy.

###  IV-C Instructions and Knowledge Base for the Tailored LLM

In this study, we selected ChatGPT as the foundational LLM. Prompts can be
utilized in two ways when interacting with an LLM like ChatGPT. The first
method involves directly requesting ChatGPT to generate code based on provided
requirements. The second method introduces a structured approach where,
instead of allowing ChatGPT to autonomously navigate software development
tasks, we embed specific instructions to guide the development process. These
instructions include, for example, heuristics on converting use cases into
functional requirements and developing an object-oriented design. These
guidelines act as constraints and safeguards to align the development closely
with an organization’s standard processes and mitigate the risk of generating
irrelevant or inaccurate content.

In this work, we took advantage of ChatGPT’s new feature, GPTs, by customizing
a base ChatGPT to excel in generating code from high-level requirements. The
tailored GPT is named “Software Engineer
GPT”333https://chat.openai.com/g/g-bahoiKzkB-software-engineer-gpt. We also
make the instructions for the GPT
available444https://github.com/Washingtonwei/software-engineer-gpt so that
other practitioners can freely modify the instructions to create their own
customized GPT.

Besides instructions, we provided a comprehensive knowledge
base555https://github.com/Washingtonwei/software-engineer-
gpt/blob/main/knowledge.md for the tailored GPT. The document is an extensive
exploration of requirements engineering. It starts with a general introduction
to requirements engineering, emphasizing its role as a collection of
activities for defining, documenting, and adapting the objectives and
constraints of a software system based on existing problems and new
technological opportunities. The document then delves into the specific roles
and responsibilities of a business analyst in this process, detailing their
crucial function in forging partnerships between customers and developers. It
covers various types of requirements in software projects, such as business
requirements, user requirements, functional requirements, and quality
attributes. These are organized into a hierarchy, illustrating how each level
adds detail and elaborates on higher-level requirements. The document also
provides an in-depth look at user requirements, including their representation
through use cases, and the specific elements that constitute a use case.
Additionally, it addresses functional requirements and their derivation from
user requirements. Furthermore, the document outlines a software development
workflow incorporating requirements analysis, object-oriented design, and
testing, followed by a discussion on software architecture with a focus on the
“Clean Architecture”. Finally, the document offers guidelines for object-
oriented design, including identifying key classes and assigning
responsibilities, and concludes with an overview of test-driven development,
demonstrating its application in the context of the presented software
development approach. The contents in the knowledge base are extracted from
[7] and [8].

##  V Case Study

To demonstrate LLMs’ capability of generating code from requirements, we chose
a medium-sized web project called “SuperFrog Scheduler”. SuperFrog is the
iconic horned frog mascot of Texas Christian University (TCU), known for its
participation in numerous events annually, including sports, weddings, charity
functions, and media appearances. To facilitate the scheduling of SuperFrog’s
appearances, a request management system is necessary, involving submission by
customers, review by the Spirit Director, and acceptance by student performers
embodying SuperFrog. A development team, consisting of five software
developers, commenced work on the SuperFrog Scheduler in October 2018 and
completed the project in May 2019. During the requirements gathering phase,
the team identified and documented 26 user-goal level use cases, which are
available here (Google Docs). The “SuperFrog Scheduler” was selected for its
complexity and relevance, involving multiple stakeholders and intricate
scheduling requirements typical of real-world software projects. This case
study not only provides detailed documentation for verifying the tailored
LLM’s code generation capabilities but also showcases the model’s practical
application in a dynamic educational environment. Its visibility and the
educational context offer a unique opportunity to demonstrate the potential of
LLMs in streamlining complex software development tasks while educating future
software engineers on AI-driven development tools. For this preview paper, our
focus is restricted to the implementation of Use Case 18 (Google Docs). Use
Case 18 describes the process where the Spirit Director generates TCU
Honorarium Payment Request Forms for SuperFrog Students who have completed
appearance requests. The system facilitates the creation of these forms by
providing the necessary details for each eligible appearance. This process
aims to ensure SuperFrog Student workers are compensated for their services in
a timely and efficient manner.

Note that the design and the source code of this project are never made
accessible via the web, and therefore not part of ChatGPT’s training data.
This is different from all the previous work. In this section, we demonstrate
the complete software development process focusing on Use Case 18 by
conversing with the tailored GPT. The complete conversation with the tailored
GPT is available at this
link666https://chat.openai.com/share/8f52df6a-d00c-44df-a2c4-4a9235415418.
This real-world application can provide tangible evidence of the effectiveness
and challenges of using ChatGPT in software engineering.

To enhance the accessibility and reproducibility of our research, we have
compiled all essential project artifacts into a replication
package777https://drive.google.com/drive/folders/1CFxMNblwOV-
mthVcRRb2gTsFxNRO7nlz?usp=sharing. This package includes the project glossary,
vision and scope, and detailed use cases, which are fundamental to
understanding the development context and requirements of the “SuperFrog
Scheduler”.

###  V-A Uploading Software Requirements

We initiated the process by uploading the project glossary, vision and scope,
and use cases to the tailored GPT. These requirements documents provide
critical context and background information for subsequent tasks needed. The
GPT then summarized the contents of the three documents (see the conversation
excerpt in Fig. 3). The GPT prompted us to pick one use case to start.

Figure 3: The user uploads requirements documents to Software Engineer GPT.

###  V-B Deriving Functional Requirements

Use cases describe tasks that users will need to perform with the system, or
user-system interactions that will result in a valuable outcome for some
stakeholders. We instructed the GPT to derive the necessary functional
requirements that must be implemented to enable each use case. As a proof of
concept, we only demonstrated the design of Use Case 18, which pertains to the
generation of Honorarium (Payment for Services) request forms for student
workers (see the derived functional requirements in the conversation excerpt
in Fig. 4). Then, the GPT asked us to proceed with creating an object-oriented
design for this use case.

Figure 4: Software Engineer GPT derives the functional requirements from use
cases.

###  V-C Generating an Object-Oriented Design

In this step, we instructed the GPT to carry out an object-oriented design for
Functional Requirement 2: The system shall automatically populate the
Honorarium Request Forms with details of the appearance, including date,
location, and SuperFrog Student involved. Based on the instructions defined in
the knowledge document, the GPT:

  * •

identified key classes that users use to describe the problem domain and
implementers use to describe the solution domain,

  * •

assigned responsibilities to each class,

  * •

provided properties and operations to each class that are needed to carry out
these responsibilities,

  * •

came up with an object collaboration so that the objects of the classes can
collaborate to carry out the functional requirements of a use case.

Fig. 5 shows the excerpt of the conversation. As expected, some designs were
not aligned with our intentions. So, we provided detailed feedback to the GPT,
and the GPT quickly adjusted the design.

Figure 5: Software Engineer GPT creates an object-oriented design for one
functional requirement.

###  V-D Generating Test Cases

In this step (Fig. 6), the tailored GPT was instructed to generate one unit
test case for the generateForm method in the class FormGenerator. We also
specified the technologies required. It turned out that again we needed to
clarify some misunderstandings (detailed conversion is not shown).

Figure 6: Software Engineer GPT generates a test case for one method of a
class.

###  V-E Generating Implementation Code

In the end, based on the intermediate artifacts or “chain of thoughts”
generated in the previous steps, we believe that the GPT has enough context
and information to move to the final step. We then instructed the GPT to
generate the implementation code for the generateForm in the class
FormGenerator (Fig. 7).

Figure 7: Software Engineer GPT generates the implementation code based on the
test case.

##  VI Discussion

In this section, we explore the implications of our approach for the future of
software engineering, education, and agile methodology. Additionally, we
address the limitations of our study and outline directions for future
research.

###  VI-A Requirements are All You Need

While the title of this paper, “Requirements are All You Need: From
Requirements to Code with LLMs”, might seem hyperbolic, it aptly highlights
the pivotal role of requirements engineering in contemporary AI-assisted
software engineering. Even amidst the advanced capabilities of LLMs and other
AI tools in streamlining the coding process, the initial step of meticulously
defining requirements remains a cornerstone. A well-articulated set of
requirements is fundamental to leveraging AI technologies effectively in
software development, thereby reinforcing the indispensability of requirements
engineering as a discipline within the AI-enhanced software engineering
landscape.

###  VI-B Impact on Software Engineering Education

LLMs have transformed the landscape of programming, showcasing exceptional
abilities in code generation and problem-solving. This technological
advancement has undeniably increased efficiency and productivity within
software development. However, the question arises: Is teaching traditional
designing, programming, and testing skills to students still necessary? The
unequivocal answer is yes. Despite the prowess of LLMs in handling a variety
of programming tasks, their limitations cannot be overlooked. These models
sometimes misunderstand us and produce code that is not aligned with our
intent, underscoring the need for human oversight and validation. It is
imperative for software engineering education to evolve, teaching students to
critically assess AI-generated designs and code for accuracy, efficiency,
maintainability, and security.

The emergence of LLMs, such as ChatGPT, and tools like GitHub Copilot and
Devin AI, signals a pivotal shift in software engineering education. To stay
ahead, educators must not only embrace the LLMs themselves but also guide
students on how to effectively leverage LLMs. This entails a significant
pedagogical shift towards enhancing soft skills. Students should be trained to
excel in communication with various stakeholders, the art of drafting high-
quality software requirements, and conducting thorough design and code
reviews. Such skills are becoming increasingly vital as the role of manual
coding, particularly for minor features, diminishes.

###  VI-C LLMs Redefine Agile

This paper presupposes the availability of detailed and extensive
requirements, such as use cases, for input into LLMs. Crafting effective
requirements, however, can be a labor-intensive process, and this strategy
might initially be met with skepticism. A key question arises: How does this
strategy align with Agile methodologies, which prioritize working software
over comprehensive documentation? Critics may argue that the focus on detailed
and often extensive use cases could result in an undue emphasis on
documentation, thereby potentially redirecting time and resources away from
actual software development. Yet, this concern may be mitigated in the context
of LLMs. We contend that the emergence of LLMs is poised to transform the
Agile methodology. Owing to LLMs’ capabilities in test and code generation,
the process of translating well-defined requirements into code has become
significantly more efficient. This efficiency could allow software engineers
to allocate more time to the crucial tasks of communication and requirement
specification, thereby enhancing the development process.

###  VI-D Limitations and Future Work

The proof-of-concept case study showcased the significant potential of
leveraging LLMs in software development, particularly in the context of use-
case-driven development for web projects. However, further testing across a
broader spectrum of software projects—including real-time systems, AI-driven
applications, and games—is essential to fully understand the applicability and
limitations of LLMs in these varied contexts. Additionally, exploring
different requirements specifications and design methodologies is crucial to
assess the adaptability and effectiveness of LLMs in diverse software
engineering paradigms. While a tailored version of ChatGPT has been developed
and made publicly available, utilizing the default user interface of ChatGPT
for software development presents practical challenges. Specifically, software
engineers may find it cumbersome to navigate through previously generated
designs or code snippets due to the need to scroll extensively. To address
this issue, we envisage the creation of a user-friendly web application in
future work. This application will aim to streamline the process, offering a
more intuitive and visual approach to translating requirements into tests and
code.

A comprehensive evaluation of this approach remains a priority for future
research. We intend to encourage software engineers to incorporate these LLMs
into their workflow and solicit their feedback. This will provide valuable
insights into the practicality, efficiency, and user experience of using LLMs
in real-world software development scenarios, thereby informing further
improvements and adaptations.

##  VII Conclusion

In this research preview, we introduced a tailored LLM designed to assist
software engineers in refining requirements into software design, test cases,
and implementation code. This LLM incorporates an external knowledge base that
encompasses both the knowledge and heuristics of requirements engineering and
software design. A case study was conducted to demonstrate the practicality
and effectiveness of this customized LLM, underscoring its potential in
software development. Furthermore, our research underscored the critical role
of meticulously crafted requirements in maximizing the benefits of LLMs within
the realm of software engineering.

Future work will explore a broader array of requirements specification
techniques and software design methodologies. Additionally, a more thorough
evaluation of this innovative approach will be undertaken to further validate
its efficacy and applicability in diverse software engineering contexts.

## References

  * [1] M. Kassab, C. Neill, and P. Laplante, “State of practice in requirements engineering: contemporary data,” _Innovations in Systems and Software Engineering_ , vol. 10, pp. 235–241, 2014.
  * [2] L. Zhao, W. Alhoshan, A. Ferrari, K. J. Letsholo, M. A. Ajagbe, E.-V. Chioasca, and R. T. Batista-Navarro, “Natural language processing for requirements engineering: A systematic mapping study,” _ACM Computing Surveys (CSUR)_ , vol. 54, no. 3, pp. 1–41, 2021.
  * [3] L. Belzner, T. Gabor, and M. Wirsing, “Large language model assisted software engineering: prospects, challenges, and a case study,” in _International Conference on Bridging the Gap between AI and Reality_. Springer, 2023, pp. 355–374.
  * [4] S. Hong, X. Zheng, J. Chen, Y. Cheng, J. Wang, C. Zhang, Z. Wang, S. K. S. Yau, Z. Lin, L. Zhou _et al._ , “Metagpt: Meta programming for multi-agent collaborative framework,” _arXiv preprint arXiv:2308.00352_ , 2023.
  * [5] J. Wei, X. Wang, D. Schuurmans, M. Bosma, F. Xia, E. Chi, Q. V. Le, D. Zhou _et al._ , “Chain-of-thought prompting elicits reasoning in large language models,” _Advances in Neural Information Processing Systems_ , vol. 35, pp. 24 824–24 837, 2022.
  * [6] F. A. Pinheiro, “Requirements traceability,” _Perspectives on software requirements_ , pp. 91–113, 2004.
  * [7] K. E. Wiegers and J. Beatty, _Software requirements_. Pearson Education, 2013.
  * [8] B. Meyer, _Object-oriented software construction_. Prentice hall Englewood Cliffs, 1997, vol. 2.


# Strengthening Hadwiger’s conjecture for $4$\- and $5$-chromatic graphs

Anders Martinsson  Department of Computer Science, Institute of Theoretical
Computer Science, ETH Zürich, Switzerland<EMAIL_ADDRESS>and
Raphael Steiner  Department of Computer Science, Institute of Theoretical
Computer Science, ETH Zürich, Switzerland<EMAIL_ADDRESS>
###### Abstract.

Hadwiger’s famous coloring conjecture states that every $t$-chromatic graph
contains a $K_{t}$-minor. Holroyd [Bull. London Math. Soc. 29, (1997), pp.
139–144] conjectured the following strengthening of Hadwiger’s conjecture: If
$G$ is a $t$-chromatic graph and $S\subseteq V(G)$ takes all colors in every
$t$-coloring of $G$, then $G$ contains a $K_{t}$-minor _rooted at $S$_.

We prove this conjecture in the first open case of $t=4$. Notably, our result
also directly implies a stronger version of Hadwiger’s conjecture for
$5$-chromatic graphs as follows:

Every $5$-chromatic graph contains a $K_{5}$-minor with a singleton branch-
set. In fact, in a $5$-vertex-critical graph we may specify the singleton
branch-set to be any vertex of the graph.

The second author was supported by an ETH Zürich Postdoctoral Fellowship.

##  1\. Introduction

Given a graph $G$ and a number $t\in\mathbb{N}$, a _$K_{t}$ -minor_ in $G$ is
a collection $(B_{i})_{i=1}^{t}$ of pairwise disjoint non-empty subsets of
$V(G)$ such that $G[B_{i}]$ is connected for every $i\in[t]$ and for every
distinct $i,j\in[t]$ the sets $B_{i}$ and $B_{j}$ are adjacent111Two subsets
$A,B$ of the vertex-set $V(G)$ of a graph $G$ are called _adjacent_ if there
exists an edge in $G$ with one endpoint in $A$ and one endpoint in $B$. in
$G$. The sets $B_{1},\ldots,B_{t}$ are also called the _branch-sets_ of the
$K_{t}$-minor.

Hadwiger’s conjecture, among the most famous and difficult open problems in
graph theory, states the following.

######  Conjecture 1.1 (Hadwiger 1943 [9]).

For every integer $t\geq 1$, every graph $G$ with $\chi(G)=t$ contains a
$K_{t}$-minor.

Hadwiger’s conjecture was proved for $t\leq 4$ by Hadwiger himself [9], and
also by Dirac [6], while the case $t=5$ was shown to be equivalent to the
Four-Color-Problem by Wagner [20]. Since Appel and Haken’s proof of the Four-
Color-Theorem [1, 2] in 1976 and its later independent proof by Robertson,
Sanders, Seymour and Thomas [18], Hadwiger’s conjecture was known to hold for
$t=5$. In a tour de force, in 1993 Robertson, Seymour and Thomas [17] proved
Hadwiger’s conjecture for $t=6$ by reducing it to the Four-Color Theorem. All
the cases $t\geq 7$ remain wide open as of today. Much of recent research has
focused on asymptotic bounds for coloring graphs with no $K_{t}$-minor rather
than on the precise version of the conjecture, and there has been some
exciting progress in this direction recently [3, 16]. For further partial
results on Hadwiger’s conjecture and background, we refer the reader to the
survey article [19] by Seymour.

In this paper, we investigate a strengthening of Hadwiger’s conjecture
proposed by Holroyd [11] in 1997. His stronger version of Hadwiger’s
conjecture concerns the containment of minors in graphs of given chromatic
number that are _rooted_ at a particular set of vertices. Rooted minors have
received significant attention before, we refer to [4, 7, 8, 10, 12, 13, 15,
21] for a selection of results on rooted minors in graphs. Here we use the
following definition: For a set $S\subseteq V(G)$, we say that a $K_{t}$-minor
$(B_{i})_{i=1}^{t}$ in $G$ is _$S$ -rooted_ or _rooted at $S$_ if $B_{i}\cap
S\neq\emptyset$ for all $i\in[t]$. A second notion we need to introduce before
stating Holroyd’s conjecture is that of _colorful sets_. For a graph $G$ and
$S\subseteq V(G)$ we say that $S$ is _colorful_ in $G$ if for every proper
$\chi(G)$-coloring of $G$ there are vertices of all $\chi(G)$ colors contained
in $S$.

A colorful set in a graph may be seen as a part of the graph that “is hard to
color”. In that sense, it is quite intuitive that one may hope to find a
$K_{t}$-minor rooted at this part of the graph. This is exactly Holroyd’s
conjecture (named “Strong Hadwiger’s conjecture” in [11]):

######  Conjecture 1.2 (Strong Hadwiger’s conjecture, Holroyd 1997 [11]).

Let $G$ be a graph with $\chi(G)=t$, and let $S$ be a colorful set in $G$.
Then $G$ contains an $S$-rooted $K_{t}$-minor.

Holroyd proved his conjecture for $t\leq 3$ in [11]. Here, we take the next
step and prove the Strong Hadwiger’s conjecture for $t=4$.

######  Theorem 1.3.

Let $G$ be a graph with $\chi(G)=4$ and let $S$ be a colorful set in $G$. Then
$G$ contains an $S$-rooted $K_{4}$-minor.

As was already noted by Holroyd (Theorem 2 in [11]), the truth of the Strong
Hadwiger’s conjecture for a value $t$ implies the truth of Hadwiger’s
conjecture for the value $t+1$. Therefore, Theorem 1.3 implies Hadwiger’s
conjecture for $t=5$. In fact, combining Holroyd’s argument with Theorem 1.3
we obtain a slight strengthening of Hadwiger’s conjecture for $t=5$ as
follows.

######  Corollary 1.4.

  * •

Every $5$-vertex-critical graph $G$ for every $v\in V(G)$ has a $K_{5}$-minor
containing $\\{v\\}$ as a singleton branch-set.

  * •

Every $5$-chromatic graph contains a $K_{5}$-minor with a singleton branch-
set.

###### Proof.

  * •

Let $v\in V(G)$. Then by criticality of $G$ we have $\chi(G)=5,\chi(G-v)=4$.
This implies that $N_{G}(v)$ is a colorful set in $G-v$. By Theorem 1.3 there
exists an $N_{G}(v)$-rooted $K_{4}$-minor in $G-v$, and adding to it the
branch-set $\\{v\\}$ yields the desired $K_{5}$-minor.

  * •

This follows from the first item since every $5$-chromatic graph has a
$5$-critical subgraph.

∎

To the best of our knowledge these strengthenings of Hadwiger’s conjecture for
$t=5$ are novel.

### Organization and Outline.

The rest of the paper is devoted to the proof of Theorem 1.3. In Section 2, we
prepare the proof by discussing a few results from the literature that will be
needed in our proof. Most crucially, we will rely on a characterization for
the existence of $K_{4}$-minors rooted at a set of four distinct vertices by
Fabila-Monroy and Wood [8]. We then present our proof in Section 3. A main
part of the proof is to establish several properties of a smallest
counterexample $G$ to Theorem 1.3 in terms of connectivity and the
distribution of the vertices in $S$ over the graph. In another step, these
structural properties can then either be used to find the desired rooted
$K_{4}$-minor directly, or to restrict the structure of $G$ to a planar graph
(Lemma 3.1). At this final stage, we invoke the Four-Color-Theorem to derive a
$4$-coloring that shows that $S$ cannot be colorful and this yields the
desired contradiction.

##  2\. Preliminaries

In this section we state a few preliminary results from the literature that we
will use in our proof of Theorem 1.3. The first is a precise characterization
when a graph admits a $K_{3}$-minor rooted at $3$ given vertices due to
Holroyd [11] and Linusson and Wood [14].

######  Lemma 2.1 (Theorem 6 in [11], Lemma 5 in [14]).

Let $G$ be a graph, and let $a,b,c\in V(G)$ be three distinct vertices. If for
every vertex $v\in V(G)$ at least two of $a,b,c$ are in a common component of
$G-v$, then there exists an $\\{a,b,c\\}$-rooted $K_{3}$-minor in $G$.

Second, we will need a result by Fabila-Monroy and Wood [8] for characterising
when a graph contains a $K_{4}$-minor rooted at four given verties $a,b,c,d$.
Following the notation in [8], given a graph $H$, we denote by $H^{+}$ a graph
obtained from $H$ by, for each triangle $T$ in $H$, adding a disjoint
(possibly empty) set of vertices $C_{T}$ to $H$, making them a clique and
adjacent to the three vertices of the triangle $T$ in $H$ (the sets $C_{T}$
and $C_{T^{\prime}}$ must be chosen disjoint for different triangles
$T,T^{\prime}$ in $H$). An $\\{a,b,c,d\\}$-web is a graph $H^{+}$ where $H$
has a planar embedding with outerface $\\{a,b,c,d\\}$ in some order, and such
that every triangle in $H$ forms a face in this embedding. Fabila-Monroy and
Wood [8] give a precise description of the edge-maximal graphs with no
$K_{4}$-minor rooted at four specified vertices. Here, we will only need a
weaker version of their main result.

######  Theorem 2.2.

Let $G$ be a graph with four marked vertices $a,b,c,d$ such that $G$ contains
no $\\{a,b,c,d\\}$-rooted $K_{4}$-minor. Then either

  1. (1)

$G$ is a spanning subgraph of an $\\{a,b,c,d\\}$-web, or

  2. (2)

there exist vertices $u,v\in V(G)$ such that $G-\\{u,v\\}$ has at least three
distinct connected components.

###### Proof.

By Theorem 15 in [8], $G$ is a spanning subgraph of a graph in one the classes
$\mathcal{A}$-$\mathcal{F}$. Class $\mathcal{D}$ is precisely the
$\\{a,b,c,d\\}$-webs in which case $(1)$ holds. It can be directly checked
that all graphs in the remaining classes (and thus also their spanning
subgraphs) have a $2$-separator as described in $(2)$. ∎

Throughout the proof we will use the following convenient (and standard)
terminology to speak about separators in graphs: A _separation_ of a graph is
a tuple $(A,B)$ where $A,B$ are subsets of $V(G)$ with $A\cup B=V(G)$, such
that $A\setminus B\neq\emptyset\neq B\setminus A$ and such that there are no
edges in $G$ connecting a vertex in $A\setminus B$ to a vertex in $B\setminus
A$. The _order_ of a separation is $|A\cap B|$, and $A\cap B$ is called the
_separator_ of the separation $(A,B)$. It is easy to see that a graph is
$k$-connected if and only if all its separations have order at least $k$. In
the proof, we repeatedly use Menger’s theorem for vertex-disjoint paths in the
following two variants:

######  Theorem 2.3 (Menger’s theorem-set versions, cf. Theorem 3.3 in [5]).

Let $G$ be $k$-connected, $v\in V(G)$ and $A,B\subseteq V(G)$.

  * •

There are $\min\\{k,|A|,|B|\\}$ vertex-disjoint paths in $G$ each with
endpoints in $A$ and $B$.

  * •

If $v\notin A$ then there are $\min\\{k,|A|\\}$ paths in $G$, each of them
connecting $v$ to a vertex in $A$, and any two of them only sharing the vertex
$v$.

We note that in the above statement as well as throughout the whole manuscript
we allow paths to consist of single vertices (i.e., be of length $0$).

##  3\. The proof

For a $3$-connected graph $G$ and a subset $S\subseteq V(G)$ of vertices, we
say that $S$ is _spread out in $G$_ if for every separation $(A,B)$ in $G$ of
order $3$, it holds that $S\setminus A\neq\emptyset\neq S\setminus B$. The
following auxiliary statement will be of crucical use in our proof of Theorem
1.3.

######  Lemma 3.1.

Let $G$ be a $3$-connected graph, and let $S\subseteq V(G)$ such that $|S|\geq
4$ and $S$ is spread out in $G$. If $G$ contains no $S$-rooted $K_{4}$-minor
then the graph $G^{a}(S)$, obtained from $G$ by adding a new vertex and making
it adjacent to every element of $S$, is planar.

We will prove Lemma 3.1 by combining Theorem 2.2 with the following statement.

######  Lemma 3.2.

Let $G$ be a 3-connected graph, and let $S\subseteq V(G)$ be spread out in $G$
such that $G$ contains no $S$-rooted $K_{4}$-minor. Then for any separation
$(A,B)$ of order $3$ such that $|A\cap S|\geq 3$, it holds that $G[B]$ has a
planar embedding with $A\cap B$ on the outerface.

###### Proof of Lemma 3.2.

We prove Lemma 3.2 by induction on the size of $B$. Note that for any
separation, we have $|B|\geq 4$. Moreover, for $|B|=4$, it is clear that such
a planar embedding exists. Turning to the induction step, we fix any
separation $(A,B)$ as above with $|B|\geq 5$, and assume the statement is true
for any separation $(A^{\prime},B^{\prime})$ as above with $|B^{\prime}|<|B|$.
Furthermore, we pick some $S^{\prime}\in\binom{A\cap S}{3}$.

######  Claim 3.3.

$G[A]$ and $G[B]$ are connected.

###### Proof.

By Menger’s theorem, any $v\in A\setminus B$ is connected to $A\cap B$ in $G$
by three paths that pairwise only share $v$ as a common vertex. These paths
are completely contained in $A$ as $A\cap B$ is a separator, so, in
particular, $G[A]$ is connected. Similarly, any $v\in B\setminus A$ is
connected to $A\cap B$ by three internally disjoint paths in $G$, so $G[B]$ is
also connected. ∎

######  Claim 3.4.

There exist enumerations $\\{s_{1},s_{2},s_{3}\\}=S^{\prime}$ and
$\\{c_{1},c_{2},c_{3}\\}=A\cap B$ and disjoint sets
$A_{1},A_{2},A_{3}\subseteq A$ such that $\\{s_{i},c_{i}\\}\subseteq A_{i}$
and $G[A_{i}]$ is connected for each $i\in[3]$ and such that $A_{2}$ is
adjacent to $A_{1}$ and $A_{3}$ in $G$.

###### Proof.

Since $G$ is $3$-connected, there exists three vertex-disjoint paths from
$S^{\prime}$ to $A\cap B$. Let $P_{1},P_{2},P_{3}$ be an ordering of the paths
such that
$\text{dist}_{G[A]}(V(P_{1}),V(P_{2}))+\text{dist}_{G[A]}(V(P_{2}),V(P_{3}))$
is minimized. Then letting $A_{1}=V(P_{1})$, $A_{3}=V(P_{3})$ and $A_{2}$
equal the connected component of $G[A\setminus(V(P_{1})\cup V(P_{3}))]$
containing $V(P_{2})$, we obtain sets with the desired properties (by the
minimality assumption a shortest path from $V(P_{2})$ to $V(P_{i})$ for
$i\in\\{1,3\\}$ does not intersect $V(P_{4-i})$, certifying that $A_{2}$ is
adjacent to $A_{i}$). ∎

We will below let $s_{1},s_{2},s_{3}$ and $c_{1},c_{2},c_{3}$ denote the
orderings of the respective sets, as prescribed by Claim 3.4.

######  Claim 3.5.

Let $X\subseteq B$ be such that $|X|\in\\{1,2\\}$. Any connected component of
$G[B\setminus X]$ contains at least one of the vertices $c_{1},c_{2},c_{3}$.

###### Proof.

$G-X$ is connected by $3$-connectivity of $G$. Thus for any $v\in B\setminus
X$ there exists a shortest path from $v$ to $(A\cap B)\setminus X$ in $G-X$.
By minimality, this path is contained in $B$. Hence $v$ is in the same
connected component of $G[B\setminus X]$ as the end-point of this path. ∎

######  Claim 3.6.

If $G[B]$ has a cut-vertex, then $G[B]$ has a planar embedding with $A\cap B$
on its outerface.

###### Proof.

Let $x$ be a cut-vertex in $G[B]$. By Claim 3.5, one of $c_{1},c_{2},c_{3}$
has to be in a connected component of $G[B\setminus\\{x\\}]$ that does not
contain the other two vertices. We may w.l.o.g. assume that $c_{1}$ has this
property. As each vertex in $G[B\setminus\\{x,c_{1}\\}]$ is in the same
connected component as $c_{2}$ or $c_{3}$, it follows that $c_{1}$ is isolated
in $G[B\setminus\\{x\\}]$, hence $x$ is the only neighbor of $c_{1}$ in
$G[B]$.

It is straight-forward to see that $(A\cup\\{c_{1}\\},B\setminus\\{c_{1}\\})$
is a separation in $G$ with separator $\\{x,c_{2},c_{3}\\}$. By the induction
hypothesis, $G[B\setminus\\{c_{1}\\}]$ has a planar embedding with
$x,c_{2},c_{3}$ on the outerface, which by adding $c_{1}$ to the outerface of
the embedding and connecting it to $x$ can be extended to a planar embedding
of $G[B]$ with $c_{1},c_{2},c_{3}$ on the outerface.

∎

It remains to consider the case where $G[B]$ is 2-connected and $|B|\geq 5$.
For this we will use Theorem 2.2.

Let $s_{4}\in S\cap(B\setminus A)$ (such a vertex exists since $S$ is spread
out in $G$). Observe that $G[B]$ has no $K_{4}$-minor rooted at
$\\{c_{1},c_{2},c_{3},s_{4}\\}$ as then using Claim 3.4 we could immediately
extend it to a $K_{4}$-minor rooted at $S$ (replace any occurrence of a vertex
$c_{i}$ in a branch-set by the connected set $A_{i}\supseteq\\{s_{i},c_{i}\\}$
in $A$). Hence, $G[B]$ must satisfy either Cases $(1)$ or $(2)$ of Theorem
2.2.

Let us first consider Case $(1)$. Then $G[B]$ is a spanning subgraph of a
$\\{c_{1},c_{2},c_{3},s_{4}\\}$-web $H^{+}$. Concretely, $H$ is a planar graph
that admits a planar embedding with outerface $\\{c_{1},c_{2},c_{3},s_{4}\\}$
(in some possibly permuted order) and such that every triangle $T$ in $H$
forms a face in this embedding. Further, for every triangle $T$ in $H$ there
is a disjoint (possibly empty) set $C_{T}$ of vertices in $H^{+}$ such that
$H^{+}$ is formed from $H$ by making $C_{T}$ a clique fully connected to the
three vertices of $T$ for every triangle $T$.

Now note that for every triangle $T$ in $H$ for which $C_{T}\neq\emptyset$, we
have that $(V(H),V(T)\cup C_{T})$ forms a separation of order $3$ in $G[B]$
with separator $V(T)$. Further, $(A\cup V(H),V(T)\cup C_{T})$ is a separation
of order $3$ in the whole graph $G$. Since $H$ contains at least $4$ vertices,
we have $|V(T)\cup C_{T}|<|B|$ for every triangle $T$ in $H$ and now the
inductive assumption implies that $G[V(T)\cup C_{T}]$ admits a planar
embedding with $V(T)$ on its outerface, for every triangle $T$ in $H$. It is
now easy to see that we can take the planar embedding of $H$ as prescribed
above, and for each triangular face $T$ with $C_{T}\neq\emptyset$ glue into it
an embedding of $G[V(T)\cup C_{T}]$ with $V(T)$ on its outerface, to overall
reach a planar embedding with $c_{1},c_{2},c_{3}$ (and in fact also $s_{4}$)
on its outerface. After deleting some edges from this embedding we reach a
planar embedding of $G[B]$ with $c_{1},c_{2},c_{3}$ on the outerface. This is
the desired outcome and concludes the proof in this case.

It only remains to consider Case $(2)$. By Claims 3.3 and 3.6 we may assume
that $G[B]$ is $2$-connected. Let $\\{x,y\\}\subseteq B$ be the prescribed cut
such that $G[B\setminus\\{x,y\\}]$ has at least $3$ distinct connected
components. As by Claim 3.5, any connected component of
$G[B\setminus\\{x,y\\}]$ contains a vertex among $c_{1},c_{2},c_{3}$, we
conclude that $G[B\setminus\\{x,y\\}]$ has exactly three connected components
$C_{1},C_{2},C_{3}$ where we may w.l.o.g. assume $c_{i}\in C_{i}$ for
$i=1,2,3$.

To conclude the induction proof, we will show that these assumptions are
sufficient to find branch sets $c_{1}\in B_{1},c_{2}\in B_{2},c_{3}\in
B_{3},s_{4}\in B_{4}\subseteq B$ such that any pair of sets except for
possibly $B_{2}$ and $B_{3}$ are adjacent. Combining this with Claim 3.4, this
would imply the existence of an $S$-rooted $K_{4}$-minor (with branch-sets
$A_{1}\cup B_{1},A_{2}\cup B_{2},A_{3}\cup B_{3}$ and $B_{4}$), hence
concluding the proof.

As $G[B]$ is $2$-connected, there exist for each $i=1,2,3$ two internally
disjoint paths $P_{i},Q_{i}$ in $G[B]$ with endpoints $c_{i},x$ and $c_{i},y$,
respectively. Then as $\\{x,y\\}$ separates $C_{i}$ from the rest of $B$, we
must have $V(P_{i}),V(Q_{i})\subseteq C_{i}\cup\\{x,y\\}$. Let
$X:=\bigcup_{i=1}^{3}{(V(P_{i})\setminus\\{c_{i}\\})}$ and
$Y:=\bigcup_{i=1}^{3}{(V(Q_{i})\setminus\\{c_{i}\\})}$. Note that $G[X]$ and
$G[Y]$ are connected. If $s_{4}$ is already contained in either $X$ or $Y$,
let us w.l.o.g. assume $X$, then $B_{1}=\\{c_{1}\\}\cup
Y,B_{2}=\\{c_{2}\\},B_{3}=\\{c_{3}\\}$ and $B_{4}=X$ are vertex sets with the
desired properties. Otherwise $s_{4}$ is contained in some component $C_{i}$.
Note that by choice of $s_{4}$ it is distinct from $c_{i}$. Let $P$ be a
shortest path from $s_{4}$ to $X\cup Y$ in $G[B\setminus\\{c_{i}\\}]$. Such a
path exists as $G[B]$ is $2$-connected. Let us, w.l.o.g., assume that the end-
point of $P$ is in $X$. Then similar to before $B_{1}=\\{c_{1}\\}\cup
Y,B_{2}=\\{c_{2}\\},B_{3}=\\{c_{3}\\}$ and $B_{4}=X\cup V(P)$ have the desired
properties. This concludes the proof of Lemma 3.2. ∎

Before giving the proof of Lemma 3.1 it will be useful to observe the
following simple statement about planar graphs.

######  Lemma 3.7.

Let $G$ be a planar graph and let $S\subseteq V(G)$ be a set with $|S|\geq 4$.
Suppose that for every choice of vertices $s_{1},s_{2},s_{3},s_{4}\in S$ there
is a planar embedding of $G$ in which $s_{1},\ldots,s_{4}$ are on the boundary
of the outerface. Then the graph $G^{a}(S)$, obtained from $G$ by adding a new
vertex whose neighbors are the elements of $S$, is planar.

###### Proof.

We claim that for every 4-subset $\\{s_{1},s_{2},s_{3},s_{4}\\}\subseteq S$,
the graph $G^{a}(s_{1},s_{2},s_{3},s_{4})$, obtained by adding a new vertex to
$G$ with neighborhood $\\{s_{1},s_{2},s_{3},s_{4}\\}$, is planar. Indeed,
given a planar embedding with $s_{1},s_{2},s_{3},s_{4}$ on the outerface, we
can simply embed the new vertex in the outerface and preserve a planar
embedding. Now, suppose towards a contradiction that $G^{a}(S)$ is non-planar.
By Kuratowksi’s theorem, this means that $G^{a}(S)$ contains a subdivision of
$K_{5}$ or of $K_{3,3}$. Fix one such subdivision of a Kuratowski graph. It is
a subgraph of $G^{a}(S)$ of maximum degree at most $4$. But then it has to be
also contained in a graph $G^{a}(s_{1},s_{2},s_{3},s_{4})$ for some
$\\{s_{1},s_{2},s_{3},s_{4}\\}\subseteq S$, a contradiction, since the latter
graph is planar. ∎

###### Proof of Lemma 3.1..

Take any four vertices $s_{1},s_{2},s_{3},s_{4}\in S.$ By Theorem 2.2 it
follows that if there is no $K_{4}$-minor rooted at these four vertices, then
as $G$ is $3$-connected it must satisfy Case $(2)$ with
$s_{1},s_{2},s_{3},s_{4}$ on the outerface. Concretely, $G$ is a spanning
subgraph of an $\\{s_{1},s_{2},s_{3},s_{4}\\}$-web $H^{+}$. This means $H$ is
a graph with a planar embedding with outerface $\\{s_{1},s_{2},s_{3},s_{4}\\}$
(in some order) and every triangle $T$ in $H$ forms a face in this embedding.
Further, for every triangle $T$ in $H$ there is a disjoint set $C_{T}$ of
vertices in $H^{+}$ such that $H^{+}$ is formed from $H$ by making $C_{T}$ a
clique fully connected to the three vertices of $T$ for every triangle $T$.
Since for every triangle $T$ in $H$ we have that $(V(H),V(T)\cup C_{T})$ forms
a $3$-separation in $G$, by applying Lemma 3.2 we find for every triangle $T$
in $H$ a planar embedding of $G[V(T)\cup C_{T}]$ with $V(T)$ on the outerface.
Hence, by taking the prescribed planar embedding of $H$ and glueing for every
triangle $T$ a planar embedding of $G[V(T)\cup C_{T}]$ as above into the
corresponding face, we find a planar embedding of a supergraph of $G$ that has
$s_{1},s_{2},s_{3},s_{4}$ on the outerface. This yields a planar embedding
also of $G$ with $s_{1},\ldots,s_{4}$ on the outerface.

Since our choice of $s_{1},s_{2},s_{3},s_{4}$ was arbitrary, Lemma 3.7 implies
that $G^{a}(S)$ is planar. ∎

Equipped with Lemma 3.1 we can now present the proof of our main result.

###### Proof of Theorem 1.3.

We prove the theorem by contradiction. Suppose (reductio ad absurdum) that a
graph $G$ is a smallest counterexample (in terms of $|V(G)|$). Then
$\chi(G)=4$, and there is a colorful set $S$ of vertices in $G$ such that $G$
contains no $S$-rooted $K_{4}$-minor. We start by establishing some simple
facts concerning the connectivity of $G$.

######  Claim 3.8.

$G$ is connected.

###### Proof.

Suppose not, then there exists a partition $(A,B)$ of $V(G)$ with
$A,B\neq\emptyset$ such that no edge in $G$ connects $A$ and $B$. Then
$\chi(G[A]),\chi(G[B])\leq 4$ and $G[A]$ and $G[B]$ respectively do not
contain a $K_{4}$-minor rooted at $S\cap A$ and $S\cap B$ respectively. By
minimality of $G$, there exist proper $4$-colorings $c_{A}:A\rightarrow[4]$
and $c_{B}:B\rightarrow[4]$ such that $S\cap A$ does not contain all $4$
colors in $c_{A}$, and $S\cap B$ does not contain all $4$ colors in $c_{B}$.
By permuting colors we may assume w.l.o.g. that $c_{A}(S\cap
A)\subseteq\\{2,3,4\\}$ and $c_{B}(S\cap B)\subseteq\\{2,3,4\\}$. But then
putting together $c_{A}$ and $c_{B}$ yields a proper coloring of $G$ in which
no vertex in $S$ receives color $1$, a contradiction to $S$ being colorful. ∎

######  Claim 3.9.

$G$ is $2$-connected.

###### Proof.

Towards a contradiction, suppose there exists a separation $(A,B)$ of $G$ of
order $|A\cap B|=1$. Write $A\cap B=\\{v\\}$. Clearly,
$\chi(G[A]),\chi(G[B])\leq 4$.

Suppose first that $S\cap A=\emptyset$ or $S\cap B=\emptyset$. By symmetry, we
may assume w.l.o.g. that the latter holds, i.e. $S\subseteq A\setminus B$.
Then $G[A]$ contains no $S$-rooted $K_{4}$-minor, hence there is a proper
$4$-coloring $c_{A}:A\rightarrow[4]$ of $G[A]$ in which no vertex in $S$
receives color $1$. Let $c_{B}:B\rightarrow[4]$ be a proper $4$-coloring of
$G$. Possibly after permuting colors in $c_{B}$ we have $c_{A}(v)=c_{B}(v)$,
and then the common extension of $c_{A}$ and $c_{B}$ to $G$ forms a proper
$4$-coloring in which no vertex in $S$ receives color $1$, a contradiction.

Moving, suppose that $S\cap A\neq\emptyset\neq S\cap B$. We claim that $G[A]$
does not contain an $(S\cap A)\cup\\{v\\}$-rooted $K_{4}$-minor. Indeed, if
$G[A\cup\\{v\\}]$ contains a $K_{4}$-minor $(B_{i})_{i=1}^{4}$ rooted at
$(S\cap A)\cup\\{v\\}$, then one of the branch-sets must contain $v$ (for
otherwise $(B_{i})_{i=1}^{4}$ is an $S$-rooted $K_{4}$-minor in $G$), say
$v\in B_{1}$. By connectivity, there exists a path $P$ in $G$ connecting $v$
to a vertex in $S\cap B$, and $V(P)\subseteq B$. Then $(B_{1}\cup
V(P),B_{2},B_{3},B_{4})$ form the branch-set of an $S$-rooted $K_{4}$-minor in
$G$, a contradiction. The symmetric argument works to show that $G[B]$
contains no $(S\cap B)\cup\\{v\\}$-rooted $K_{4}$-minor.

By minimality of $G$, it follows that there exist proper $4$-colorings
$c_{A}:A\rightarrow[4]$ of $G_{A}$ and $c_{B}:B\rightarrow[4]$ of $G_{B}$ such
that $(S\cap A)\cup\\{v\\}$ and $(S\cap B)\cup\\{v\\}$ do not contain a vertex
of color $1$. Then $c_{A}(v)\neq 1\neq c_{B}(v)$, and by applying a suitable
$1$-invariant permutation of the colors in $c_{B}$ we may assume w.l.o.g. that
$c_{A}(v)=c_{B}(v)$. Now, the common extension of $c_{A}$ and $c_{B}$ is a
proper coloring of $G$ in which no vertex in $S$ receives color $1$, a
contradiction. ∎

######  Claim 3.10.

$G$ is $3$-connected.

###### Proof.

Suppose not, then there exists a separation $(A,B)$ of $G$ of order $|A\cap
B|=2$. Write $A\cap B=\\{u,v\\}$. Let us fix (arbitrarily) a proper coloring
$c:V(G)\rightarrow[4]$ of $G$. We now consider two cases depending on the
distribution of $S$ on the two sides $A$ and $B$ of the separation.

Case 1. $|S\cap A|\geq 2$ and $|S\cap B|\geq 2$. Since $G$ is $2$-connected,
by Menger’s theorem there exist two vertex-disjoint paths
$P_{u}^{A},P_{v}^{A}$ in $G$ starting in $S\cap A$ and ending at $u,v$
respectively. Similarly, there exist two disjoint paths $P_{u}^{B},P_{v}^{B}$
starting at $S\cap B$ and ending at $u$ and $v$ respectively. Clearly, the
paths $P_{u}^{A},P_{v}^{A}$ are fully contained in $G[A]$ and the paths
$P_{u}^{B},P_{v}^{B}$ are fully contained in $G[B]$. Since $G$ is
$2$-connected, it is easy to see that $G[A]$ and $G[B]$ are connected graphs,
for otherwise $u$ or $v$ would form a cut-vertex of $G$. This implies that
there exists a path $P^{A}$ in $G[A]$ and a path $P^{B}$ in $G[B]$ such that
$P^{A}$ has endpoints $p_{u}^{A}\in V(P_{u}^{A})$ and $p_{v}^{A}\in
V(P_{v}^{A})$, while $P^{B}$ has endpoints $p_{u}^{B}\in V(P_{u}^{B})$ and
$p_{v}^{B}\in V(P_{v}^{B})$. W.l.o.g. (by choosing shortest paths) we may
assume $V(P_{u}^{A})\cap V(P^{A})=\\{p_{u}^{A}\\},V(P_{v}^{A})\cap
V(P^{A})=\\{p_{v}^{A}\\}$ and $V(P_{u}^{B})\cap
V(P^{B})=\\{p_{u}^{B}\\},V(P_{v}^{B})\cap V(P^{B})=\\{p_{v}^{B}\\}$. It is
then easy to see that the sets
$(V(P_{u}^{A}),V(P_{v}^{A})\cup(V(P^{A})\setminus\\{p_{u}^{A}\\}))$ form a
$K_{2}$-minor in $G[A]$ rooted at $u,v$ and at $S$, and similarly
$(V(P_{u}^{B}),V(P_{v}^{B})\cup(V(P^{B})\setminus\\{p_{u}^{B}\\}))$ form a
$K_{2}$-minor in $G[B]$ rooted at $u,v$ and at $S$.

Consider first the case that $c(u)\neq c(v)$. Then we define $G_{A},G_{B}$ as
the graphs obtained from $G[A]$ and $G[B]$ respectively by adding an edge
between $u$ and $v$ (if it does not already exist). Since $c$ induces proper
colorings on $G_{A}$ and $G_{B}$, we have $\chi(G_{A}),\chi(G_{B})\leq 4$. Let
us further define $S_{A}:=(S\cap A)\cup\\{u,v\\},S_{B}:=(S\cap
B)\cup\\{u,v\\}$. We claim that $G_{A}$ contains no $S_{A}$-rooted
$K_{4}$-minor. Indeed, if $G_{A}$ were to contain an $S_{A}$-rooted
$K_{4}$-minor, then replacing every occurrence of $u$ or $v$ in one of its
branch-sets by the sets $V(P_{u}^{B})$ or
$V(P_{v}^{B})\cup(V(P^{B})\setminus\\{p_{u}^{B}\\})$ in $G$ respectively would
yield an $S$-rooted $K_{4}$-minor in $G$, a contradiction. A symmetric
argument shows that $G_{B}$ contains no $S_{B}$-rooted $K_{4}$-minor.

The above facts, $|V(G_{A})|,|V(G_{B})|<|V(G)|$ and the minimality assumption
on $G$ now imply that there exist proper colorings
$c_{A}:V(G_{A})\rightarrow[4]$ of $G_{A}$ and $c_{B}:V(G_{B})\rightarrow[4]$
of $G_{B}$ such that no vertex in $S_{A}$ receives color $1$ in $G_{A}$ and no
vertex in $S_{B}$ receives color $1$ in $G_{B}$. In particular,
$c_{A}(u),c_{A}(v)$ are distinct and not equal to $1$, and the same is true
for $c_{B}(u),c_{B}(v)$. Hence, after applying a $1$-invariant permutation of
$[4]$ that maps $c_{B}(u)$ to $c_{A}(u)$ and $c_{B}(v)$ to $c_{A}(v)$, we may
assume w.l.o.g. that $c_{A}(u)=c_{B}(u),c_{A}(v)=c_{B}(v)$. Now, the common
extension of $c_{A}$ and $c_{B}$ to $V(G)$ forms a proper coloring of $G$ in
which no vertex in $S$ receives color $1$. This is a contradiction to $S$
being colorful and shows that the case $c(u)\neq c(v)$ cannot occur.

Next, suppose that $c(u)=c(v)$. Then we define $G_{A}$ and $G_{B}$ as the
graphs obtained from $G[A]$ and $G[B]$ by identifying $u$ and $v$ into a new
vertex $x_{uv}$, and define $S_{A}:=S\cup\\{x_{uv}\\}$ and
$S_{B}:=S\cup\\{x_{uv}\\}$. Similar to the previous case we claim that $G_{A}$
contains no $S_{A}$-rooted $K_{4}$-minor. Indeed, if it did, then possibly
after replacing the occurence of the vertex $x_{uv}$ in one of the four
branch-sets with the set $V(P_{u}^{B})\cup V(P^{B})\cup V(P_{v}^{B})$ in $G$
yields the four branch-sets of an $S$-rooted $K_{4}$-minor in $G$, a
contradiction. A symmetric argument shows that $G_{B}$ contains no
$S_{B}$-rooted $K_{4}$-minor. Note that $c$ induces a proper $4$-coloring on
both $G_{A}$ and $G_{B}$, so that $\chi(G_{A}),\chi(G_{B})\leq 4$. These facts
imply (using the minimality of $G$ and that $G_{A}$ and $G_{B}$ are smaller
than $G$) the existence of proper $[4]$-colorings $c_{A},c_{B}$of $G_{A}$ and
$G_{B}$ respectively in which no vertex in $S_{A}$ and $S_{B}$ respectively
gets assigned color $1$. In particular, this means $c_{A}(x_{uv})\neq 1\neq
c_{B}(x_{uv})$. Hence (possibly after applying a $1$-invariant permutation of
the color-set $[4]$ in $c_{B}$ that maps $c_{B}(x_{uv})$ to $c_{A}(x_{uv})$)
we may assume w.l.o.g. that $c_{A}(x_{uv})=c_{B}(x_{uv})$. It is now easy to
see that $c^{\ast}:V(G)\rightarrow[4]$ defined by
$c^{\ast}(u):=c^{\ast}(v):=c_{A}(x_{uv})$, $c^{\ast}(x):=c_{A}(x)$ for $x\in
A\setminus\\{u,v\\}$, $c^{\ast}(x):=c_{B}(x)$ for $x\in B\setminus\\{u,v\\}$,
forms a proper $4$-coloring of $G$ in which no vertex in $S$ gets assigned
color $1$. This yields a contradiction to the fact that $S$ is colorful and
hence shows that also the case $c(u)=c(v)$ is impossible. All in all, we
conclude that Case 1 cannot occur.

Case 2. $|S\cap A|\leq 1$ or $|S\cap B|\leq 1$. W.l.o.g. we assume $|S\cap
B|\leq 1$ in the following. We denote by $P$ a path in $G[B]$ connecting $u$
and $v$ (such a path must exist, since $G$ is $2$-connected). Furthermore, if
$S\setminus A\neq\emptyset$, that is, $S\cap B=\\{s\\}$ for some $S\in
B\setminus A$, then by $2$-connectivity of $G$ and Menger’s theorem there
exist two internally disjoint paths in $G$ connecting $s$ to $u$ and $v$,
which we denote by $P_{u}$ and $P_{v}$ respectively. Clearly, $P_{u}$ and
$P_{v}$ have to be entirely contained in $G[B]$.

Moving on, let us first consider the case $c(u)=c(v)$. Let $G_{A}$ be the
graph obtained from $G[A]$ by identifying $u$ and $v$ into a single vertex
$x_{uv}$. Note that $c$ induces a proper $4$-coloring on $G_{A}$, and so
$\chi(G_{A})\leq 4$. We furthermore define a set $S_{A}$ of vertices in
$G_{A}$ as $S_{A}:=S$ if $S\cap B=\emptyset$ and $S_{A}:=S\cup\\{x_{uv}\\}$ if
$S\cap B\neq\emptyset$. We claim that $G_{A}$ does not contain an
$S_{A}$-rooted $K_{4}$-minor. In the case $S\subseteq A$, this follows since
the occurrence of $x_{uv}$ in any branch-set of an $S_{A}$-rooted
$K_{4}$-minor in $G_{A}$ can be replaced by the full set $V(P)$ in $G$, which
would result in an $S$-rooted $K_{4}$-minor in $G$, a contradiction.
Similarly, in the case $S\setminus A\neq\emptyset$ the occurrence of $x_{uv}$
in a branch-set of an $S_{A}$-rooted $K_{4}$-minor in $G_{A}$ can be replaced
by the set $V(P_{1})\cup V(P_{2})$ in $G$, again resulting in an $S$-rooted
$K_{4}$-minor in $G$, a contradiction. Hence, $G_{A}$ is $4$-colorable,
contains no $S_{A}$-rooted $K_{4}$-minor and is smaller than $G$. By
minimality of $G$ there must exist a proper coloring
$c_{A}:V(G_{A})\rightarrow[4]$ in which no vertex in $S_{A}$ receives color
$1$. Let $\pi\in S_{4}$ be a permutation with
$\pi(c(u))=\pi(c(v))=c_{A}(x_{uv})$ and such that $\pi(s)\neq 1$ in the case
that $S\setminus A\neq\emptyset$. The existence of such a $\pi$ in can be seen
as follows: Either we have $c(s)=c(u)=c(v)$, in which any choice of $\pi$ with
$\pi(c(u))=\pi(c(v))=c_{A}(x_{uv})$ automatically satisfies
$\pi(c(s))=c_{A}(x_{uv})\neq 1$, since $x_{uv}\in S_{A}$ by definition. And
otherwise if $c(s)\neq c(u)=c(v)$, we have enough freedom to choose $\pi$ such
that it maps $c(u)=c(v)$ to $c_{A}(x_{uv})$ and $c(s)$ to an element distinct
from $1$. Having found the permutation $\pi$, we can see that the coloring
$c^{\ast}$ of $G$, defined by $c^{\ast}(x):=c_{A}(x)$ if $x\in A\setminus B$,
and $c^{\ast}(x):=\pi(c(x))$ if $x\in B$, forms a proper coloring of $G$ in
which no vertex in $S$ receives color $1$. This is a contradiction to $S$
being colorful and shows that the subcase $c(u)=c(v)$ cannot occur.

Next, let us consider the case $c(u)\neq c(v)$. We let $G_{A}$ be the graph
obtained from $G[A]$ by adding an edge between $u$ and $v$ (if it not already
exists). Given our assumption on $c$, we have $\chi(G_{A})\leq 4$. We define a
set $S_{A}\subseteq V(G)$ as follows: If $S\subseteq A$, then $S_{A}:=S$. If
$S\setminus A\neq\emptyset$, then we define $S_{A}:=S\setminus\\{s\\}$ if
$c(s)\notin\\{c(u),c(v)\\}$, $S_{A}:=(S\setminus\\{s\\})\cup\\{u\\}$ if
$c(s)=c(u)$ and $S_{A}:=(S\setminus\\{s\\})\cup\\{v\\}$ if $c(s)=c(v)$. We
claim that in each case, $G_{A}$ does not contain an $S_{A}$-rooted
$K_{4}$-minor. Suppose towards a contradiction such a rooted minor
$(B_{i})_{i=1}^{4}$ exists in $G_{A}$. If $S\subseteq A$ or $S\setminus
A\neq\emptyset$ and $c(s)\notin\\{c(u),c(v)\\}$, then $S_{A}\subseteq S$, so
that we can replace any branch-set $B_{i}$ containing $u$ by the set
$B_{i}\cup(V(P)\setminus\\{v\\})$ to obtain an $S$-rooted $K_{4}$-minor in
$G$. If $S\setminus A\neq\emptyset$ and $c(s)=c(u)$, we replace any branch-set
$B_{i}$ containing $u$ by $B_{i}\cup(V(P_{1})\cup V(P_{2}))\setminus\\{v\\}$
to obtain an $S$-rooted $K_{4}$-minor in $G$. Finally, if $S\setminus
A\neq\emptyset$ and $c(s)=c(v)$, we replace any branch-set $B_{i}$ containing
$v$ by $B_{i}\cup((V(P_{1})\cup V(P_{2}))\setminus\\{u\\})$ to obtain an
$S$-rooted $K_{4}$-minor in $G$. As an $S$-rooted $K_{4}$-minor in $G$ does
not exist by initial assumption, we find that there is indeed no
$S_{A}$-rooted $K_{4}$-minor in $G_{A}$. Using the minimality of $G$ we
conclude the existence of a proper $4$-coloring $c_{A}:V(G_{A})\rightarrow[4]$
of $G_{A}$ in which no vertex in $S_{A}$ receives color $1$. Note that
$c_{A}(u)\neq c_{A}(v)$. Let $\pi:[4]\rightarrow[4]$ be a permutation such
that $\pi(c(u))=c_{A}(u),\pi(c(v))=c_{A}(v)$ and $\pi(c(s))\neq 1$ in the case
$S\setminus A\neq\emptyset$. The existence of $\pi$ can be easily seen as
follows: If $S\subseteq A$, this is obvious, as we just have to map two
distinct colors to a set of two other distinct colors. If $S\setminus
A\neq\emptyset$ and $c(s)\notin\\{c(u),c(v)\\}$, we can use the range of $4$
colors to map $c(u)$ to $c_{A}(u)$, $c(v)$ to $c_{A}(v)$ and $c(s)$ to an
element of $[4]\setminus\\{1,c_{A}(u),c_{A}(v)\\}$. If $S\setminus
A\neq\emptyset$ and $c(s)=c(u)$, then $u\in S_{A}$ ensures that
$\pi(c(s))=\pi(c(u))=c_{A}(u)\neq 1$ for any $\pi$ that maps $c(u)$ to
$c_{A}(u)$ and $c(v)$ to $c_{A}(v)$. A symmetric argument works in the case
$c(s)=c(v)$.

Having found the permutation $\pi$, consider the $[4]$-coloring $c^{\ast}$ of
$G$ defined as $c^{\ast}(x):=c_{A}(x)$ if $x\in A\setminus B$, and
$c^{\ast}(x):=\pi(c(x))$ if $x\in B$. This coloring is proper and no vertex in
$S$ is assigned color $1$. Again, this contradicts $S$ being colorful and
shows that also the assumption $c(u)\neq c(v)$ leads to a contradiction.

Since both assumptions on the colors of $u$ and $v$ eventually yield a
contradiction, we conclude that Case 2 cannot occur.

We found that neither Case 1 nor Case 2 is feasible. Thus our initial
assumption on the existence of a separation of order $2$ in $G$ must have been
wrong. $G$ is a $3$-connected graph. ∎

######  Claim 3.11.

$S$ is spread out in $G$.

###### Proof.

Towards a contradiction, suppose there exists a separation $(A,B)$ in $G$ of
order $3$ such that $S\subseteq A$.

Suppose first that $|B\setminus A|=1$. Writing $B\setminus A=\\{x\\}$, we can
see that all neighbors of the vertex $x$ in $G$ are members of the separator
$A\cap B$ of size $3$. Hence $x$ has degree at most $3$ in $G$. By initial
assumption on $(A,B)$, we have $x\notin S$. Now, consider the graph $G-x$. By
minimality of $G$, there exists a proper $[4]$-coloring of $G-x$ in which no
vertex in $S$ receives color $1$. We may extend this to a proper coloring of
$G$ by picking a color for $x$ that does not appear on its neighborhood. In
this coloring of $G$ still no vertex in $S$ receives color $1$, contradicting
that $S$ is colorful.

Next, suppose $|B\setminus A|\geq 2$. Write $\\{d_{1},d_{2},d_{3}\\}=A\cap B$
for the vertices in the separator induced by $(A,B)$. Note that since $G$ is
$3$-connected, by Menger’s theorem for every $b\in B\setminus A$ there exist
$3$ internally disjoint paths connecting $b$ to $d_{1},d_{2}$ and $d_{3}$
respectively. Clearly, these paths have to be fully contained in $G[B]$. We
now claim that for every vertex $v\in B$, at least two of $d_{1},d_{2},d_{3}$
are contained together in a common connected component of $G[B]-v$. Indeed,
pick a vertex $b\in(B\setminus A)\setminus\\{v\\}$. Since $b$ is connected to
$d_{1},d_{2},d_{3}$ by three internally disjoint paths in $G[B]$, at least two
of these paths still exist in $G[B]-v$ and thus certify that their endpoints
in $\\{d_{1},d_{2},d_{3}\\}$ are contained in a common connected component of
$G[B]-v$. Now Lemma 2.1 implies the existence of a $K_{3}$-minor in $G[B]$
rooted at $A\cap B$. Let $(D_{i})_{i=1}^{3}$ be the branch-sets of such a
rooted $K_{3}$-minor in $G[B]$ with $d_{i}\in D_{i},i=1,2,3$.

Moving on, fix any proper $4$-coloring $c:V(G)\rightarrow[4]$ of $G$. W.l.o.g.
(possibly after relabelling colors and vertices) we may assume that one of the
following three cases holds: (1) $c(d_{1})=c(d_{2})=c(d_{3})=1$, (2)
$c(d_{1})=c(d_{2})=1,c(d_{3})=2$, (3) $c(d_{1})=1,c(d_{2})=2,c(d_{3})=3$.

Case 1. $c(d_{1})=c(d_{2})=c(d_{3})=1$. Let $G_{A}$ be defined as the graph
obtained from $G[A]$ by identifying $d_{1},d_{2},d_{3}$ into a single vertex
$d_{A}$. Let $S_{A}\subseteq V(G_{A})$ be defined as $S_{A}:=S$ if
$S\cap\\{d_{1},d_{2},d_{3}\\}=\emptyset$ and $S_{A}:=S\cup\\{d_{A}\\}$ if
$S\cap\\{d_{1},d_{2},d_{3}\\}\neq\emptyset$. Note that $c$ induces a proper
$4$-coloring of $G_{A}$ by assigning color $1$ to $d_{A}$. Further, $G_{A}$
contains no $S_{A}$-rooted $K_{4}$-minor: Towards a contradiction, suppose
that $(B_{i})_{i=1}^{4}$ form branch-sets of an $S_{A}$-rooted $K_{4}$-minor
in $G_{A}$. Then either $d_{A}\notin\bigcup_{i=1}^{4}{B_{i}}$ and then
$(B_{i})_{i=1}^{4}$ form an $S$-rooted $K_{4}$-minor in $G$, a contradiction.
Otherwise, we have $d_{A}\in B_{i}$ for some $i\in[4]$ (w.l.o.g. $d_{A}\in
B_{1}$) and then $((B_{1}\setminus\\{d_{A}\\})\cup D_{1}\cup D_{2}\cup
D_{3},B_{2},B_{3},B_{4})$ are easily seen to form the branch-sets of an
$S$-rooted $K_{4}$-minor in $G$, again, a contradiction. The facts that
$\chi(G_{A})\leq 4$, that $G_{A}$ contains no $S_{A}$-rooted $K_{4}$-minor,
that $|V(G_{A})|<|V(G)|$ and the minimality assumption on $G$ now imply that
$G_{A}$ admits a proper $4$-coloring $c_{A}:V(G_{A})\rightarrow[4]$ such that
no vertex in $S_{A}$ receives color $j$, for some $j\in[4]$. Possibly after
permuting colors we may assume w.l.o.g. that $c_{A}(d_{A})=1$. But then the
coloring $c^{\ast}:V(G)\rightarrow[4]$ defined by $c^{\ast}(x):=c_{A}(x)$ for
every $x\in A\setminus B$ and $c^{\ast}(x):=c(x)$ for every $x\in B$ forms a
proper $4$-coloring of $G$ in which no vertex in $S$ receives color $j$, a
contradiction to $S$ being colorful. This shows that Case 1 cannot occur.

Case 2. $c(d_{1})=c(d_{2})=1,c(d_{3})=2$. In this case, we define $G_{A}$ as
the graph obtained from $G[A]$ by identifying only $d_{1}$ and $d_{2}$ into a
new vertex $d_{A}$ and adding an edge between $d_{A}$ and $d_{3}$ (if it does
not already exist). Again it is easy to see that the coloring $c$ induces a
proper $4$-coloring of $G_{A}$ by assigning color $1$ to $d_{A}$. Let
$S_{A}:=S$ if $S\cap\\{d_{1},d_{2}\\}=\emptyset$ and $S_{A}:=S\cup\\{d_{A}\\}$
otherwise. We claim that there is no $S_{A}$-rooted $K_{4}$-minor in $G_{A}$.
Towards a contradiction, suppose such a minor would be described by branch-
sets $(B_{i})_{i=1}^{4}$. For each $i\in[4]$, set

$B_{i}^{\ast}:=\begin{cases}B_{i},&\text{if
}B_{i}\cap\\{d_{A},d_{3}\\}=\emptyset,\cr(B_{i}\setminus\\{d_{A}\\})\cup(D_{1}\cup
D_{2}),&\text{if
}B_{i}\cap\\{d_{A},d_{3}\\}=\\{d_{A}\\},\cr(B_{i}\setminus\\{d_{3}\\})\cup
D_{3},&\text{if
}B_{i}\cap\\{d_{A},d_{3}\\}=\\{d_{3}\\},\cr(B_{i}\setminus\\{d_{A},d_{3}\\})\cup(D_{1}\cup
D_{2}\cup D_{3}),&\text{if }B_{i}\supseteq\\{d_{A},d_{3}\\}\end{cases}.$

It is then easy to see that $(B_{i}^{\ast})_{i=1}^{4}$ form an $S$-rooted
$K_{4}$-minor in $G$, a contradiction.

Given that $G_{A}$ is a $4$-colorable graph with no $S_{A}$-rooted
$K_{4}$-minor which is smaller than $G$, there must exist a proper
$4$-coloring $c_{A}:V(G_{A})\rightarrow[4]$ of $G_{A}$ such that for some
$j\in[4]$ no vertex in $S_{A}$ receives color $j$. Since necessarily
$c_{A}(d_{A})\neq c_{A}(d_{3})$ in this coloring, we may assume w.l.o.g.
(possibly after permuting colors) that $c_{A}(d_{A})=1,c_{A}(d_{3})=2$. But
then it is easy to see that $c^{\ast}:V(G)\rightarrow[4]$, defined by
$c^{\ast}(x):=c_{A}(x)$ for every $x\in A\setminus B$ and $c^{\ast}(x):=c(x)$
for every $x\in B$ forms a proper coloring of $G$ such that no vertex in $S$
receives color $j$. This is a contradiction to $S$ being colorful and shows
that also Case 2 cannot occur.

Case 3. $c(d_{1})=1,c(d_{2})=2,c(d_{3})=3$. In this final case we define a
graph $G_{A}$ on the vertex set $A$ simply by adding all the three edges
$d_{1}d_{2},d_{1}d_{3},d_{2}d_{3}$ to $G[A]$ (if they do not exist already).
Since $c$ induces a proper coloring also with the added edges, we have
$\chi(G_{A})\leq 4$. We further claim that $G_{A}$ has no $S$-rooted
$K_{4}$-minor. Indeed if it did, then we could easily obtain a $K_{4}$-minor
rooted at $S$ in $G$ by replacing each occurrence of a vertex $d_{i}$ in one
of its branch-sets by the full set $D_{i}\subseteq B$ in $G$. Hence, and by
minimality of $G$, we find that there is a proper $[4]$-coloring $c_{A}$ of
$G_{A}$ in which no vertex in $S$ receives color $j$, for some $j\in[4]$.
Since $c_{A}(d_{1}),c_{A}(d_{2}),c_{A}(d_{3})$ have to be pairwise different,
we may assume w.l.o.g. $c_{A}(d_{i})=i$ for $i=1,2,3$. However, then clearly
the coloring $c^{\ast}$ of $G$ which is the common extension of $c_{A}$ and
the restriction of $c$ to $B$ is a proper $[4]$-coloring of $G$ in which no
vertex in $S$ receives color $j$. This again is a contradiction to our
assumption that $S$ is colorful in $G$. Thus, Case 3 cannot occur as well.

As we have reached contradictions in all $3$ cases, we conclude that our
initial assumption on the existence of a $3$-separation $(A,B)$ with
$S\subseteq A$ was wrong. This proves the claim, $S$ is indeed spread out. ∎

Having established that $G$ is a $3$-connected graph and $S$ is spread out in
$G$ in the previous claims, and since $G$ has no $S$-rooted $K_{4}$-minor by
assumption, we now may apply Lemma 3.1 to $G$ (note that $|S|\geq 4$ holds
trivally, for otherwise $S$ is not colorful). We thus find that $G^{a}(S)$
(the graph obtained from $G$ by adding a new vertex adjacent to all elements
of $S$) is planar. But then the $4$-color theorem guarantees the existence of
a proper $4$-coloring of $G^{a}(S)$. Then in the induced proper $4$-coloring
of $G$, no vertex in $S$ can have the color assigned to the additional vertex
in $G^{a}(S)$. This is a contradiction to $S$ being colorful. This
contradiction shows that our initial assumption on the existence of a smallest
counterexample $G$ was wrong, and concludes the proof of Theorem 1.3. ∎

## References

  * [1] K. Appel and W. Haken,  Every planar map is four colorable, I. Discharging,  Illinois Journal of Mathematics, 21(3) (1977) 429–490.
  * [2] K. Appel, W. Haken and J. Koch,  Every planar map is four colorable, II. Reducibility,  Illinois Journal of Mathematics, 21(3) (1977) 491–567.
  * [3] M. Delcourt and L. Postle,  Reducing Linear Hadwiger’s conjecture to coloring small graphs,  arXiv preprint (2021), arXiv:2108.01633.
  * [4] L. Demasi and B. Mohar,  Four terminal planar Delta-Wye reducibility via rooted $K_{2,4}$-minors,  Proceedings of the 2015 Annual ACM-SIAM Symposium on Discrete Algorithms (SODA) (2015), 1728–1742.
  * [5] R. Diestel,  Graph Theory,  Springer GTM 173, 5th edition 2016.
  * [6] G. A. Dirac,  A property of $4$-chromatic graphs and some remarks on critical graphs,  Journal of the London Mathematical Society, 27 (1952), 85–92.
  * [7] F. Ellen Fich, A. Kündgen, M. J. Pelsmajer and R. Ramamurthi,  Graph minors and reliable single message transmission,  SIAM Journal on Discrete Mathematics, 19(4) (2005), 815–847.
  * [8] R. Fabila-Monroy and D. R. Wood,  Rooted $K_{4}$-minors,  Electronic Journal of Combinatorics, 20(2) (2013), Article No P64.
  * [9] H. Hadwiger,  Über eine Klassifikation der Streckenkomplexe,  Vierteljahrsschrift der naturforschenden Gesellschaft Zürich, 88 (1943), 133–143.
  * [10] K. Hayashi and K. Kawarabyashi,  Rooted topological minors on four vertices,  Journal of Combinatorial Theory, Series B, https://doi.org/10.1016/j.jctb.2021.05.002 (2022)
  * [11] F. Holroyd,  Strengthening Hadwiger’s conjecture,  Bulletin of the London Mathematical Society, 29 (1997), 139–144.
  * [12] M. Kriesell and S. Mohr,  Rooted complete minors in line graphs with a Kempe coloring,  Graphs and Combinatorics, 35 (2019), 551–557.
  * [13] M. Kriesell and S. Mohr,  Kempe chains and rooted minors,  arXiv preprint (2019), arXiv:1911.09998.
  * [14] S. Linusson and D. R. Wood,  Thomassen’s choosability argument revisited,  SIAM J. Discrete Math., 24(4) (2010), 1632–1637.
  * [15] D. Marx, P. Seymour and P. Wollan,  Rooted grid minors,  Journal of Combinatorial Theory, Series B, 122 (2017), 428–437.
  * [16] S. Norin, L. Postle, Z.-X. Song,  Breaking the degeneracy barrier for coloring graphs with no $K_{t}$ minor,  arXiv preprint (2020), arXiv:1910.09378.
  * [17] R. Robertson, P. Seymour and R. Thomas.  Hadwiger’s conjecture for $K_{6}$-free graphs,  Combinatorica, 13 (1993), 279–361.
  * [18] R. Robertson, D. Sanders, P. Seymour and R. Thomas.  The four-colour theorem,  Journal of Combinatorial Theory, Series B, 70(1) (1997), 2–44.
  * [19] P. Seymour,  Hadwiger’s conjecture, in:  Open Problems in Mathematics, Springer (2016), 417–437.
  * [20] K. Wagner,  Über eine Eigenschaft der ebenen Komplexe,  Mathematische Annalen (1937), 570–590.
  * [21] P. Wollan,  Extremal functions for rooted minors,  Journal of Graph Theory, 58 (2008), 159–178.