The EDA (Electronic Design Automation) Challenge focuses on the innovative EDA algorithms and aims to bridge the gap between academic research and industrial application. From an algorithmic perspective, numerous core problems in EDA applications are NP-Complete or NP-hard. Algorithms of EDA involve different fields, which could be technically divided into 4 tracks: SAT, Optimization, Industrial and Machine Learning.
The SAT track consists of decision problems that involve Boolean Algebra engines, while the optimization track considers optimization problems related to Operations Research, Combinatorial Optimization, and Mathematical Optimization. The Industrial track puts emphasis on the original problems of EDA applications and the solutions of problems in Machine Learning track will be able to make accurate predictions in various EDA scenarios. It is worth mentioning that the core problems in EDA applications usually involve more than one track.
For each track of EDA Challenge, there is an individual Academic Chair Committee composed of 2 or 3 leading scientists. The organization committee also includes an Industrial Steering Committee from various companies. See here for more details.
The FIRST event of EDA Challenge is focused on SAT track, while events involving other tracks will be announced later. The first EDA Challenge is affiliated with the 24th International Conference on Theory and Applications of Satisfiability Testing (SAT2021), which is the premier annual conference for SAT research. SAT is the first problem that was proven to be NP-complete (Cook–Levin Theorem), which means that all problems in the complexity class NP are at most as difficult to solve as SAT.
SAT solvers are widely used in a number of EDA applications, such as Equivalence Checking, formal verification, ATPG (Automatic Test Pattern Generation) and etc. The aim of EDA Challenge 2021 is to promote SAT research on EDA applications, identifying EDA problems that can be solved using SAT technology and driving the development of effective SAT techniques for EDA.
The submitted solvers will be evaluated on a benchmark containing numerous circuits. There are two types of circuits in reality: Combinatorial Circuits and Sequential Circuits. A combinatorial circuit is a generalized gate that can be abstracted as a function `f:{0,1}^N→{0,1}^M` with `N` inputs and `M` outputs. Such a circuit can always be constructed as `M` separate combinatorial circuits, each with exactly one output.
In EDA Challenge 2021, only Combinatorial Circuits with exactly one output are considered. Each circuit can be formulated as a DAG (Direct Acyclic Graph) with `N` inputs and only one output (`M=1`). There are three kinds of nodes in the DAG: input nodes, output nodes and internal nodes. Each internal node is one of seven standard logical operations, namely, `AND`, `OR`, `NOT`(also denoted by `INV`), `NAND` (NOT of AND), `NOR` (NOT of OR) and `XOR` and `NXOR` (NOT of XOR). See here for more details.
The task is to determine whether the given circuit has an assignment of its inputs that makes the output be 1 (true or SAT). If there exists such an assignment of inputs, the circuit is said to be satisfiable (SAT); otherwise, the circuit is called unsatisfiable (UNSAT). This challenge is also known as the Circuit Satisfiability (CIRCUIT-SAT) problem.
To make use of SAT solver for EDA tasks, there are two essential steps. The first step is to transfer circuits to CNFs. A good encoding of CNF, which provides useful circuit knowledge for SAT solvers, would greatly accelerate the following SAT solving. The second step is to solve the encoded CNFs efficiently. The challenge consists of two races (Fixed CNF Encoding Race and No-Limits SAT Solving Race) for the above two steps respectively. See here for more details.
The winners will share a cash bonus of 20,000 Euros:
| Fixed CNF Encoding Race | No-Limits SAT Solving Race |
| 3,000 Euros for the 1st Place Team | 4,000 Euros for the 1st Place Team |
| 2,000 Euros for the 2nd Place Team | 2,500 Euros for the 2nd Place Team |
| 1,000 Euros for the 3rd Place Team | 1,500 Euros for the 3rd Place Team |
| 100 Euros for each of Top 30 Teams[1] | 3,000 Euros for the Best CNF Encoding Prize[2] |
[1] If there were LESS than 30 submitted solvers, the total 3,000 Euros bonus would be EQUALLY awarded to all participated solvers.
[2] The Best CNF Encoding Prize is awarded to the team whose algorithm transfers the circuits to CNFs most efficiently and the result is evaluated by a virtual portfolio solver (composed of the TOP 3 SAT solvers in the Fixed CNF Encoding Race).
All times are Anywhere on Earth (AoE).
| Fixed CNF Encoding Race | |
| Beginning of Registration | June 2 24:00 |
| Solver Submission Deadline | June 17 24:00June 27 24:00 |
| Result Announcement | At the SAT Conference 2021 (July 5-9th) |
| No-Limits SAT Solving Race | |
| Beginning of Registration | At the SAT Conference 2021 (July 5-9th) |
| Solver Submission Deadline | October 15 (to be confirmed) |
| Result Announcement | To Be Announced |
For any question, please feel free to send email to hi@eda-ai.org.