Second-Order Propositional Satisfiability

TL;DR

This paper introduces a new decidable fragment of second-order logic called Second-Order SAT, which captures many program analysis problems and is solvable with a decision procedure based on program synthesis, showing practical tractability.

Contribution

It defines Second-Order SAT as a decidable fragment of second-order logic, provides complexity analysis, and develops a decision procedure demonstrating practical applicability.

Findings

Second-Order SAT is NEXPTIME-complete.

The decision procedure is effective for various program analysis problems.

Experimental results suggest tractability for real-world applications.

Abstract

Fundamentally, every static program analyser searches for a proof through a combination of heuristics providing candidate solutions and a candidate validation technique. Essentially, the heuristic reduces a second-order problem to a first-order/propositional one, while the validation is often just a call to a SAT/SMT solver. This results in a monolithic design of such analyses that conflates the formulation of the problem with the solving process. Consequently, any change to the latter causes changes to the whole analysis. This design is dictated by the state of the art in solver technology. While SAT/SMT solvers have experienced tremendous progress, there are barely any second-order solvers. This paper takes a step towards addressing this situation by proposing a decidable fragment of second-order logic that is still expressive enough to capture numerous program analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We refer to the satisfiability problem for this fragment as Second-Order SAT and show it is NEXPTIME-complete. Finally, we build a decision procedure for Second-Order SAT based on program synthesis and present experimental evidence that our approach is tractable for program analysis problems.