We prove that every cyclically 4-edge-connected cubic graph that can be embedded in the torus, with the exception of two specific infinite families of “Petersen-like” graphs, is 3-edge-colorable. This shows that every toroidal snark can be obtained from several copies of the Petersen graph using the dot product operation. The first two snarks in this family are the Petersen graph and one of the Blanuša snarks; the rest were exposed by Belcastro and Kaminski and by Vodopivec. This proves a strengthening of the well-known, long-standing conjecture of Grünbaum from 1968.

We prove that every cyclically 4-edge-connected cubic graph that can be embedded in the projective plane, with the single exception of the Petersen graph, is 3-edge-colorable. In other words, the only (nontrivial) snark that can be embedded in the projective plane is the Petersen graph. This implies that a 2-connected cubic (multi)graph that can be embedded in the projective plane is not 3-edge-colorable if and only if it can be obtained from the Petersen graph by replacing each vertex by a 2-edge-connected planar cubic (multi)graph. Here, a replacement of a vertex$v$in a cubic graph$G$is the operation that takes a 2-connected planar (cubic) multigraph$H$containing some vertex$u$of degree 3, unifying$G-v$and$H-u$, and connecting the vertices in$N_{G}[v]$in$G-v$with the three neighbors of$u$in$H-u$with 3 edges. Any graph obtained in such a way is said to be Petersen-like. This result is a nontrivial generalization of the Four Color Theorem, and its proof requires a combination of extensive computer verification and computer-free extension of existing proofs on colorability. Using this result, we obtain the following algorithmic consequence. Input: A cubic graph$G$. Output: Either a 3-edge-coloring of$G$, an obstruction showing that$G$is not 3-edge-colorable, or the conclusion that$G$cannot be embedded in the projective plane (certified by exposing a forbidden minor for the projective plane contained in$G$). Time complexity:$O(n^{2})$, where$n=\vert V(G)\vert$. An unexpected consequence of this result is a coloring-flow duality statement for the projective plane: A cubic graph embedded in the projective plane is 3-edge-colorable if and only if its dual multigraph is 5-vertex-colorable. Moreover, we show that a 2-edge connected graph embedded in the projective plane admits a nowhere-zero 4-flow unless it is Petersen-like (in which case it does not admit nowhere-zero 4-flows). This proves a strengthening of the Tutte 4-flow conjecture for graphs on the projective plane. Some of our proofs require extensive computer verification. The necessary source codes, together with the input and output files and the complete set of more than 5000 reducible configurations, are available on Github11https://github.com/edge-coloring. Refer to the “README.md” file in each directory for instructions on how to run each program. which can be considered as an addendum to this paper. Moreover, we provide pseudocodes for all our computer verifications.

SAT solvers are widely used to solve many industrial problems because of their high performance, which is achieved by various heuristic methods. Understanding why these methods are effective is essential to improving them. One approach to this is analyzing them using qualitative measurements. In our previous study, we proposed search similarity index (SSI), a metric to quantify the similarity between searches. SSI significantly improved the performance of the parallel SAT solver. Here, we apply SSI to analyze the effect of restart, a key SAT solver technique. Experiments using SSI reveal the correlation between the difficulty of instances and the search change effect by restart, and the reason behind the effectiveness of the state-of-the-art restart method is also explained.

We consider the following general graph clustering problem: given a complete undirected graph G=(V,E,c) with an edge weight function c:E->Q, we are asked to find a partition C of V that maximizes the sum of edge weights within the clusters in C. Owing to its high generality, this problem has a wide variety of real-world applications, including correlation clustering, group technology, and community detection. In this study, we investigate the design of mathematical programming formulations and constraint satisfaction formulations for the problem. First, we present a novel integer linear programming (ILP) formulation that has far fewer constraints than the standard ILP formulation by Groetschel and Wakabayashi (1989). Second, we propose an ILP-based exact algorithm that solves an ILP problem obtained by modifying our above ILP formulation and then performs simple post-processing to produce an optimal solution to the original problem. Third, we present maximum satisfiability (MaxSAT) counterparts of both our ILP formulation and ILP-based exact algorithm. Computational experiments using well-known real-world datasets demonstrate that our ILP-based approaches and their MaxSAT counterparts are highly effective in terms of both memory efficiency and computation time.

Recent deep learning approaches for representation learning on graphs follow a neighborhood aggregation procedure. We analyze some important properties of these models, and propose a strategy to overcome those. In particular, the range of "neighboring" nodes that a node’s representation draws from strongly depends on the graph structure, analogous to the spread of a random walk. To adapt to local neighborhood properties and tasks, we explore an architecture – jumping knowledge (JK) networks – that flexibly leverages, for each node, different neighborhood ranges to enable better structure-aware representation. In a number of experiments on social, bioinformatics and citation networks, we demonstrate that our model achieves state-of-the-art performance. Furthermore, combining the JK framework with models like Graph Convolutional Networks, GraphSAGE and Graph Attention Networks consistently improves those models’ performance.

Fueled by the increasing popularity of online social networks, social influence analysis has attracted a great deal of research attention in the past decade. The diffusion process is often modeled using influence graphs, and there has been a line of research that involves algorithmic problems in influence graphs. However, the vast size of today's real-world networks raises a serious issue with regard to computational efficiency.

Literal Block Distance (LBD) is the criterion to evaluate the quality of learnt clauses and is used as a standard technique to reserve important ones in the reduction phase of state-of-the-art SAT solvers. A LBD of a clause can be updated (decreased) during the search when it is re-evaluated at the Boolean constraint propagation phase. The update is essential to evaluate the real LBD value of a learnt clause and to enhance the solver performance. We are interested in what kind of clause tends to be updated, and we conduct a survey for them by using statistical tests. The results indicate that features of literal blocks affect the update of LBD. Moreover, we utilize the fact to save more promising learnt clauses in the reduction phase of them, and we improve the performance of the solver.