Call for Verified Proof Checkers

We are looking for proposals of new proof checkers for the international SAT competitions. In case you are interested in submitting a proposal, please read the following information carefully and send your proposal by 31st of January 2023 to organizers@satcompetition.org.

Your proposal should specify a proof format and include an actual proof checker implementation for that format. Please provide an empirical evaluation of the performance of your proof checker implementation. Your proof checker should run in polynomial time in the size of the formula and proof. In this regard, your proposal should address the complexity of the proposed proof system.

The proposed checker or checker tool-chain must be formally verified. If you propose a tool chain with preprocessors, it is sufficient to verify only the relevant tools in the chain. In your proposal, you should elaborate on the verified properties and the tools or methods used to verify them. References to previous publications that support your statements are helpful.

If you have a checker or checker tool-chain and plan to formally verify it but have not yet done so, we encourage you to outline your timeline and expected completion date in your proposal. Depending on the timing of completion, we may decide whether to consider the proposal for the next SAT competition or a later one.