GraphTrials: Visual Proofs of Graph Properties

TL;DR

This paper presents a framework that defines what it means to visually prove a graph property, and introduces the notion of a visual certificate, that is, a specialized faithful graph visualization that leverages the viewer’s perception, in particular, pre-attentive processing, to verify a given assertion about the represented graph.

Abstract

Graph and network visualization supports exploration, analysis and communication of relational data arising in many domains: from biological and social networks, to transportation and powergrid systems. With the arrival of AI-based question-answering tools, issues of trustworthiness and explainability of generated answers motivate a greater role for visualization. In the context of graphs, we see the need for visualizations that can convince a critical audience that an assertion about the graph under analysis is valid. The requirements for such representations that convey precisely one specific graph property are quite different from standard network visualization criteria which optimize general aesthetics and readability. In this paper, we aim to provide a comprehensive introduction to visual proofs of graph properties and a foundation for further research in the area. We present a framework that defines what it means to visually prove a graph property. In the process, we introduce the notion of a visual certificate, that is, a specialized faithful graph visualization that leverages the viewer's perception, in particular, pre-attentive processing (e.g. via pop-out effects), to verify a given assertion about the represented graph. We also discuss the relationships between visual complexity, cognitive load and complexity theory, and propose a classification based on visual proof complexity. Finally, we provide examples of visual certificates for problems in different visual proof complexity classes.

Figures (7)

• Figure 1: Our model GraphTrials identifies key processes for visually proving an assertion about a given graph in an adversarial setting. The prosecution lawyer, i. e., a software or a human (assisted by software), intends to highlight evidence for a graph being guilty of satisfying an assertion using a visual certificate drawing. To convince the judge, i. e., the human audience of the drawing, the visual certificate guides the judge's perception to form a mental model which makes the assertion easy to validate. The visual certificate must be unimpeachable as a defense lawyer (software or human adversary) checks for reasons to doubt the certificate's validity to influence the judge's verdict.
• Figure 2: Three layouts generated with yEdyed. (a) and (b) Circular and organic layouts generated with standard settings, resp. (c) Manually created layout highlighting the cut-vertex.
• Figure 3: (a)--(b) Organic layout generated with standard settings by yEdyed, with a spanning tree highlighted in (b). (c) A manually created layout highlighting the spanning tree.
• Figure 4: Four layouts of a graph with a Hamiltonian cycle (red).
• Figure 5: Visualizing $k$-colorability. (a) A bipartite graph. (b) A dense $4$-colorable graph. (c) and (d) a adjacency matrix and a node-link visualization of a sparse $4$-colorable graph.

Theorems & Definitions (3)

• Example 1
• Example 2
• Example 3