Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis

Understand

CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems.

• The increasing popularity of these constraint problems in electronic design automation encourages studies on different SAT problems and their properties for further computational efficiency.
• There has been both theoretical and practical success of modern Conflict-driven clause learning SAT solvers, which allows solving very large industrial instances in a relatively short amount of time.
• Recently, machine learning approaches provide a new dimension to solving this challenging problem.