Cargando…
Mining definitions in Kissat with Kittens
Bounded variable elimination is one of the most important preprocessing techniques in SAT solving. It benefits from discovering functional dependencies in the form of definitions encoded in the CNF. While the common approach pioneered in SatELite relies on syntactic pattern matching, our new approac...
| Autores principales: | , |
|---|---|
| Formato: | Online Artículo Texto |
| Lenguaje: | English |
| Publicado: |
Springer US
2023
|
| Materias: | |
| Acceso en línea: | https://www.ncbi.nlm.nih.gov/pmc/articles/PMC10564679/ https://www.ncbi.nlm.nih.gov/pubmed/37829794 http://dx.doi.org/10.1007/s10703-023-00421-2 |