model communicates logits rather than bools (good/bad)

Kernel/Clause.cpp

@@ -75,7 +75,7 @@ Clause::Clause(unsigned length,const Inference& inf)
     _component(false),
     _store(NONE),
     _numSelected(0),
-    _modelSaidYes(1), // be optimistic by default (delayed eval takes care of demoting the bad guys)
+    _modelSaid(std::numeric_limits<decltype(_modelSaid)>::lowest()), // be optimistic by default (delayed eval takes care of demoting the bad guys)
     _weight(0),
     _weightForClauseSelection(0),
     _refCnt(0),
@@ -439,7 +439,7 @@ vstring Clause::toString() const
     }
 
     if(env.options->evalForKarel()) {
-      result += ",msY:" + Int::toString(_modelSaidYes);
+      result += ",msY:" + Int::toString(_modelSaid);
     }
 
     result += ",thAx:" + Int::toString((int)(_inference.th_ancestors));

Kernel/Clause.hpp

@@ -346,12 +346,12 @@ class Clause
 
   unsigned numPositiveLiterals(); // number of positive literals in the clause
 
-  void modelSaid(bool value) {
-    _modelSaidYes = value;
+  void setModelSaid(float value) {
+    _modelSaid = value;
   }
 
-  bool modelSaidYes() const {
-    return _modelSaidYes;
+  float modelSaid() const {
+    return _modelSaid;
   }
 
 protected:
@@ -374,7 +374,7 @@ class Clause
   /** number of selected literals */
   unsigned _numSelected : 20;
 
-  unsigned _modelSaidYes : 1;
+  float _modelSaid; // small is good
 
   /** weight */
   mutable unsigned _weight;

Saturation/PredicateSplitPassiveClauseContainer.cpp

@@ -103,6 +103,7 @@ void PredicateSplitPassiveClauseContainer::add(Clause* cl)
   ASS(cl->store() == Clause::PASSIVE);
 
   auto bestQueueIndex = bestQueue(evaluateFeature(cl));
+
   if (_layeredArrangement)
   {
     // add clause to all queues starting from best queue for clause
@@ -236,11 +237,12 @@ Clause* PredicateSplitPassiveClauseContainer::popSelected()
 
   if (currIndex < (long int)_queues.size()-1 && // not the last index
       _delayedEvaluator) { // we can re-evaluate
+
     _delayedEvaluator(cl);
 
     if (evaluateFeature(cl) > _cutoffs[currIndex]) {
       // we don't like the clause here!
-      // cout << "Didn't like " << cl->number() << " in " << currIndex << endl;
+      //cout << "Didn't like " << cl->number() << " in " << currIndex << endl;
       goto search_for_an_appropriate_queue;
     }
   }
@@ -566,20 +568,23 @@ float PositiveLiteralMultiSplitPassiveClauseContainer::evaluateFeatureEstimate(u
 
 NeuralEvalSplitPassiveClauseContainer::NeuralEvalSplitPassiveClauseContainer(bool isOutermost, const Shell::Options &opt, Lib::vstring name, Lib::vvector<std::unique_ptr<PassiveClauseContainer>> queues) :
   PredicateSplitPassiveClauseContainer(isOutermost, opt, name, std::move(queues),
-      Lib::vvector<float>({0.0, std::numeric_limits<float>::max()}),
+      opt.neuralEvalSplitQueueCutoffs(),
       opt.neuralEvalSplitQueueRatios(),
       true /* monotone queue split hard-wired here */) {}
 
 float NeuralEvalSplitPassiveClauseContainer::evaluateFeature(Clause* cl) const
 {
   CALL("NeuralEvalSplitPassiveClauseContainer::evaluateFeature");
-  return 1.0-(float)cl->modelSaidYes(); // 0.0 is good, 1.0 is bad (because the hard-wired < comparison in PredicateSplitPassiveClauseContainer)
+
+  // cout << "evaluateFeature " << cl->number() << " " << cl->modelSaid() << endl;
+
+  return cl->modelSaid(); // small is good, large is bad
 }
 
 float NeuralEvalSplitPassiveClauseContainer::evaluateFeatureEstimate(unsigned numPositiveLiterals, const Inference& inference) const
 {
   CALL("NeuralEvalSplitPassiveClauseContainer::evaluateFeatureEstimate");
-  return 0.0; // simply estimate that the clause is good
+  return std::numeric_limits<float>::lowest(); // simply estimate that the clause is good
 }
 
 };

Saturation/SaturationAlgorithm.cpp

@@ -215,7 +215,7 @@ static std::unique_ptr<PassiveClauseContainer> makeLevel5(bool isOutermost, cons
   if (opt.useNeuralEvalSplitQueues())
   {
     Lib::vvector<std::unique_ptr<PassiveClauseContainer>> queues;
-    Lib::vvector<float> cutoffs = opt.positiveLiteralSplitQueueCutoffs();
+    Lib::vvector<float> cutoffs = opt.neuralEvalSplitQueueCutoffs();
     for (unsigned i = 0; i < cutoffs.size(); i++)
     {
       auto queueName = name + "NESQ" + Int::toString(cutoffs[i]) + ":";
@@ -540,7 +540,7 @@ void SaturationAlgorithm::embed_and_evaluate(Clause* cl, const char* method_name
     inputs.push_back(id);
 
     auto out = _model.forward(inputs);
-    cl->modelSaid(out.toBool());
+    cl->setModelSaid(-out.toDouble()); // already here, we reverse the logit's logic to "small is good"!
   }
 }
 
@@ -1367,7 +1367,7 @@ void SaturationAlgorithm::addToPassive(Clause* cl)
 
   if (_opt.evalForKarel()) {
     // talkToKarel(cl); // delayed evaluation trick (TODO: do this for initial as well?)
-    cl->modelSaid(true);
+    // cl->modelSaid(true); // the clause is born as good; see Clause::Clause
   }
 
   {

Shell/Options.cpp

@@ -1021,6 +1021,12 @@ void Options::Options::init()
     _useNeuralEvalSplitQueues.reliesOn(_evalForKarel.is(notEqual(vstring(""))));
     _useNeuralEvalSplitQueues.tag(OptionTag::SATURATION);
 
+    _neuralEvalSplitQueueCutoffs = StringOptionValue("neural_eval_split_queue_cutoffs", "nesqc", "0");
+    _neuralEvalSplitQueueCutoffs.description = "The cutoff-values for the neural-eval-split-queues (the cutoff value for the last queue is omitted, since it has to be infinity).";
+    _lookup.insert(&_neuralEvalSplitQueueCutoffs);
+    _neuralEvalSplitQueueCutoffs.reliesOn(_useNeuralEvalSplitQueues.is(equal(true)));
+    _neuralEvalSplitQueueCutoffs.tag(OptionTag::SATURATION);
+
     _neuralEvalSplitQueueRatios = StringOptionValue("neural_eval_split_queue_ratios", "nesqr", "10,1");
     _neuralEvalSplitQueueRatios.description = "The ratios for picking clauses from the neural-eval-split-queues using weighted round robin. If a queue is empty, the clause will be picked from the next non-empty queue to the right."
         " There should be exactly two numbers in the list.";
@@ -3529,3 +3535,30 @@ Lib::vvector<int> Options::neuralEvalSplitQueueRatios() const
   return inputRatios;
 }
 
+Lib::vvector<float> Options::neuralEvalSplitQueueCutoffs() const
+{
+  CALL("Options::neuralEvalSplitQueueCutoffs");
+  // initialize cutoffs and add float-max as last value
+  Lib::vvector<float> cutoffs;
+  vstringstream cutoffsStream(_neuralEvalSplitQueueCutoffs.actualValue);
+  std::string currentCutoff;
+  while (std::getline(cutoffsStream, currentCutoff, ','))
+  {
+    cutoffs.push_back(std::stof(currentCutoff));
+  }
+  cutoffs.push_back(std::numeric_limits<float>::max());
+
+  // sanity checks
+  for (unsigned i = 0; i < cutoffs.size(); i++)
+  {
+    auto cutoff = cutoffs[i];
+
+    if (i > 0 && cutoff <= cutoffs[i-1])
+    {
+      USER_ERROR("The cutoff values (supplied by option '-nesqc') must be strictly increasing");
+    }
+  }
+
+  return cutoffs;
+}
+

Shell/Options.hpp

@@ -2131,6 +2131,7 @@ bool _hard;
 
   bool useNeuralEvalSplitQueues() const { return _useNeuralEvalSplitQueues.actualValue; }
   Lib::vvector<int> neuralEvalSplitQueueRatios() const;
+  Lib::vvector<float> neuralEvalSplitQueueCutoffs() const;
 
   void setWeightRatio(int v){ _ageWeightRatio.otherValue = v; }
 	AgeWeightRatioShape ageWeightRatioShape() const { return _ageWeightRatioShape.actualValue; }
@@ -2413,6 +2414,7 @@ bool _hard;
   StringOptionValue _positiveLiteralSplitQueueCutoffs;
   BoolOptionValue _positiveLiteralSplitQueueLayeredArrangement;
   BoolOptionValue _useNeuralEvalSplitQueues;
+  StringOptionValue _neuralEvalSplitQueueCutoffs;
   StringOptionValue _neuralEvalSplitQueueRatios;
 
 	BoolOptionValue _randomAWR;