A SAT-based Resolution of Lam's Problem
In 1989, computer searches by Lam, Thiel, and Swiercz experimentally resolved Lam's problem from projective geometry$\unicode{x2014}$the long-standing problem of determining if a projective plane of order ten exists. Both the original search and an independent verification in 2011 discovered no such projective plane. However, these searches were each performed using highly specialized custom-written code and did not produce nonexistence certificates. In this paper, we resolve Lam's problem by translating the problem into Boolean logic and use satisfiability (SAT) solvers to produce nonexistence certificates that can be verified by a third party. Our work uncovered consistency issues in both previous searches$\unicode{x2014}$highlighting the difficulty of relying on special-purpose search code for nonexistence results.
Code (1)
Similar Papers 제목 키워드 기반
Mapping Low-Resolution Images To Multiple High-Resolution Images Using Non-Adversarial Mapping
Several methods have recently been proposed for the Single Image Super-Resolution (SISR) problem. The current methods assume that a single low-resolution image can only yield a single high-resolution image. In addition, …
Image Super-ResolutionSuper-ResolutionLatent Image and Video Resolution Prediction using Convolutional Neural Networks
This paper introduces a Video Quality Assessment (VQA) problem that has received little attention in the literature, called the latent resolution prediction problem. The problem arises when images or videos are upscaled …
Video Quality AssessmentVisual Question Answering (VQA)LRIP-Net: Low-Resolution Image Prior based Network for Limited-Angle CT Reconstruction
In the practical applications of computed tomography imaging, the projection data may be acquired within a limited-angle range and corrupted by noises due to the limitation of scanning conditions. The noisy incomplete pr…
CT ReconstructionMulti-Modality Image Super-Resolution using Generative Adversarial Networks
Over the past few years deep learning-based techniques such as Generative Adversarial Networks (GANs) have significantly improved solutions to image super-resolution and image-to-image translation problems. In this paper…
Image Super-ResolutionImage-to-Image TranslationSuper-ResolutionTranslationFlexER: Flexible Entity Resolution for Multiple Intents
Entity resolution, a longstanding problem of data cleaning and integration, aims at identifying data records that represent the same real-world entity. Existing approaches treat entity resolution as a universal task, ass…
Entity ResolutionGraph Neural NetworkMulti-Label ClassificationMUlTI-LABEL-ClASSIFICATION