Item Infomation
Full metadata record
| DC Field | Value | Language |
|---|---|---|
| dc.contributor.author | Yong Kiam, Tan | - |
| dc.contributor.author | Marijn J. H., Heule | - |
| dc.contributor.author | Magnus O., Myreen | - |
| dc.date.accessioned | 2023-03-31T03:11:45Z | - |
| dc.date.available | 2023-03-31T03:11:45Z | - |
| dc.date.issued | 2023 | - |
| dc.identifier.uri | https://link.springer.com/article/10.1007/s10009-022-00690-y | - |
| dc.identifier.uri | https://dlib.phenikaa-uni.edu.vn/handle/PNK/7368 | - |
| dc.description | CC BY | vi |
| dc.description.abstract | 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. | vi |
| dc.language.iso | en | vi |
| dc.publisher | Springer | vi |
| dc.subject | SAT | vi |
| dc.subject | LPR | vi |
| dc.title | Verified Propagation Redundancy and Compositional UNSAT Checking in CakeML | vi |
| dc.type | Book | vi |
| Appears in Collections | ||
| OER - Công nghệ thông tin | ||
Files in This Item:
