Our research project lies at two research topics: Boolean Network Tomography and Proof Complexity and SAT Solving. Network tomography is a study of distributed algorithms whose aim is to localize corrupted components in a network based on end-to-end path measurements.The problem of detecting the maximum number of simultaneous failure nodes in a network turns out to be an interesting combinatorial problem with several real-world applications.
On the Complexity Theory side, we are looking at Proof Complexity view of Pseudo-Boolean (BP) SAT Solving. In particular we look at subsystems of cutting planes (CP) which captures reasoning with linear inequalities motivated by pseudo-Boolean proof search algorithms.
The research project will seek to explore and investigate the following:
1. Despite of the evident practical implications of failure detection in network reliability and of the recent theoretical and experimental studies on maximal identifiability, there still is lack of complete understanding of what maximizing failure node identifiability requires in terms of network properties as the topology and the monitor placement, in particular if we assume the more general routing protocols. Our work contributes to this line of research. In particular from a theoretical point of view, through a combinatorial approach we focus on studying upper and lower bounds for maximal identifiability in specific topologies. On a more applied level using our theoretical results we propose and evaluate a heuristic to boost maximal identifiability in a network and provide new estimates for maximal number of nodes whose states can be uniquely determined. Moreover we derive the necessary and sufficient conditions in terms of edge/vertex connectivity of the network topology.
2. Separations between different subsystems of CP would require major technical breakthroughs in proof complexity. In order to make significant advances in pseudo-Boolean solving one crucial aspect is to make full use of the division rule in cutting planes, and we believe that further study is a promising approach for gaining a deeper understanding of the theoretical reasoning power of pseudo-Boolean solvers implementing conflict-driven proof search.