Compression of sat-solver refutations of pseudo-boolean constraints

[ceilican]

Proposed by Pascal:

He (Daniel) was suggesting we studied together something about proofs for SAT, for PxTP. I proposed to look at proofs for pseudo-boolean constraints (linear constraints of the from a1 L1 + a2 L2 +... an LN >= k, where a1... an k are natural numbers, and L1... LN are propositional literals having value 0 or 1 depending on their truth value),

This is another direction for PxTP. It may be motivating also because it seems the pigeon hole problem is efficiently solved with pseudo-boolean constraints. What do you think?

[ceilican]

When we solve pseudo-boolean constraints with a sat-solver, we get a refutation of the propositional encoding of the pseudo-boolean constraints, right? It would be interesting to transform this propositional refutation into a first-order refutation of the original problem. From a human user perspective, this non-encoded refutation would be more understandable and hence more valuable. And it might be possible that this first-order refutation could be smaller than the propositional refutation.

Is this the idea that you have in mind? Or is it something else?

Assuming that this is the idea, here are some practical questions: are there pseudo-boolean constraint solvers that could solve the original problem and directly output the desired non-encoded refutation of the original problem? If yes, why would we want to do it indirectly, using a Sat-solver? Efficiency?

When I say "first-order refutation", I am intentionally ambiguous, because I think we have two options:

1) to transform the encoded Sat proof into an SMT proof (i.e. the axioms would be the pseudo-boolean constraints, and the rules would be the rules of VeriT for linear arithmetic).

2) to transform the encoded Sat proof into a "cutting planes" proof (http://www2.isye.gatech.edu/~wcook/papers/cpcomplex.pdf).

Which of these options do you have in mind? Do you see any other option?