Cargando…
Strong Extension-Free Proof Systems
We introduce proof systems for propositional logic that admit short proofs of hard formulas as well as the succinct expression of most techniques used by modern SAT solvers. Our proof systems allow the derivation of clauses that are not necessarily implied, but which are redundant in the sense that...
Autores principales: | Heule, Marijn J. H., Kiesl, Benjamin, Biere, Armin |
---|---|
Formato: | Online Artículo Texto |
Lenguaje: | English |
Publicado: |
Springer Netherlands
2019
|
Materias: | |
Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7089731/ https://www.ncbi.nlm.nih.gov/pubmed/32226181 http://dx.doi.org/10.1007/s10817-019-09516-0 |
Ejemplares similares
-
Mycielski Graphs and [Formula: see text] Proofs
por: Yolcu, Emre, et al.
Publicado: (2020) -
Generating Extended Resolution Proofs with a BDD-Based SAT Solver
por: Bryant, Randal E., et al.
Publicado: (2021) -
A Flexible Proof Format for SAT Solver-Elaborator Communication
por: Baek, Seulkee, et al.
Publicado: (2021) -
Sorting Parity Encodings by Reusing Variables
por: Chew, Leroy, et al.
Publicado: (2020) -
cake_lpr: Verified Propagation Redundancy Checking in CakeML
por: Tan, Yong Kiam, et al.
Publicado: (2021)