Author name cluster

Tomohiro Sonobe

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

SAT Conference 2024 Conference Paper

Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem

Yoichiro Iida
Tomohiro Sonobe
Mary Inaba

Parallelization of SAT solvers is an important technique for improving solver performance. The selection of the learnt clauses to share among parallel workers is crucial for its efficiency. Literal block distance (LBD) is often used to evaluate the quality of clauses to select. We propose a new method, Parallel Clause sharing based on graph Structure (PaCS), to select good clauses for sharing. First, we conducted three preliminary experiments to assess the performance of LBD in parallel clause sharing: a performance comparison between the LBD and clause size, an analysis of the utilization of shared clauses, and a comparison of the LBD values of shared clauses at originating and receiving workers. These experiments indicate that the LBD may not be optimal for learnt clause sharing. We attribute the results to the LBD’s inherent dependency on decision trees. Each parallel worker has a unique decision tree; thus, a sharing clause that is good for its originating worker may not be good for others. Therefore, we propose PaCS, a search-independent method that uses the graph structure derived from the input CNF of SAT problems. PaCS evaluates clauses using their edges' weight in the variable incidence graph. Using the input CNF’s graph is effective for parallel clause sharing because it is the common input for all parallel workers. Furthermore, using edge weight can select clauses whose variables' Boolean values are more likely to be determined. Performance evaluation experiments demonstrate that our strategy outperforms LBD by 4% in the number of solved instances and by 12% in PAR-2. This study opens avenues for further improvements in parallel-solving strategies using the structure of SAT problems and reinterpretations of the quality of learnt clauses.

Details

FOCS Conference 2024 Conference Paper

Three-Edge-Coloring Projective Planar Cubic Graphs: A Generalization of the Four Color Theorem

Yuta Inoue
Ken-ichi Kawarabayashi
Atsuyuki Miyashita
Bojan Mohar
Tomohiro Sonobe

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 Github 1 1 https: //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.

Details

AAAI Conference 2023 Short Paper

Understand Restart of SAT Solver Using Search Similarity Index (Student Abstract)

Yoichiro Iida
Tomohiro Sonobe
Mary Inaba

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.

PDF Details DOI

AAAI Conference 2018 Conference Paper

Exact Clustering via Integer Programming and Maximum Satisfiability

Atsushi Miyauchi
Tomohiro Sonobe
Noriyoshi Sukegawa

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 ﬁnd 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 Grötschel 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 satisﬁability (MaxSAT) counterparts of both our ILP formulation and ILP-based exact algorithm. Computational experiments using well-known realworld datasets demonstrate that our ILP-based approaches and their MaxSAT counterparts are highly effective in terms of both memory efﬁciency and computation time.

PDF Details

ICML Conference 2018 Conference Paper

Representation Learning on Graphs with Jumping Knowledge Networks

Keyulu Xu
Chengtao Li
Yonglong Tian
Tomohiro Sonobe
Ken-ichi Kawarabayashi
Stefanie Jegelka

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.

Details

SAT Conference 2014 Conference Paper

Community Branching for Parallel Portfolio SAT Solvers

Tomohiro Sonobe
Shuya Kondoh
Mary Inaba

Abstract Portfolio approach for parallel SAT solvers is known as the standard parallelisation technique. In portfolio, diversification is one of the important factors in order to enable workers (solvers) to conduct a vast search. The diversification is implemented by setting different parameters for each worker in the state-of-the-art parallel portfolio SAT solvers. However, it is difficult to combine the search parameters properly in order to avoid overlaps of search spaces between the workers For this issue, we propose a novel diversification technique, called community branching. In this method, we assign a different set (or sets) of variables (called a community) to each worker and force them to select these variables as decision variables in early decision levels. In this manner, we can avoid the overlaps of the search spaces between the workers more vigorously than the existing method. We create a graph, where a vertex corresponds to a variable and an edge stands for a relation between two variables in a same clause, and we apply a modularity-based community detection algorithm to it. The variables in a community have strong relationships, and a distributed search for different communities can benefit the whole search. Experimental results show that we could speedup an existing parallel SAT solver with our proposal.

Details