clingcon is twice as fast with --single-shot

[MaxOstrowski]

Taking the newest clingcon dev version from conda:
The call
clingcon test.lp --stats=2 0 --single-shot
is twice as fast as
clingcon test.lp --stats=2 0
test.zip

(The number of choices and conflicts is reduced to half,
why is this the case).

@BenKaufmann @rkaminsk Just in case you are interested in an example.

Could this option be made default for clingcon binary calls? Or is it possible to do multi-shot solving within python inside the encoding.

[MaxOstrowski]

test2.zip
Here is an example, where all offline statistics (even number of frozen variables) are exactly the same.
Still 150% performance boost when using --single-shot. What is the difference here, and why aren't the calls determinstic (both the same).

Testing this instance with additionally --solve-limit=1 reveals that there is a very slight difference in binary lemmas. (2 more with --single-shot).
So either a completely different order of propagation is done, or something else is happening here (the total number of lemmas seems to stay the same?)

Also the Lemma count does not seem to add up:

Lemmas       : 334      (Deleted: 0)
  Binary     : 315      (Ratio:  94.31%)
  Ternary    : 2        (Ratio:   0.60%)
  Conflict   : 2        (Average Length:    9.0 Ratio:   0.60%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 332      (Average Length:    2.3 Ratio:  99.40%) 

Maybe its just hard to read:
We have 334 lemmas, 332 comming from clingcon propagator, 2 conflict lemmas. 2 of the total 334 lemmas are ternary, 315 binary, and therefore 334-315-2 bigger than size 3.

Given this interpretation, and a similar statistics with --single-shot:

Lemmas       : 334      (Deleted: 0)
  Binary     : 317      (Ratio:  94.91%)
  Ternary    : 2        (Ratio:   0.60%)
  Conflict   : 2        (Average Length:    9.0 Ratio:   0.60%) 
  Loop       : 0        (Average Length:    0.0 Ratio:   0.00%) 
  Other      : 332      (Average Length:    2.2 Ratio:  99.40%) 

I would conclude that with the single shot option some of the lemmas are simplified ? (Either the two conflict lemmas or the actual lemmas from the clingcon propagator).
Is this intended behaviour? And why isn't this possible in the multi-shot case.

Edit: The single-shot option does not need to add the step literal to every learnt nogood. This is why we have shorter (-1 in size) nogoods in general. Using --solve-limit=100 reveals that the searches slowly start to diverge. The single-shot option has 100 Backjumps "executed" while with multi-shot solving we only have 99 Backjumps executed and 1 "Bounded".

Backjumps    : 100      (Average:  4.72 Max:  81 Sum:    472)
  Executed   : 100      (Average:  4.72 Max:  81 Sum:    472 Ratio: 100.00%)
  Bounded    : 0        (Average:  0.00 Max:   0 Sum:      0 Ratio:   0.00%)

vs

Backjumps    : 100      (Average:  4.72 Max:  81 Sum:    472)  
  Executed   : 99       (Average:  4.71 Max:  81 Sum:    471 Ratio:  99.79%)
  Bounded    : 1        (Average:  1.00 Max:   1 Sum:      1 Ratio:   0.21%)

Edit: This backjump is bounded by the step variable. Therefore, in the 'single-shot' case simplifySAT is called, as it backjumps to level 0, while in multi-shot it is bounded to level 1.

[MaxOstrowski]

Is there a possibility from the API to check if the scripts have a callable "main" like Clingo does in

void ClingoControl::main(IClingoApp &app, StringVec const &files, const ClingoOptions& opts, Clasp::Asp::LogicProgram* out) {
    if (app.has_main()) {
        parse({}, opts, out, false);                                                                    
        if (opts.singleShot) { clasp_->keepProgram(); }                                                 
        else { clasp_->enableProgramUpdates(); }                                                        
        app.main(*this, files);
    }                                                                                                   
    else {
        parse(files, opts, out);
        if (scripts_.callable("main")) {                                                                
            if (opts.singleShot) { clasp_->keepProgram(); }
            else { clasp_->enableProgramUpdates(); }                                                    
            scripts_.main(*this);                                                                       
        }                                                                                               
        else if (incmode_) {                                                                            
            if (opts.singleShot) { clasp_->keepProgram(); }                                             
            else { clasp_->enableProgramUpdates(); }                                                    
            incmode(*this);
        }
        else {                                                                                          
            claspConfig_.releaseOptions();                                                              
            Control::GroundVec parts;                                                                   
            parts.emplace_back("base", SymVec{});                                                       
            ground(parts, nullptr);                                                                     
            solve({nullptr, 0}, 0, nullptr)->get();
        }                                                                                               
    }
}

so that --single-shot could automagically be added within the clingcon and clingo-dl binaries ?

[rkaminsk]

We cannot inject an option but would have to extend the API to delay calling keepProgram or enableProgramUpdates. According to clasp's documentation, we have to call these functions before the first call to prepare (i.e., before solving). For example, in the clingcon application, we could call keepProgram instead of enableProgramUpdates because there is no multi-shot solving. People using the Python module, would have to enable it themselves. Whether we can disable multi-shot solving in clingo-dl depends on the options. All of this sounds actually like a good idea because doing this via the API is more helpful then via an option.

PS: I think it makes sense that adding the enumeration assumptions to clauses can lead to runtime differences. I suspect that we can end up with slightly longer clauses and maybe weaker clause strengthening.