A Satisfiability Algorithm for Sparse Depth Two Threshold Circuits

TL;DR

This paper presents a novel satisfiability algorithm for sparse depth-two threshold circuits that outperforms exhaustive search, with implications for circuit lower bounds and the complexity of related problems.

Contribution

It introduces the first nontrivial satisfiability algorithm for cn-wire depth-two threshold circuits, reducing complexity via a reduction to the Vector Domination Problem.

Findings

Algorithm achieves constant savings over exhaustive search.

First satisfiability algorithm for sparse depth-two threshold circuits.

Implications for lower bounds in circuit complexity.

Abstract

We give a nontrivial algorithm for the satisfiability problem for cn-wire threshold circuits of depth two which is better than exhaustive search by a factor 2^{sn} where s= 1/c^{O(c^2)}. We believe that this is the first nontrivial satisfiability algorithm for cn-wire threshold circuits of depth two. The independently interesting problem of the feasibility of sparse 0-1 integer linear programs is a special case. To our knowledge, our algorithm is the first to achieve constant savings even for the special case of Integer Linear Programming. The key idea is to reduce the satisfiability problem to the Vector Domination Problem, the problem of checking whether there are two vectors in a given collection of vectors such that one dominates the other component-wise. We also provide a satisfiability algorithm with constant savings for depth two circuits with symmetric gates where the total weighted fan-in is at most cn. One of our motivations is proving strong lower bounds for TC^0 circuits, exploiting the connection (established by Williams) between satisfiability algorithms and lower bounds. Our second motivation is to explore the connection between the expressive power of the circuits and the complexity of the corresponding circuit satisfiability problem.