search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

ICP explanations include innocent literals #56

Open danbryce opened 10 years ago

danbryce commented 10 years ago

Currently, ICP will return any literal representing a constraint that was propagated. Many of these constraints are not to blame for conflicts. It should be easy to maintain provenance so that we can return a smaller set of constraints.

What I'm imagining is maintaining a layered graph of variables and constraints. The initial layer is all the variables. We add a layer for each constraint that is propagated (results in interval shrinkage), and then a layer for each variable that is shrunk. When a constraint results in an empty interval (unsatifiability), we return any literal that is an ancestor in the provenance graph as an explanation.

This will likely include some innocent literals, but it would be an improvement.

Thoughts?

danbryce commented 10 years ago

I think what I want is the minimal(-ish) unsatisfiable core of the CSP. See: http://ebooks.iospress.nl/Download/Pdf/2661 (Extracting MUCs from Constraint Networks)

scungao commented 10 years ago

I believe we do have implemented at least part of this. It's called unsat cores in SMT as well.

I think right now if ICP only returns one constraint, that constraint should be unsat by itself, unless there's a bug?

@soonhokong please comment.

soonhokong commented 10 years ago

We have an option -new_explanation which does naive things to minimize a set of explanations. I agree that there is a lot of room for improvement.

There is another branch on my repository, https://github.com/soonhokong/dreal/tree/new_nra with which I experimented to generate smaller explanations. I almost re-implemented ICP_Solver, and it doesn't have ODE_Solver yet. When I measure the performance, it works at least twice faster than the blessed version.