#	Pagina
attuale pagina	/open-h2020/projects/203540/results.html

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - SC-square (SC-square - Satisfiability Checking and Symbolic Computation: uniting two communities to solve real problems)

Teaser

Summary

In summary, this proposal was motivated by the following four main problems.

Problem 1 Disjoint communities
The two communities of Satisfiability Checking and Symbolic Computation share interests and
challenges, but they are currently not well connected: there are no common communication platforms
(journals, conferences etc.), cross-community cooperations are rare, and they do not join their forces
to offer powerful solutions to challenging industrial problems.
Problem 2 Missing research roadmap
Both communities would profit from cross-community interactions, however, the potentials are
not clearly identified. Discussions are needed on what the communities can learn from each other,
what are the common challenges which they can solve together.
Problem 3 Missing standards
Though in Satisfiability Checking the standard input language allows large benchmark sets, benchmarks for non-linear arithmetic theories are still rare, and harder to describe without ambiguity.
Problem 4 Visibility
Both areas are highly relevant in many theoretic as well as practical application domains, however, though their visibility in other areas is increasing, it still does not reflect their importance.

Why is it important for society?
Expected Impacts:
â€¢ European thought-leadership on new and emerging technologies with a strong engagement of scientists, citizens,innovators and policy makers
â€¢ Improved long-term innovation potential in Europe both from the abundance of novel ideas and the range of actors ready to take them forward
â€¢ Improved readiness across Europe to engage in silo-breaking research collaboration and to take up new research and innovation practices
â€¢ Increased take-up of long-term science and technology research results

What are the overall objectives?
The overall aim of this project is to create a new research community bridging the gap between
Satisfiability Checking and Symbolic Computation, whose members will ultimately be well
informed about both fields, and thus able to combine the knowledge and techniques of both
fields to develop new research and to resolve problems (both academic and industrial) currently
beyond the scope of either individual field.
We call the new community SC2 (SC-square in ASCII, e.g. for the web site), as it will join the communities of
Satisfiability Checking and Symbolic Computation.
O1 Build a joint SC2 community
Build a community of researchers interested in developing technologies at the boundary of the traditionally separate areas of Satisfiability Checking and Symbolic Computation.
O2 Create a research roadmap
Create a research roadmap of potentials and challenges, both to the two traditional silos of Satisfiability Checking and Symbolic Computation, but also challenges that only the new joined SC2 community
can address.
O3 Initiate SC2 standards
Create standards and benchmark libraries such that the SC2 community can share challenges and measure its progress.
O4 Increase the visibility of SC2
Disseminate research topics and results to other related research areas and to the public, with a special
focus on young researchers and aiming at gender and geographic balance.

Work performed

Work started before the project officially began, with LORIA (at their expense) hosting a meeting of LORIA/MPI/RWTH and the Coordinator. This enabled the dissemination and community building phases to hit the ground running, with the poster at ISSAC, paper at CICM, and session at CASC all accepted before the project officially started.

The first three months were largely spent in dissemination, culminating in the first workshop, very much a community-building exercise, in Timisoara in September 2016. This was also the first Project Board meeting. To save time and expense, we agreed to hold electronic, rather than physical, project boards if there was no major event to tie them to. Hence electronic Project Board meetings were held in December 2016 and March 2017. A physical one was scheduled to coincide with the second workshop in July 2017.

O1 Build a joint SC2 community Progress has undoubtedly been made here: we have held two successful workshops, with 26 and 35 attendees respectively. The special session at CASC 2016 is an example of visibility at other events, and we have had a steady flow of people wising to become associates.
O1.1 Create communication platforms. The mailing lists, both of members and, more widely, that of associates, have communicated informal news and information. The workshop proceedings have helped communicate semi-formal results, and the proposed Special Issue of the Journal of Symbolic Computation, suggested by the Editor-in-Chief after he attended our workshops, will help with more finished results.
O1.2 Initiate cooperations. There are two clear examples of inter-field coop-ration here, and one of novel applications.
* The two Italian partners (FBK and Genoa) did not know each other until the project started. The two are now co-operating, and the Genoa leader has also found new cooperations within her own department, with people who had been communicating with FBK.
* RWTH and RISC-Linz initiated a cooperation, with a talk at ICAI 2017.
* The MPI/Bath/Coventry collaboration was formed out of the requirement of Bath/MPI to plan the summer school, but led to papers at ISSAC and CASC in the applications of the techniques of all three SC2 partners to a problem in Biology.
O1.3 Strengthen research and technology transfer to industry. This is happening: we had industrial talks at the workshops, and particularly at the summer school to inspire young researchers with the challenges. In particular see Oxford\'s part in the Exploitation part of Deliverable D6.5. It has also greatly strengthened Bath\'s collaboration with Altran.
O1.4 Support scientific offspring. The Summer School had 50 attendees - double the plan. The young scientists at the partners benefit from increased cooperation and dialogue, and Maplesoft are supporting a research student to start in Bath in 2017.
O2 Create a research roadmap. The launch of SC2 has led to an increase in research in the SC2 area. The specific research prototyping exercises planned in WP 1-3 have not really begun (as planned, they are largely over summer 2017). However, we have been asked to participate in the ARCADE conference, aimed at setting the research roadmap for the Automated Deduction area. This has helped crystallise the discussions within the SC2 consortium and the early stages of the roadmapping exercise.
O3 Initiate SC2 standards This is a complex process.
O3.1 Propose input language standards. OpenMath and SMTLIB are the two standards from the two communities, but they are rather different in focus. A comparison paper has been written, and seen by the OpenMath and SC2 communities.
O3.2 Create an SC2 benchmark library. Being collected.
O4 Increase the visibility of SC2 This is happening: see the invitation to ARCADE (O2) and the many activities in the Dissemination part of Deliverable D6.5.

Final results

Progress beyond the state of the art
The state of the art was, as said, that the two communities did not talk to each
other, and indeed even within one country, and one department, did not know
of each other. This is being remedied, and we can see collaborations forming.

Expected results until the end of the project
The research prototypes being worked on over this summer should help con-
solidate the research roadmaps, as should ideas coming out of the ARCADE
initiative.