| TÃtulo : |
23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings |
| Tipo de documento: |
documento electrónico |
| Autores: |
Pulina, Luca, ; Seidl, Martina, |
| Mención de edición: |
1 ed. |
| Editorial: |
[s.l.] : Springer |
| Fecha de publicación: |
2020 |
| Número de páginas: |
XI, 538 p. 271 ilustraciones, 70 ilustraciones en color. |
| ISBN/ISSN/DL: |
978-3-030-51825-7 |
| Nota general: |
Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos. |
| Palabras clave: |
Ciencias de la Computación IngenierÃa Informática Red de computadoras Microprogramación Análisis numérico Programación lógica IngenierÃa de software TeorÃa de la Computación IngenierÃa Informática y Redes Estructuras de control y microprogramación Lógica en IA |
| Ãndice Dewey: |
40.151 |
| Resumen: |
Este libro constituye las actas de la 23.ª Conferencia Internacional sobre TeorÃa y Aplicaciones de las Pruebas de Satisfacibilidad, SAT 2020, que estaba prevista para realizarse en Alghero, Italia, del 5 al 9 de julio de 2020. Debido a la pandemia de coronavirus COVID-19, la La conferencia se llevó a cabo virtualmente. Los 25 artÃculos completos, 9 breves y 2 artÃculos presentados en este volumen fueron cuidadosamente revisados ​​y seleccionados entre 69 presentaciones. Se ocupan del SAT interpretado en un sentido amplio, incluidos avances teóricos (como algoritmos exactos, complejidad de las pruebas y otras cuestiones de complejidad), algoritmos de búsqueda prácticos, recopilación de conocimientos, detalles a nivel de implementación de solucionadores de SAT y sistemas basados ​​en SAT, codificaciones de problemas. y reformulaciones, aplicaciones (incluidos dominios de aplicación novedosos y mejoras de los enfoques existentes), asà como estudios de casos e informes sobre hallazgos basados ​​en experimentación rigurosa. . |
| Nota de contenido: |
Sorting Parity Encodings by Reusing Variables -- Community and LBD-based Clause Sharing Policy for Parallel SAT Solving -- Clause size reduction with all-UIP Learning -- Trail Saving on Backtrack -- Four Flavors of Entailment -- Designing New Phase Selection Heuristics -- On the Effect of Learned Clauses on Stochastic Local Search -- SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers -- Distributed Cube and Conquer with Paracooba -- Reproducible E cient Parallel SAT Solving -- Improving Implementation of SAT Competitions 2017-2019 Winners -- On CDCL-based Proof Systems with the Ordered Decision Strategy -- Equivalence Between Systems Stronger Than Resolution -- Simplified and Improved Separations Between Regular and General Resolution by Lifting -- Mycielski graphs and PR proofs -- Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems -- Towards a Complexity-theoretic Understanding of Restarts in SAT solvers -- On the Sparsityof XORs in Approximate Model Counting -- A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth -- Abstract Cores in Implicit Hitting Set MaxSat Solving -- MaxSAT Resolution and SubCube Sums -- A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints -- On Weakening Strategies for PB Solvers -- Reasoning About Strong Inconsistency in ASP -- Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology -- Reducing Bit-Vector Polynomials to SAT using Groebner Bases -- Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions -- Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths -- Short Q-Resolution Proofs with Homomorphisms -- Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness -- Positional Games and QBF: The Corrective Encoding -- Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles -- Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits -- SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing -- SAT-based Encodings for Optimal Decision Trees with Explicit Paths -- Incremental Encoding of Pseudo-Boolean Goal Functions based on Comparator Networks. . |
| En lÃnea: |
https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] |
| Link: |
https://biblioteca.umanizales.edu.co/ils/opac_css/index.php?lvl=notice_display&i |
23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings [documento electrónico] / Pulina, Luca, ; Seidl, Martina, . - 1 ed. . - [s.l.] : Springer, 2020 . - XI, 538 p. 271 ilustraciones, 70 ilustraciones en color. ISBN : 978-3-030-51825-7 Libro disponible en la plataforma SpringerLink. Descarga y lectura en formatos PDF, HTML y ePub. Descarga completa o por capítulos.
| Palabras clave: |
Ciencias de la Computación IngenierÃa Informática Red de computadoras Microprogramación Análisis numérico Programación lógica IngenierÃa de software TeorÃa de la Computación IngenierÃa Informática y Redes Estructuras de control y microprogramación Lógica en IA |
| Ãndice Dewey: |
40.151 |
| Resumen: |
Este libro constituye las actas de la 23.ª Conferencia Internacional sobre TeorÃa y Aplicaciones de las Pruebas de Satisfacibilidad, SAT 2020, que estaba prevista para realizarse en Alghero, Italia, del 5 al 9 de julio de 2020. Debido a la pandemia de coronavirus COVID-19, la La conferencia se llevó a cabo virtualmente. Los 25 artÃculos completos, 9 breves y 2 artÃculos presentados en este volumen fueron cuidadosamente revisados ​​y seleccionados entre 69 presentaciones. Se ocupan del SAT interpretado en un sentido amplio, incluidos avances teóricos (como algoritmos exactos, complejidad de las pruebas y otras cuestiones de complejidad), algoritmos de búsqueda prácticos, recopilación de conocimientos, detalles a nivel de implementación de solucionadores de SAT y sistemas basados ​​en SAT, codificaciones de problemas. y reformulaciones, aplicaciones (incluidos dominios de aplicación novedosos y mejoras de los enfoques existentes), asà como estudios de casos e informes sobre hallazgos basados ​​en experimentación rigurosa. . |
| Nota de contenido: |
Sorting Parity Encodings by Reusing Variables -- Community and LBD-based Clause Sharing Policy for Parallel SAT Solving -- Clause size reduction with all-UIP Learning -- Trail Saving on Backtrack -- Four Flavors of Entailment -- Designing New Phase Selection Heuristics -- On the Effect of Learned Clauses on Stochastic Local Search -- SAT Heritage: a community-driven effort for archiving, building and running more than thousand SAT solvers -- Distributed Cube and Conquer with Paracooba -- Reproducible E cient Parallel SAT Solving -- Improving Implementation of SAT Competitions 2017-2019 Winners -- On CDCL-based Proof Systems with the Ordered Decision Strategy -- Equivalence Between Systems Stronger Than Resolution -- Simplified and Improved Separations Between Regular and General Resolution by Lifting -- Mycielski graphs and PR proofs -- Towards a Better Understanding of (Partial Weighted) MaxSAT Proof Systems -- Towards a Complexity-theoretic Understanding of Restarts in SAT solvers -- On the Sparsityof XORs in Approximate Model Counting -- A Faster Algorithm for Propositional Model Counting Parameterized by Incidence Treewidth -- Abstract Cores in Implicit Hitting Set MaxSat Solving -- MaxSAT Resolution and SubCube Sums -- A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints -- On Weakening Strategies for PB Solvers -- Reasoning About Strong Inconsistency in ASP -- Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology -- Reducing Bit-Vector Polynomials to SAT using Groebner Bases -- Speeding Up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions -- Strong (D)QBF Dependency Schemes via Tautology-free Resolution Paths -- Short Q-Resolution Proofs with Homomorphisms -- Multi-Linear Strategy Extraction for QBF Expansion Proofs via Local Soundness -- Positional Games and QBF: The Corrective Encoding -- Matrix Multiplication: Verifying Strong Uniquely Solvable Puzzles -- Satisfiability Solving Meets Evolutionary Optimisation in Designing Approximate Circuits -- SAT Solving with Fragmented Hamiltonian Path Constraints for Wire Arc Additive Manufacturing -- SAT-based Encodings for Optimal Decision Trees with Explicit Paths -- Incremental Encoding of Pseudo-Boolean Goal Functions based on Comparator Networks. . |
| En lÃnea: |
https://link-springer-com.biblioproxy.umanizales.edu.co/referencework/10.1007/97 [...] |
| Link: |
https://biblioteca.umanizales.edu.co/ils/opac_css/index.php?lvl=notice_display&i |
|  |
Hacer una sugerencia Refinar búsqueda23rd International Conference, Alghero, Italy, July 3–10, 2020, Proceedings / Pulina, Luca ; Seidl, Martina
