Welcome to cadical Discussions!

[arminbiere]

👋 Welcome!

We’re using Discussions as a place to connect with other members of our community. We hope that you:

• Ask questions you’re wondering about.
• Share ideas.
• Engage with other community members.
• Welcome others and are open-minded. Remember that this is a community we
  build together 💪.

To get started, comment below with an introduction of yourself and tell us about what you do with this community.

[MxaWnag]

I am a new comer for solvers, and now I want to connect the latest CaDiCal to Painless V2 for experiments, and I want to export and import learning clause in the cdcl loop, what api should I focus on？

[MxaWnag]

thank you for your suggestion on using ipasir-up. I have connected cadical to painless successfully by implementing Learner and External Propagator ,but there is still room for improvement.It would be much better if the interface can support handling with the information of shared clauses like lbd value

[m-fleury]

On the one hand, I understand your motivation to have it. On the other hand, I am not aware of any other application that requires this knowledge and it is extremely constraining as it means that have to support this and cannot change the meaning anymore (like let say replacing glue by lbd which is one off).

How did you solve the issue of variable elimination?

[MxaWnag]

I realized that I seem to have made some mistakes, ExternalPropagator doesn't seem to be able to be used to import shared learning clauses directly, you have to import propagated_elit first, is there a way to import learning clauses directly.

And i didn`t solve the issue of variable elimination.

[m-fleury]

The comment above cb_has_external_clause indicates that it should work. What is your issue exactly?

[MxaWnag]

I have tried cb_has_external_clause And cb_add_external_clause_lit but it didn`t work well, and i tried to use cb_add_reason_clause_lit .Maybe i am misunderstanding the concept, Is it enough to use cb_has_external_clause And cb_add_external_clause_lit if i want to import learning clause from other solvers?