检索结果-内蒙古大学图书馆

Discovering and certifying lower bounds for the online bin stretching problem

THEORETICAL COMPUTER SCIENCE 2022年 938卷 1-15页

作者： Bohm, Martin Simon, Bertrand Univ Wroclaw Inst Comp Sci Wroclaw Poland CNRS IN2P3 Comp Ctr Villeurbanne France

There are several problems in the theory of online computation where tight lower bounds on the competitive ratio are unknown and expected to be difficult to describe in a short form. A good example is the ONLINE BIN STRETCHING problem, in which the task is to pack the incoming items online into bins while minimizing the load of the largest bin. Additionally, the optimal load of the entire instance is known in advance. The contribution of this paper is twofold. We use the Coq proof assistant to formalize the ONLINE BIN STRETCHING problem and provide a program certifying lower bounds of this problem. Because of the size of the certificates, previously claimed lower bounds were never formally proven. To the best of our knowledge, this is the first use of a formal verification toolkit to certify a lower bound for an online problem. We also provide the first non-trivial lower bounds for ONLINE BIN STRETCHING with 6, 7 and 8 bins, and increase the best known lower bound for 3 bins. We describe in detail the algorithmic improvements which were necessary for the discovery of the new lower bounds, which are several orders of magnitude more complex.(c) 2022 Elsevier B.V. All rights reserved.

关键词： Online bin stretching Online lower bound certifying algorithms Proof assistant

来源：评论

学校读者我要写书评

暂无评论

Cyclability in graph classes?,??

引用

DISCRETE APPLIED MATHEMATICS 2022年 313卷 147-178页

作者： Crespelle, Christophe Golovach, Petr A. Univ Claude Bernard Lyon 1 INRIA Lyon France Univ Bergen Dept Informat Bergen Norway

A subset T subset of V(G) of vertices of a graph G is said to be cyclable if G has a cycle C containing every vertex of T, and for a positive integer k, a graph G is k-cyclable if every set of vertices of size at most k is cyclable. The Terminal Cyclability problem asks, given a graph G and a set T of vertices, whether T is cyclable, and the k-Cyclability problem asks, given a graph G and a positive integer k, whether G is k-cyclable. These problems are generalizations of the classical Hamiltonian Cycle problem. We initiate the study of these problems for graph classes that admit polynomial algorithms for Hamiltonian Cycle. We show that Terminal Cyclability can be solved in linear time for interval graphs, bipartite permutation graphs and cographs. Moreover, we construct certifying algorithms that either produce a solution, that is a cycle, or output a graph separator that certifies a no-answer. We use these results to show that k-Cyclability can be solved in polynomial time when restricted to the aforementioned graph classes. (c) 2022 The Author(s). Published by Elsevier B.V. This is an open access article under the CC BY license (http://***/licenses/by/4.0/).

关键词： Cyclability Interval graphs Bipartite permutation graphs Cographs certifying algorithms

来源：评论

学校读者我要写书评

暂无评论

Dichotomizing k-vertex-critical H-free graphs for H of order four

引用

DISCRETE APPLIED MATHEMATICS 2022年 312卷 106-115页

作者： Cameron, Ben Hoang, Chinh T. Sawada, Joe Univ Guelph Sch Comp Sci Guelph ON Canada Wilfrid Laurier Univ Dept Phys & Comp Sci Waterloo ON Canada

For every k > 1 and pound > 1, we prove that there is a finite number of k-vertex-critical (P2 + P1)-free pound graphs. This result establishes the existence of new polynomial-time certifying algorithms for deciding the k-colorability of (P2 + P1)-free pound graphs. Together with previous research, our result also implies the following characterization: There is a finite number of k-vertex-critical H-free graphs for H of order and for fixed k > 5 if and only if H is one of K4, P4, P2 + 2P1, or P3 + P1. We also improve the recent known result that there is a finite number of k-vertex-critical (P3 + P1)-free graphs for all k by showing that such graphs have at most 2k - 1 vertices. We use this stronger result to exhaustively generate all k-vertex-critical (P3 + P1)-free graphs for k <= 7.(c) 2021 Elsevier B.V. All rights reserved.

关键词： Graph coloring certifying algorithms

来源：评论

学校读者我要写书评

暂无评论

Certified Core-Guided MaxSAT Solving 1

引用

29th International Conference on Automated Deduction (CADE)

作者： Berg, Jeremias Bogaerts, Bart Nordstrom, Jakob Oertel, Andy Vandesande, Dieter Univ Helsinki Dept Comp Sci HIIT Helsinki Finland Vrije Univ Brussel Artificial Intelligence Lab Brussels Belgium Univ Copenhagen Copenhagen Denmark Lund Univ Lund Sweden

ISBN: (数字)9783031384998

ISBN: (纸本)9783031384998;9783031384981

In the last couple of decades, developments in SAT-based optimization have led to highly efficient maximum satisfiability (MaxSAT) solvers, but in contrast to the SAT solvers on which MaxSAT solving rests, there has been little parallel development of techniques to prove the correctness of MaxSAT results. We show how pseudo-Boolean proof logging can be used to certify state-of-the-art core-guided MaxSAT solving, including advanced techniques like structure sharing, weight-aware core extraction and hardening. Our experimental evaluation demonstrates that this approach is viable in practice. We are hopeful that this is the first step towards general proof logging techniques for MaxSAT solvers.

关键词： MaxSAT core-guided search proof logging certifying algorithms

来源：评论

学校读者我要写书评

暂无评论

A refinement on the structure of vertex-critical (P5, gem)-free graphs

引用

THEORETICAL COMPUTER SCIENCE 2023年第1期961卷

作者： Cameron, Ben Hoang, Chinh T. Kings Univ Dept Comp Sci Edmonton AB Canada Wilfrid Laurier Univ Dept Phys & Comp Sci Waterloo ON Canada

We give a new, stronger proof that there are only finitely many k-vertex-critical (P5, gem)-free graphs for all k. Our proof further refines the structure of these graphs and allows for the implementation of a simple exhaustive computer search to completely list all 6-and 7-vertex-critical (P5, gem)-free graphs. Our results imply the existence of polynomial-time certifying algorithms to decide the k-colourability of (P5, gem)-free graphs for all k where the certificate is either a k-colouring or a (k + 1)-vertex-critical induced subgraph. Our complete lists for k < 7 allow for the implementation of these algorithms for all k < 6.(c) 2023 Elsevier B.V. All rights reserved.

关键词： Graph colouring certifying algorithms Critical graph P5-free graph Gem-free graph Structural graph theory

来源：评论

学校读者我要写书评

暂无评论

Polynomial time certifying algorithms for the planar quantified integer programming problem

引用

JOURNAL OF LOGIC AND COMPUTATION 2013年第5期23卷 1017-1033页

作者： Liang, Z. Subramani, K. Worthington, J. W Virginia Univ LCSEE Morgantown WV 26508 USA

This article is concerned with the design and analysis of polynomial time algorithms for determining whether a Planar Quantified Integer Program (PQIP) is feasible. A PQIP can be described briefly as an integer program involving two variables, in which each variable can be either universally or existentially quantified. There are four types of PQIPs, depending on how the variables are quantified (existentially or universally). In this article, we present two new, simple, and efficient algorithms for the for all there exists case as well as a detailed account of the complexity of the other cases. Moreover, we discuss certification with respect to the provided algorithms.

关键词： certifying algorithms polynomial time Quantified Integer Programs constraints lattice points

来源：评论

学校读者我要写书评

暂无评论

Linear-time recognition of map graphs with outerplanar witness

引用

DISCRETE OPTIMIZATION 2018年 28卷 63-77页

作者： Mnich, Matthias Rutter, Ignaz Schmidt, Jens M. Univ Bonn Inst Informat Friedrich Ebert Allee 144 D-53113 Bonn Germany Maastricht Univ Dept Quantitat Econ POB 616 NL-6200 MD Maastricht Netherlands Karlsruhe Inst Technol Inst Theoret Informat Fach 6980 D-76128 Karlsruhe Germany Tech Univ Ilmenau Inst Math Weimarer Str 25Curiebau C210 D-98693 Ilmenau Germany

Map graphs generalize planar graphs and were introduced by Chen et al. (STOC 1998, J. ACM, 2002). They showed that the problem of recognizing map graphs is in NP by proving the existence of a planar witness graph W. Shortly after, Thorup (FOGS 1998) published a polynomial-time recognition algorithm for map graphs. However, the run time of this algorithm is estimated to be Omega(n(120)) for n-vertex graphs, and a full description of its details remains unpublished. We give a new and purely combinatorial algorithm that decides whether a graph G is a map graph having an outerplanar witness W. This is a step towards a first combinatorial recognition algorithm for general map graphs. The algorithm runs in time and space O(n + m). In contrast to Thorup's approach, it computes the witness graph W in the affirmative case. (C) 2017 Elsevier B.V. All rights reserved.

关键词： Planar graphs Map graphs certifying algorithms

来源：评论

学校读者我要写书评

暂无评论

Communication Efficient Checking of Big Data Operations 32

Communication Efficient Checking of Big Data Operations

引用

32nd IEEE International Parallel and Distributed Processing Symposium (IPDPS)

作者： Huebschle-Schneider, Lorenz Sanders, Peter Karlsruhe Inst Technol Inst Theoret Informat Karlsruhe Germany

ISBN: (纸本)9781538643686

We propose fast probabilistic algorithms with low (i.e., sublinear in the input size) communication volume to check the correctness of operations in Big Data processing frameworks and distributed databases. Our checkers cover many of the commonly used operations, including sum, average, median, and minimum aggregation, as well as sorting, union, merge, and zip. An experimental evaluation of our implementation in Thrill (Bingmann et al., 2016) confirms the low overhead and high failure detection rate predicted by theoretical analysis.

关键词： certifying algorithms checking computation communication efficiency data-parallel probabilistic algorithms

来源：评论

学校读者我要写书评

暂无评论

Forbidden induced subgraphs of normal Helly circular-arc graphs: Characterization and detection

引用

DISCRETE APPLIED MATHEMATICS 2017年第Part1期216卷 67-83页

作者： Cao, Yixin Grippo, Luciano N. Safe, Martin D. Hong Kong Polytech Univ Dept Comp Hong Kong Hong Kong Peoples R China Univ Nacl Gen Sarmiento Inst Ciencias Los Polvorines Buenos Aires Argentina

A normal Helly circular-arc graph is the intersection graph of a set of arcs on a circle of which no three or less arcs cover the whole circle. Lin et al. (2013) characterized circular-arc graphs that are not normal Helly circular-arc graphs, and used them to develop the first recognition algorithm for this graph class. As open problems, they ask for the forbidden subgraph characterization and a direct recognition algorithm for normal Helly circular-arc graphs, both of which are resolved by the current paper. Moreover, when the input is not a normal Helly circular-arc graph, our recognition algorithm finds in linear time a minimal forbidden induced subgraph as a certificate. Our approach yields also a considerably simpler algorithm for the certifying recognition of proper Helly circular-arc graphs, a subclass of normal Helly circular-arc graphs. (C) 2015 Elsevier B.V. All rights reserved.

关键词： certifying algorithms Linear-time (proper) interval graphs Chordal graphs (minimal) forbidden induced subgraphs Holes (normal, Helly, proper) circular-arc models

来源：评论

学校读者我要写书评

暂无评论

Complexity of coloring graphs without paths and cycles

引用

DISCRETE APPLIED MATHEMATICS 2017年第Part1期216卷 211-232页

作者： Hell, Pavol Huang, Shenwei Simon Fraser Univ Sch Comp Sci Burnaby BC V5A 1S6 Canada

Let P-t and C-l denote a path on t vertices and a cycle on t vertices, respectively. In this paper we study the k-coloring problem for (P-t, C-l)-free graphs. Bruce et al. (2009), and Maffray and Morel (2012) have proved that 3-colorability of P-5-free graphs has a finite forbidden induced subgraphs characterization, while Hoang et al. (2015) have shown that k-colorability of P-5-free graphs fork >= 4 does not. These authors have also shown, aided by a computer search, that 4-colorability of (P-5, C-5)-free graphs does have a finite forbidden induced subgraph characterization. We prove that for any k >= 1, the k-colorability of (P-6, C-4)-free graphs has a finite forbidden induced subgraph characterization. For k = 3 and k = 4, we provide the full lists of minimal forbidden induced subgraphs. As an application, we obtain certifying polynomial time algorithms for 3-coloring and 4-coloring (P-6, C-4)-free graphs. (Polynomial time algorithms have been previously obtained by Golovach, Paulusma, and Song, but those algorithms are not certifying.) To complement these results we show that in most other cases the k-coloring problem for (P-t, C-l)-free graphs is NP-complete. Specifically, we prove that the k-coloring problem is NP-complete for (P-t, C-l)-free graphs when - l = 5, k >= 4, and t >= 7. - l >= 6, k >= 5, and t >= 6. - l >= 6 but l not equal 7, k = 4, and t >= 7. - l >= 6 but l not equal 9, k = 4, and t >= 9. Our results almost completely classify the complexity for the cases when k >= 4, t >= 4, and identify the last few open cases. (C) 2015 Elsevier B.V. All rights reserved.

关键词： Coloring certifying algorithms Paths and cycles NP-complete Obstructions

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：