Proving circuit lower bounds using SAT solvers
Supervisors
Suitable for
Abstract
We would be happy to supervise a project on SAT solving of circuit lower bounds.
The goal of the project is to experimentally verify simple finitistic versions of important conjectures in the theory of computation.
Proving lower bounds on size of circuits computing explicit Boolean functions is one of the most fundamental problems in the
theory of computation, underlying questions such as the famous P versus NP problem. Intuitively, the task of proving a circuit
lower bound can be described as follows: given an explicit Boolean function show that it cannot be computed by a small circuit
(assuming it is indeed the case). This fundamental problem has strong connections to cryptography and learning algorithms.
Circuit lower bounds have been, however, notoriously difficult to prove. For these reasons we would like to check out if computers
could help us to gain some insight into the problem.
As a first step, we will verify if the existing class of algorithms known as SAT solvers could be used for this purpose. SAT
solvers are algorithms designed to decide satisfiability of propositional formulas, which turned out surprisingly powerful
in real-world applications. Circuit lower bounds can be expressed as propositional formulas as well. The project will involve
implementation of the encoding of some simple circuit lower bounds into propositional formulas and testing if SAT solvers
can resolve these formulas in a reasonable time. We expect that SAT solvers will be able to solve only very simple cases of
the problem. In general, the problem is expected to be hard for all SAT solvers. More advanced directions could involve modifications
of SAT solvers with new heuristics. In principle, this approach could also lead us to a construction of new
learning algorithms.