We introduce FRAT, a new proof format for unsatisfiable SAT problems, 
and its associated toolchain. Compared to DRAT, the FRAT format allows 
solvers to include more information in proofs to reduce the computational 
cost of subsequent elaboration to LRAT. The format is easy to parse 
forward and backward, and it is extensible to future proof methods. 
The provision of optional proof steps allows SAT solver developers to 
balance implementation effort against elaboration time, with little to no 
overhead on solver time. We benchmark our FRAT toolchain against a 
comparable DRAT toolchain and confirm >84% median reduction in elaboration 
time and >94% median decrease in peak memory usage.

A Flexible Proof Format for SAT Solver-Elaborator Communication

ETAPS is a confederation of several conferences, each with its own Programme Committee and Steering Committee. ETAPS is the most important and visible annual European event related to software sciences. Altogether, more than 500 researchers participate in this event every year. The confederated conferences cover various aspects of software systems, ranging from theoretical foundations to programming language developments, compiler advancements, analysis tools, formal approaches to software engineering, and security.

A gather.town room will be open during the whole conference, which can be found here:

https://gather.town/app/nSgVv0DDYoCkmdkP/ETAPS2021

Password: Luxembourg2021

This can be used to meet in the coffee breaks.

 PDF's of the papers are available on https://etaps.org/2021/programme