Skip to main content

Proving circuit lower bounds using SAT solvers

Supervisors

Suitable for

MSc in Advanced Computer Science
Mathematics and Computer Science, Part C
Computer Science and Philosophy, Part C
Computer Science, Part C
Computer Science, Part B

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.