Allow C++ interface to query conflict + propagations + decisions

[horenmar]

The C++ library API, CMSat::SATSolver::print_stats() should not print gathered stats to std::cout, but rather to user provided std::ostream&. As it is now, using CMSat as a library means that either I cannot retrieve its internal statistics, or that I cannot use stdout for other output, which is a big no-no for library.

I would also like to be able to gather statistics and format them myself, but if I can get them into an internal buffer, I can always parse them internally and reformat as I see fit.

----edit---- I am willing to submit a PR if this change is welcome

[msoos]

Sure, this change is very welcome :) The print_stats() may make this not that hard, actually. Take a shot at it and if it's not perfect, I can fix it up! PR is welcome. If you don't provide one, eventually, I'll make one, but the thing is, I don't know how you'd like to provide the std::ostream&, so I'd rather let you do it. Seems like you have done this before :) Thanks a lot in advance!

[horenmar]

So I went through the code and I am no longer sure that just passing it as argument everywhere is a good idea -- there is a lot of interdependencies and basically everything seems to have multiple print methods.

Is there a global config store in cmsat?

[msoos]

There is, it's in solverconf.h. However, I have thought about this, and I'm not sure it's a good idea to have the stats being readable from the library -- it's a highly-highly changing interface. As you can see, the library functions are very sparse, because once I add something there, it should be quite stable. But stats are not very stable, there are lots of changes usually (as lots of pre-processing steps change, are added or removed). I think it may not be a good idea to depend on the stats as a library caller.

Why do you need the stats? Is there anything in particular that you'd like to export? Maybe some things I can make readable in a library-call way that I believe is stable enough? Would that be OK? Let me know (as a list perhaps) what you'd like to read out and I can maybe export them in the interface in a way that's easy and more stable? What do you think?

[horenmar]

The external interface change would be quite small, print_stats() to print_stats(std::ostream&). Internal differences would be larger though, but after thinking about it for a bit, they could be made much saner by making some of the helper functions return std::string, instead of writing to stream directly.

As to the stats, for now I care mostly about the number of conflicts/decisions (and obviously runtime, but I log that outside the sat solvers), because I want to do some modelling over various instances and see if I can map features of the original problem into good estimate of required conflicts to solve a subproblem of the original problem (that I can then use further).

However, in general I want everything I can get, so I can tune how I translate the original problem domain into SAT (ie I made a small change that leads to equisatisfiable CNF, but runtime increased by an order of magnitude, why?)

[msoos]

I can give you conflicts, time, decisions and propagations as a function call return. That's a good idea. I higly recommend not depending on anything else. Even these measures are pretty weak. The rest is essentially useless, mostly even for me. Work with these and you'll be fine. Add anything else to the mix and things will get out of hand at the slightest change of the configuration of the solver, I promise. And I will change it, I promise that too :)

Mate

On 27 Jul 2017 07:24, "Martin Hořeňovský" notifications@github.com wrote:

The external interface change would be quite small, print_stats() to print_stats(std::ostream&). Internal differences would be larger though, but after thinking about it for a bit, they could be made much saner by making some of the helper functions return std::string, instead of writing to stream directly.

As to the stats, for now I care mostly about the number of conflicts/decisions (and obviously runtime, but I log that outside the sat solvers), because I want to do some modelling over various instances and see if I can map features of the original problem into good estimate of required conflicts to solve a subproblem of the original problem (that I can then use further).

However, in general I want everything I can get, so I can tune how I translate the original problem domain into SAT (ie I made a small change that leads to equisatisfiable CNF, but runtime increased by an order of magnitude, why?)

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/msoos/cryptominisat/issues/405#issuecomment-318270531, or mute the thread https://github.com/notifications/unsubscribe-auth/ABReOeBYMfXEcafuAXe9-SP9f68WpVmzks5sSC0egaJpZM4Ohjj5 .

[horenmar]

Fair

[msoos]

OK, I'm working on it this week. Sorry, I have been making a lot of updates to the testing and other systems :)

[msoos]

Please reference

bed9129f20251cf35c01c87a99619dd749ce2f27

as the one that gives access to sum of conflicts (of all threads), props and decisions. There are tests included so you can see how it's supposed to be used. Hope it works as expected!