The 8th International Workshop on Satisfiability Checking and Symbolic Computation was held on July 28, 2023, at The Arctic University of Norway (UiT) in Tromsø. It will be collocated with ISSAC 2023.
The proceedings of the workshop have been published as Volume 3455 of CEUR-WS.org. JHD has written a BiBTeX file here.
Located over 200 miles north of the Arctic Circle, Tromsø is an urban island, surrounded by beautiful nature. Life in the High North is shaped by wild nature, contrasting light and weather conditions, geographic distances and multiculturalism.
Surrounded by mountains and fjords on all sides, Tromsø is home to approximately 75,000 inhabitants, making it the second-most populated city north of the Arctic Circle. With everything a person could “need”—shopping malls, festivals, marathons, cultural venues, tourist attractions and a few movie theaters — Tromsø feels more like a small metropolitan city than a town.
UiT is the northernmost university in the world, with 18,000 students and 64 days of midnight sun.
Workshop Scope
Symbolic Computation is concerned with the efficient algorithmic determination of exact solutions to complicated mathematical problems. Satisfiability Checking has recently started to tackle similar problems but with different algorithmic and technological solutions.
The two communities share many central interests, but researchers from these two communities rarely interact. Also, the lack of common or compatible interfaces for tools is an obstacle to their fruitful combination. Bridges between the communities in the form of common platforms and road-maps are necessary to initiate an exchange, and to support and direct their interaction. The aim of this workshop is to provide an opportunity to discuss, share knowledge and experience across both communities.
Keynote Speaker:
Program
- 9:00-10:40 Session 1
- 9:00-10:00 Invited talk by Haniel Barbosa: Challenges in SMT proof production and checking for arithmetic reasoning
- 10:00-10:40 James H. Davenport and Matthew England: Iterated resultants in CAD
- 10:40-11:10 : Coffee Break
- 11:10-12:30 Session 2
- 11:10-11:50 Nicolas Faroß and Simon Schwarz: Gröbner bases for Boolean function minimization
- 11:50-12:30 Tereso del Río and Matthew England: Data augmentation for mathematical objects
- 12:30-14:00 Lunch break
- 14:00-15:40 Session 3
- 14:00-15:00 Invited talk by André Platzer: Theorem proving and computer algebra for hybrid systems
- 15:00-15:40 Christopher Brown, Zoltán Kovács, Simone Luksch, Tomas Recio, Róbert Vajda and M. Pilar Velez: Towards detection of partial truth via real geometry
- 15:40-16:10 Coffee break
- 16:10-17:30 Session 4
- 16:10-16:50 Martin Brain and Jacob Howe: Widening for systems of two variables per inequality
- 16:50-17:30 Yameen Ajani and Curtis Bright: A hybrid SAT and lattice reduction approach for integer factorization
The workshop will take place in the Scandic Ishavshotel.
Submissions and Participation
The workshop series has emerged from an H2020 FETOPEN CSA project "SC-Square", which ran from 2016 to 2018. It has been continued aiming at building bridges bewteen Satisfiability Checking and Symbolic Computation. It is open for submission and participation to everyone interested in the topics, whether or not they were members or associates of the original project.
The topics of interest include but are not limited to:
- Satisfiability Checking for Symbolic Computation
- Symbolic Computation for Satisfiability Checking
- Applications relying on both Symbolic Computation and Satisfiability Checking
- Combination of Symbolic Computation and Satisfiability Checking tools
- Quantifier elimination and decision procedures and their embedding into logic provers, including but not limited to SMT solvers, and computer algebra software
Submission guidelines
Submission implies a committment that, in case of acceptance, at least one of the authors attends and presents at the workshop. We are now accepting submissions in the following categories:
- Full papers on research, case studies or tool development should present unpublished work not submitted elsewhere (with a limit of 16 pages, not counting references)
- Extended abstracts on research, case studies or tool development should present unpublished (potentially ongoing) work not submitted elsewhere (2–4 pages, not counting references)
- Presentation-only submissions on already published work, work to be published elsewhere, or work in progress on SC-Square related open problems or future challenges. Furthermore, people from other scientific disciplines and industry and business are warmly invited to attend and describe their problems, challenges, goals, and expectations for the SC-Square community. Please submit an abstract for approval by the PC (with a limit of 2 pages).
- Posters
All submissions must be in English. Full papers and extended abstracts must and use the new CEUR-ART format. All submissions should be entered to the EasyChair system before the submission deadline. Please declare the category of your submission by prefixing the title on the EasyChair form with "FULL", "EA", "PRESENTATION", or "POSTER", respectively.
Proceedings
We have published the proceedings of the workshop as CEUR-WS proceedings covering full papers and extended abstracts.
Furthermore, there will be post-proceedings in an issue of the Springer journal Mathematics in Computer Science dedicated to the workshop. Authors of all four categories are eligible for submission of a corresponding journal article. Journal versions of full papers require at least 30% new material compared to the version originally accepted. All journal submissions will be thoroughly peer-reviewed according to the standards of the journal.
Important Dates
- Submission deadline: April 1, 2023
- Notification: May 15, 2023
- Final version due: June 15, 2023
- Workshop date: July 28, 2023
- Submission deadline for journal post-proceedings: February 29, 2024
Sponsors
- Fachgruppe Computeralgebra
- Maplesoft  
- UKRI EPSRC Project EP/T015748/1: Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition
Committees
Workshop Co-chairs
- Erika Abraham (RWTH Aachen University, Germany)
- Thomas Sturm (CNRS, France & MPI Informatics, Germany)
Program Committee
- Anna Bigatti (University of Genova, Italy)
- Curtis Bright (University of Windsor, ON, Canada)
- Martin Bromberger (MPI Informatics, Germany)
- Christopher Brown (United States Naval Academy, MD)
- James H. Davenport (University of Bath, UK)
- Matthew England (Coventry University, UK)
- Pascal Fontaine (University of Liege, Belgium)
- Juergen Gerhard (Maplesoft, Canada)
- Alberto Griggio (FBK, Italy)
- Hoon Hong (North Carolina State University, NC)
- Ilias Kotsireas (Wilfrid Laurier University & Maplesoft, ON, Canada)
- Gereon Kremer (Certora, Israel)
- Alex Ozdemir (Stanford University, CA)
- Cesare Tinelli (Iowa State University, IA)
- Christoph Wintersteiger (Microsoft Cambridge, UK)
Earlier Workshops and Their Published Proceedings
This is the 8th workshop in the series originally created by the H2020 FETOPEN CSA project "SC-Square".
- The First SC2 Workshop took place in Timisoara, Romania, in 2016. Proceedings at CEUR-WS
- The Second SC2 Workshop took place in Kaiserslautern, Germany, in 2017. Proceedings at CEUR-WS
- The Third SC2 Workshop took place in Oxford, UK, in 2018. Proceedings at CEUR-WS
- The Fourth SC2 Workshop took place in Bern, Switzerland, in 2019. Proceedings at CEUR-WS
- The Fifth SC2 Workshop was held virtially, originally to be in Paris, France, in 2020. Proceedings at CEUR-WS
- The Sixth SC2 Workshop was held virtually, originally to be in College Station, TX, in 2021.
- The Seventh SC2 Workshop took place in Haifa, Israel, in 2022.