In this paper we propose a linear programming based method to generate interpolants for two Boolean formulas
in the framework of probably approximately correct (PAC) learning. The computed interpolant is termed as a
PAC interpolant with respect to a violation level \(\epsilon \in (0,1)\) and confidence level \(\beta \in (0,1)\): with
at least \(1-\beta \) confidence, the probability that the PAC interpolant is a true interpolant is larger than \(1-\epsilon \).
Unlike classical interpolants which are used to justify that two formulas are inconsistent, the PAC interpolant is
proposed for providing a formal characterization of how inconsistent two given formulas are.
This characterization is very important, especially for situations that the two formulas cannot be proven to
be inconsistent. The PAC interpolant is computed by solving a scenario optimization problem, which can be
regarded as a statistically sound formal method in the sense that it provides formal correct guarantees expressed
using violation probabilities and confidences. The scenario optimization problem is reduced to a linear
program in our framework, which is constructed by a family of independent and identically distributed
samples of variables in the given two Boolean formulas. In this way we can synthesize interpolants for
formulas that existing methods are not capable of dealing with. Three examples demonstrate
the merits of our approach.