Cover Image

Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML

CC BY

Saved in:
Bibliographic Details
Main Authors: Yong Kiam, Tan, Marijn J. H., Heule, Magnus O., Myreen
Format: Book
Language:English
Published: Springer 2023
Subjects:
SAT
LPR
Online Access:https://link.springer.com/article/10.1007/s10009-022-00690-y
https://dlib.phenikaa-uni.edu.vn/handle/PNK/7368
Tags: Add Tag
No Tags, Be the first to tag this record!
id oai:localhost:PNK-7368
record_format dspace
spelling oai:localhost:PNK-73682023-03-31T03:11:45Z Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML Yong Kiam, Tan Marijn J. H., Heule Magnus O., Myreen SAT LPR CC BY Modern SAT solvers can emit independently-checkable proof certificates to validate their results. The state-of-the-art proof system that allows for compact proof certificates is propagation redundancy (PR ). However, the only existing method to validate proofs in this system with a formally verified tool requires a transformation to a weaker proof system, which can result in a significant blowup in the size of the proof and increased proof validation time. This article describes the first approach to formally verify PR proofs on a succinct representation. We present (i) a new Linear PR (LPR) proof format, (ii) an extension of the DPR-trim tool to efficiently convert PR proofs into LPR format, and (iii) cake_lpr, a verified LPR proof checker developed in CakeML. 2023-03-31T03:11:45Z 2023-03-31T03:11:45Z 2023 Book https://link.springer.com/article/10.1007/s10009-022-00690-y https://dlib.phenikaa-uni.edu.vn/handle/PNK/7368 en application/pdf Springer
institution Digital Phenikaa
collection Digital Phenikaa
language English
topic SAT
LPR
spellingShingle SAT
LPR
Yong Kiam, Tan
Marijn J. H., Heule
Magnus O., Myreen
Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
description CC BY
format Book
author Yong Kiam, Tan
Marijn J. H., Heule
Magnus O., Myreen
author_facet Yong Kiam, Tan
Marijn J. H., Heule
Magnus O., Myreen
author_sort Yong Kiam, Tan
title Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
title_short Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
title_full Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
title_fullStr Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
title_full_unstemmed Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML
title_sort verified propagation redundancy and compositional unsat checking in cakeml
publisher Springer
publishDate 2023
url https://link.springer.com/article/10.1007/s10009-022-00690-y
https://dlib.phenikaa-uni.edu.vn/handle/PNK/7368
_version_ 1761912524871041024
score 8.887836

Similar Items