Satisfiability Algorithms for Restricted Circuit Classes

TL;DR

This survey reviews recent advances in satisfiability algorithms for various circuit classes, highlighting connections to circuit lower bounds and reductions to polynomial time problems, and discusses open questions in the field.

Contribution

It provides an overview of recent satisfiability algorithms for different circuit classes, emphasizing common themes, connections to lower bounds, and reductions to polynomial time problems.

Findings

Identification of common themes in satisfiability algorithms

Connections between algorithms and circuit lower bounds

Reductions from satisfiability to polynomial time problems

Abstract

In recent years, finding new satisfiability algorithms for various circuit classes has been a very active line of research. Despite considerable progress, we are still far away from a definite answer on which circuit classes allow fast satisfiability algorithms. This survey takes a (far from exhaustive) look at some recent satisfiability algorithms for a range of circuit classes and high- lights common themes. A special focus is given to connections between satisfiability algorithms and circuit lower bounds. A second focus is on reductions from satisfiability algorithms to a range of polynomial time problems, such as matrix multiplication and the Vector Domination Problem.