About: Mycielski Graphs and [Formula: see text] Proofs

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Mycielski Graphs and [Formula: see text] Proofs Goto Sponge NotDistinct Permalink

An Entity of Type : schema:ScholarlyArticle, within Data Space : covidontheweb.inria.fr associated with source document(s)

Attributes	Values
type	Academic Article research paper schema:ScholarlyArticle
isDefinedBy	Covid-on-the-Web dataset
has title	Mycielski Graphs and [Formula: see text] Proofs
Creator	Heule, Marijn Wu, Xinyu Yolcu, Emre
Source	PMC
abstract	Mycielski graphs are a family of triangle-free graphs [Formula: see text] with arbitrarily high chromatic number. [Formula: see text] has chromatic number k and there is a short informal proof of this fact, yet finding proofs of it via automated reasoning techniques has proved to be a challenging task. In this paper, we study the complexity of clausal proofs of the uncolorability of [Formula: see text] with [Formula: see text] colors. In particular, we consider variants of the [Formula: see text] (propagation redundancy) proof system that are without new variables, and with or without deletion. These proof systems are of interest due to their potential uses for proof search. As our main result, we present a sublinear-length and constant-width [Formula: see text] proof without new variables or deletion. We also implement a proof generator and verify the correctness of our proof. Furthermore, we consider formulas extended with clauses from the proof until a short resolution proof exists, and investigate the performance of CDCL in finding the short proof. This turns out to be difficult for CDCL with the standard heuristics. Finally, we describe an approach inspired by SAT sweeping to find proofs of these extended formulas.
has issue date	2020-06-26(xsd:dateTime)
bibo:doi	10.1007/978-3-030-51825-7_15
has license	no-cc
sha1sum (hex)	2182092a5a28a523766941ff33e355e4dd1e9bbd
schema:url	https://doi.org/10.1007/978-3-030-51825-7_15
resource representing a document's title	Mycielski Graphs and [Formula: see text] Proofs
has PubMed Central identifier	PMC7326559
schema:publication	Theory and Applications of Satisfiability Testing - SAT 2020
resource representing a document's body	covid:2182092a5a28a523766941ff33e355e4dd1e9bbd#body_text
is schema:about of	named entity 'GENERATOR' named entity 'NEW' named entity 'FORMULAS' named entity 'SHORT' named entity 'proof systems' named entity 'CDCL' named entity 'automated reasoning' named entity 'chromatic number' named entity 'triangle-free' named entity 'vertices' named entity 'CNF' named entity 'CDCL' named entity 'negation' named entity 'resolution proof' named entity 'polynomial' named entity 'CNF' named entity 'polynomial' named entity 'unit propagation' named entity 'complete graph' named entity 'isomorphic' named entity 'satisfiable' named entity 'Proof systems' named entity 'CDCL' named entity 'tautologies' named entity 'graph' named entity 'Donald Knuth' named entity 'tautology' named entity 'isomorphic' named entity 'truth values' named entity 'chromatic number' named entity 'tautologies' named entity 'PHP' named entity 'MYC' named entity 'pigeonhole principle' named entity 'proof complexity' named entity 'vertex' named entity 'vertices' named entity 'resolution proofs' named entity 'unit propagation' named entity 'quasilinear' named entity 'CNF' named entity 'inference' named entity 'unit propagation' named entity 'PHP' named entity 'proper coloring' named entity 'vertex' named entity 'search algorithm' named entity 'unsatisfiable' named entity 'unit propagation' named entity 'MYC' named entity 'chromatic number' named entity 'proof systems' named entity 'sublinear' named entity 'subgraph' named entity 'Symmetry breaking' named entity 'proof systems' named entity 'graph' named entity 'tautologies' named entity 'isomorphic' named entity 'vertices' named entity 'tautologies' named entity 'satisfiable' named entity 'graph' named entity 'graph' named entity 'subgraph' named entity 'MYC' named entity 'induced subgraph' named entity 'SAT solving' named entity 'proof systems' named entity 'chromatic number' named entity 'conjunctive normal form' named entity 'vertices' named entity 'unsatisfiable' named entity 'partition' named entity 'graph' named entity 'algorithm' named entity 'isomorphic' named entity 'CNF' named entity 'tautologies' named entity 'concatenate' named entity 'proof systems'

Faceted Search & Find service v1.13.91 as of Mar 24 2020

Alternative Linked Data Documents: Sponger | ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3229 as of Jul 10 2020, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (94 GB total memory)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software