pccompile option --use-cnf-hypothesis-for-empowerment

bin/pccompile.cpp

@@ -56,6 +56,7 @@ struct config_t : public SUBool::PrgConfigBase
    SUBool::PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
        candidates_from_negative_policy{
            SUBool::PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP};
+   bool use_cnf_hypothesis_for_empowerment{false};
    long double timeout{-1.0};
    SUBool::AbsComp::BaseConfig comp_base_config{};
    bool unfinished_write{true};
@@ -106,6 +107,8 @@ config_t::InnerDump(unsigned level) const
        "\t", level, "initial_negatives", initial_negatives);
    SUBool::PCLearnComp::kCandidatesFromNegativePolicyAnnotation.DumpValue("\t",
        level, "candidates_from_negative", candidates_from_negative_policy);
+   SUBool::logs.DumpValue("\t", level, "use_cnf_hypothesis_for_empowerment",
+       use_cnf_hypothesis_for_empowerment);
    SUBool::logs.DumpValue("\t", level, "timeout", timeout);
    SUBool::logs.DumpValue("\t", level, "comp_base_config.timeouts.timeout",
        comp_base_config.timeouts.timeout);
@@ -150,6 +153,8 @@ parse_arguments(int argc, char *argv[], config_t &conf)
    conf.initial_negatives = pclearncomp_opts->InitialNegatives();
    conf.candidates_from_negative_policy =
        pclearncomp_opts->CandidatesFromNegativePolicy();
+   conf.use_cnf_hypothesis_for_empowerment =
+       pclearncomp_opts->UseCNFHypothesisForEmpeworment();
    conf.comp_base_config.preprocess = preprocess_opts->PreprocessMethod();
    conf.comp_base_config.propagate_backbones =
        !preprocess_opts->NoBackbonePropagation();
@@ -246,6 +251,8 @@ learning_compiler(const config_t &conf, SUBool::CNF cnf)
    l_conf.initial_negatives = conf.initial_negatives;
    l_conf.candidates_from_negative_policy =
        conf.candidates_from_negative_policy;
+   l_conf.use_cnf_hypothesis_for_empowerment =
+       conf.use_cnf_hypothesis_for_empowerment;
    return std::make_shared<SUBool::PCLearnComp>(
        std::move(cnf), std::move(l_conf));
 }

lib/pc_opt.cpp

@@ -82,6 +82,14 @@ SUBool::PCLearnCompOptions::PCLearnCompOptions()
 {
    Add(mInitialNegativesOption);
    Add(mCandidatesFromNegativePolicyOption);
+   AddOptions()("use-cnf-hypothesis-for-empowerment",
+       po::bool_switch(&mUseCNFHypothesisForEmpowerment),
+       "If present, then the CNF hypothesis is used to encode empowerment in "
+       "the SAT based PC checks within the learning algorithm. If this option "
+       "is not present, then the default approach is to use the implicational "
+       "system based on the negative examples for encoding empowerment. (It is "
+       "suggested to combine this option with '--candidates-from-negative "
+       "none'.)");
 }
 
 bool

lib/pc_opt.h

@@ -65,6 +65,7 @@ namespace SUBool
           mCandidatesFromNegativePolicyOption;
       PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
           mCandidatesFromNegativePolicy{kDefaultCandidatesFromNegativePolicy};
+      bool mUseCNFHypothesisForEmpowerment{false};
 
     public:
       PCLearnCompOptions();
@@ -74,6 +75,7 @@ namespace SUBool
       PCLearnComp::INITIAL_NEGATIVES InitialNegatives() const;
       PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
       CandidatesFromNegativePolicy() const;
+      bool UseCNFHypothesisForEmpeworment() const;
    };
 
    // pccompile preprocessing
@@ -265,6 +267,12 @@ SUBool::PCLearnCompOptions::CandidatesFromNegativePolicy() const
    return mCandidatesFromNegativePolicy;
 }
 
+inline bool
+SUBool::PCLearnCompOptions::UseCNFHypothesisForEmpeworment() const
+{
+   return mUseCNFHypothesisForEmpowerment;
+}
+
 inline bool
 SUBool::PCCompPreprocessOptions::NoBackbonePropagation() const
 {

lib/pclearncomp.cpp

@@ -105,7 +105,9 @@ SUBool::PCLearnComp::PCLearnComp(CNF cnf, Config conf)
    if (mPCCheckerSAT.RequiresImplSystem())
    {
       mHypothesis.SetImplSystemProvider(
-          make_negatives_is_provider(conf.impl_system, mNegatives));
+          conf.use_cnf_hypothesis_for_empowerment
+              ? make_enc_is_provider(conf.impl_system)
+              : make_negatives_is_provider(conf.impl_system, mNegatives));
    }
    else
    {

lib/pclearncomp.h

@@ -71,6 +71,7 @@ namespace SUBool
          INITIAL_NEGATIVES initial_negatives{INITIAL_NEGATIVES::BODY_MINIMAL};
          CANDIDATES_FROM_NEGATIVE_POLICY candidates_from_negative_policy{
              CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP};
+         bool use_cnf_hypothesis_for_empowerment{false};
 
          Config() noexcept {}