5 Search Results for "Banbara, Mutsunori"

Document
DOI: 10.4230/LIPIcs.ISAAC.2025.39
Reachability of Independent Sets and Vertex Covers Under Extended Reconfiguration Rules

Authors: Shuichi Hirahara, Naoto Ohsaka, Tatsuhiro Suga, Akira Suzuki, Yuma Tamura, and Xiao Zhou

Published in: LIPIcs, Volume 359, 36th International Symposium on Algorithms and Computation (ISAAC 2025)

Abstract
In reconfiguration problems, we are given two feasible solutions to a graph problem and asked whether one can be transformed into the other via a sequence of feasible intermediate solutions under a given reconfiguration rule. While earlier work focused on modifying a single element at a time, recent studies have started examining how different rules impact computational complexity. Motivated by recent progress, we study Independent Set Reconfiguration (ISR) and Vertex Cover Reconfiguration (VCR) under the k-Token Jumping (k-TJ) and k-Token Sliding (k-TS) models. In k-TJ, up to k vertices may be replaced, while k-TS additionally requires a perfect matching between removed and added vertices. It is known that the complexity of ISR crucially depends on k, ranging from PSPACE-complete and NP-complete to polynomial-time solvable. In this paper, we further explore the gradient of computational complexity of the problems. We first show that ISR under k-TJ with k = |I| - μ remains NP-hard when μ is any fixed positive integer and the input graph is restricted to graphs of maximum degree 3 or planar graphs of maximum degree 4, where |I| is the size of feasible solutions. In addition, we prove that the problem belongs to NP not only for μ = O(1) but also for μ = O(log |I|). In contrast, we show that VCR under k-TJ is in XP when parameterized by μ = |S| - k, where |S| is the size of feasible solutions. Furthermore, we establish the PSPACE-completeness of ISR and VCR under both k-TJ and k-TS on several graph classes, for fixed k as well as superconstant k relative to the size of feasible solutions.
Cite as

Shuichi Hirahara, Naoto Ohsaka, Tatsuhiro Suga, Akira Suzuki, Yuma Tamura, and Xiao Zhou. Reachability of Independent Sets and Vertex Covers Under Extended Reconfiguration Rules. In 36th International Symposium on Algorithms and Computation (ISAAC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 359, pp. 39:1-39:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hirahara_et_al:LIPIcs.ISAAC.2025.39,
  author =	{Hirahara, Shuichi and Ohsaka, Naoto and Suga, Tatsuhiro and Suzuki, Akira and Tamura, Yuma and Zhou, Xiao},
  title =	{{Reachability of Independent Sets and Vertex Covers Under Extended Reconfiguration Rules}},
  booktitle =	{36th International Symposium on Algorithms and Computation (ISAAC 2025)},
  pages =	{39:1--39:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-408-6},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{359},
  editor =	{Chen, Ho-Lin and Hon, Wing-Kai and Tsai, Meng-Tsung},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ISAAC.2025.39},
  URN =		{urn:nbn:de:0030-drops-249474},
  doi =		{10.4230/LIPIcs.ISAAC.2025.39},
  annote =	{Keywords: combinatorial reconfiguration, extended reconfiguration rule, independent set reconfiguration, vertex cover reconfiguration, PSPACE-completeness, NP-completeness}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.24
SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints

Authors: Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
In this paper, we propose an enhancement to the SAT-based counterexample-guided abstraction refinement (CEGAR) approach for solving the Hamiltonian Cycle Problem (HCP). Many SAT-based methods for HCP have been proposed, including a CEGAR-based method that repeatedly solves a relaxed version of HCP strengthened by counterexamples. However, when the counterexample space - represented by the full set of subcycle partitions - is large, it becomes difficult to find a solution. To address this, we introduce cut-set constraints in the refinement step, replacing traditional subcycle blocking constraints. Our evaluation shows that these cut-set constraints achieve equal or better reduction in the counterexample space, making it easier to find valid solutions. We further assessed performance using all 1001 instances from the FHCP challenge set and confirmed that the proposed method solved 937 instances within 1800 seconds, outperforming both the existing eager and CEGAR encodings (which solved at most 666 instances). This demonstrates the effectiveness of incorporating cut-set constraints into SAT-based CEGAR approaches.
Cite as

Ryoga Ohashi, Takehide Soh, Daniel Le Berre, Hidetomo Nabeshima, Mutsunori Banbara, Katsumi Inoue, and Naoyuki Tamura. SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 24:1-24:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{ohashi_et_al:LIPIcs.SAT.2025.24,
  author =	{Ohashi, Ryoga and Soh, Takehide and Le Berre, Daniel and Nabeshima, Hidetomo and Banbara, Mutsunori and Inoue, Katsumi and Tamura, Naoyuki},
  title =	{{SAT-Based CEGAR Method for the Hamiltonian Cycle Problem Enhanced by Cut-Set Constraints}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{24:1--24:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.24},
  URN =		{urn:nbn:de:0030-drops-237585},
  doi =		{10.4230/LIPIcs.SAT.2025.24},
  annote =	{Keywords: Hamiltonian Cycle Problem, SAT Encoding, CEGAR}
}
Document
DOI: 10.4230/LIPIcs.SAT.2025.29
Reencoding Unique Literal Clauses

Authors: Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)

Abstract
We present a lightweight reencoding technique that augments propositional formulas containing implicit or explicit exactly-one constraints with auxiliary variables derived from the order encoding. Our approach is based on the observation that many formulas contain clauses where each literal appears only in that clause, and that these unique literal clauses can be replaced by the corresponding sequential counter encoding of exactly-one constraints, which introduces the same variables as the order encoding. We implemented the reencoding in the state-of-the-art SAT solver CaDiCaL with support for proof logging and solution reconstruction. Experiments on SAT Competition benchmarks demonstrate that our technique enables solving dozens of additional formulas. We found that shuffling a formula before reencoding harms performance. To mitigate this issue, we introduce a method that sorts literals within clauses based on the formula structure before applying our reencoding. The same technique also predicts whether reencoding is likely to yield improvements.
Cite as

Aeacus Sheng, Joseph E. Reeves, and Marijn J. H. Heule. Reencoding Unique Literal Clauses. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 29:1-29:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{sheng_et_al:LIPIcs.SAT.2025.29,
  author =	{Sheng, Aeacus and Reeves, Joseph E. and Heule, Marijn J. H.},
  title =	{{Reencoding Unique Literal Clauses}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{29:1--29:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.29},
  URN =		{urn:nbn:de:0030-drops-237635},
  doi =		{10.4230/LIPIcs.SAT.2025.29},
  annote =	{Keywords: Satisfiability solving, auxiliary variables, graph coloring}
}
Document
DOI: 10.4230/LIPIcs.CPM.2023.17
Encoding Hard String Problems with Answer Set Programming

Authors: Dominik Köppl

Published in: LIPIcs, Volume 259, 34th Annual Symposium on Combinatorial Pattern Matching (CPM 2023)

Abstract
Despite the simple, one-dimensional nature of strings, several computationally hard problems on strings are known. Tackling hard problems beyond sizes of toy instances with straight-forward solutions is infeasible. To solve these problems on datasets of even small sizes, effort has to be put into the conception of algorithms leveraging profound characteristics of the input. Finding these characteristics can be eased by rapidly creating and evaluating prototypes of new concepts in how to tackle hard problems. Such a rapid-prototyping method for hard problems is answer set programming (ASP). In this light, we study the application of ASP on five NP-hard optimization problems in the field of strings. We provide MAX-SAT and ASP encodings, and empirically reason about the merits and flaws when working with ASP solvers.
Cite as

Dominik Köppl. Encoding Hard String Problems with Answer Set Programming. In 34th Annual Symposium on Combinatorial Pattern Matching (CPM 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 259, pp. 17:1-17:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{koppl:LIPIcs.CPM.2023.17,
  author =	{K\"{o}ppl, Dominik},
  title =	{{Encoding Hard String Problems with Answer Set Programming}},
  booktitle =	{34th Annual Symposium on Combinatorial Pattern Matching (CPM 2023)},
  pages =	{17:1--17:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-276-1},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{259},
  editor =	{Bulteau, Laurent and Lipt\'{a}k, Zsuzsanna},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CPM.2023.17},
  URN =		{urn:nbn:de:0030-drops-179711},
  doi =		{10.4230/LIPIcs.CPM.2023.17},
  annote =	{Keywords: optimization problems, answer set programming, MAX-SAT encoding, NP-hard string problems}
}
Document
DOI: 10.4230/LIPIcs.ICLP.2012.86
Generating Event-Sequence Test Cases by Answer Set Programming with the Incidence Matrix

Authors: Mutsunori Banbara, Naoyuki Tamura, and Katsumi Inoue

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

Abstract
The effective use of ASP solvers is essential for enhancing efficiency and scalability. The incidence matrix is a simple representation used in Constraint Programming (CP) and Integer Linear Programming for modeling combinatorial problems. Generating test cases for event-sequence testing is to find a sequence covering array (SCA). In this paper, we consider the problem of finding optimal sequence covering arrays by ASP and CP. Our approach is based on an effective combination of ASP solvers and the incidence matrix. We first present three CP models from different viewpoints of sequence covering arrays: the naïve matrix model, the event-position matrix model, and the incidence matrix model. Particularly, in the incidence matrix model, an SCA can be represented by a (0,1)-matrix called the incidence matrix of the array in which the coverage constraints of the given SCA can be concisely expressed. We then present an ASP program of the incidence matrix model. It is compact and faithfully reflects the original constraints of the incidence matrix model. In our experiments, we were able to significantly improve the previously known bounds for many arrays of strength three. Moreover, we succeeded either in finding optimal solutions or in improving known bounds for some arrays of strength four.
Cite as

Mutsunori Banbara, Naoyuki Tamura, and Katsumi Inoue. Generating Event-Sequence Test Cases by Answer Set Programming with the Incidence Matrix. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 86-97, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{banbara_et_al:LIPIcs.ICLP.2012.86,
  author =	{Banbara, Mutsunori and Tamura, Naoyuki and Inoue, Katsumi},
  title =	{{Generating Event-Sequence Test Cases by Answer Set Programming with the Incidence Matrix}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{86--97},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.86},
  URN =		{urn:nbn:de:0030-drops-36127},
  doi =		{10.4230/LIPIcs.ICLP.2012.86},
  annote =	{Keywords: Event-Sequence Testing, Answer Set Programming, Matrix Model, Constraint Programming, Propositional Satisfiability (SAT)}
}
  • Refine by Type
  • 5 Document/PDF
  • 3 Document/HTML

  • Refine by Publication Year
  • 3 2025
  • 1 2023
  • 1 2012

  • Refine by Author
  • 2 Banbara, Mutsunori
  • 2 Inoue, Katsumi
  • 2 Tamura, Naoyuki
  • 1 Heule, Marijn J. H.
  • 1 Hirahara, Shuichi
  • Show More...

  • Refine by Series/Journal
  • 5 LIPIcs

  • Refine by Classification
  • 1 Computing methodologies → Artificial intelligence
  • 1 Computing methodologies → Discrete space search
  • 1 Hardware → Theorem proving and SAT solving
  • 1 Theory of computation
  • 1 Theory of computation → Automated reasoning
  • Show More...

  • Refine by Keyword
  • 1 Answer Set Programming
  • 1 CEGAR
  • 1 Constraint Programming
  • 1 Event-Sequence Testing
  • 1 Hamiltonian Cycle Problem
  • Show More...

Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact