Commit c3f596ed authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

Candidates from added negative option (not yet finished)

parent a2027d23
......@@ -53,6 +53,9 @@ struct config_t : public SUBool::PrgConfigBase
unsigned pccheck_random_budget_inc{1};
SUBool::PCLearnComp::INITIAL_NEGATIVES initial_negatives{
SUBool::PCLearnComp::INITIAL_NEGATIVES::ALL_EMPOWERING};
SUBool::PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
candidates_from_negative_policy{
SUBool::PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP};
long double timeout{-1.0};
SUBool::AbsComp::BaseConfig comp_base_config{};
bool unfinished_write{true};
......@@ -101,6 +104,8 @@ config_t::InnerDump(unsigned level) const
"\t", level, "pccheck_random_budget_inc", pccheck_random_budget_inc);
SUBool::PCLearnComp::kInitialNegativesAnnotation.DumpValue(
"\t", level, "initial_negatives", initial_negatives);
SUBool::PCLearnComp::kCandidatesFromNegativePolicyAnnotation.DumpValue("\t",
level, "candidates_from_negative", candidates_from_negative_policy);
SUBool::logs.DumpValue("\t", level, "timeout", timeout);
SUBool::logs.DumpValue("\t", level, "comp_base_config.timeouts.timeout",
comp_base_config.timeouts.timeout);
......@@ -143,6 +148,8 @@ parse_arguments(int argc, char *argv[], config_t &conf)
}
conf.algorithm = algorithm_opts->Algorithm();
conf.initial_negatives = pclearncomp_opts->InitialNegatives();
conf.candidates_from_negative_policy =
pclearncomp_opts->CandidatesFromNegativePolicy();
conf.comp_base_config.preprocess = preprocess_opts->PreprocessMethod();
conf.comp_base_config.propagate_backbones =
!preprocess_opts->NoBackbonePropagation();
......@@ -237,6 +244,8 @@ learning_compiler(const config_t &conf, SUBool::CNF cnf)
l_conf.pccheck_random_budget = conf.pccheck_random_budget;
l_conf.pccheck_random_budget_inc = conf.pccheck_random_budget_inc;
l_conf.initial_negatives = conf.initial_negatives;
l_conf.candidates_from_negative_policy =
conf.candidates_from_negative_policy;
return std::make_shared<SUBool::PCLearnComp>(
std::move(cnf), std::move(l_conf));
}
......
......@@ -68,9 +68,20 @@ SUBool::PCLearnCompOptions::PCLearnCompOptions()
"How the initial negative examples in the learning algorithm "
"should be produced. The option specifies how the negatives for each "
"clause in the preprocessed CNF are created.",
kDefaultInitialNegatives)
kDefaultInitialNegatives),
mCandidatesFromNegativePolicyOption(
PCLearnComp::kCandidatesFromNegativePolicyAnnotation,
"candidates-from-negative",
"Whenever a negative example is added to the hypothesis, the "
"corresponding clauses are added to the CNF hypothesis if they are "
"empowering. In this case, the clause may be used to obtain further "
"negative examples to keep the CNF hypothesis synchronized with the "
"implicational representation of the hypothesis. This option allows "
"to set a policy of how this extraction should be done.",
kDefaultCandidatesFromNegativePolicy)
{
Add(mInitialNegativesOption);
Add(mCandidatesFromNegativePolicyOption);
}
bool
......
......@@ -53,11 +53,18 @@ namespace SUBool
public:
PCLearnComp::INITIAL_NEGATIVES kDefaultInitialNegatives{
PCLearnComp::INITIAL_NEGATIVES::BODY_MINIMAL};
PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
kDefaultCandidatesFromNegativePolicy{
PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP};
private:
EnumOption<PCLearnComp::INITIAL_NEGATIVES> mInitialNegativesOption;
PCLearnComp::INITIAL_NEGATIVES mInitialNegatives{
kDefaultInitialNegatives};
EnumOption<PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY>
mCandidatesFromNegativePolicyOption;
PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
mCandidatesFromNegativePolicy{kDefaultCandidatesFromNegativePolicy};
public:
PCLearnCompOptions();
......@@ -65,6 +72,8 @@ namespace SUBool
virtual bool GetValues() override;
PCLearnComp::INITIAL_NEGATIVES InitialNegatives() const;
PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
CandidatesFromNegativePolicy() const;
};
// pccompile preprocessing
......@@ -249,6 +258,13 @@ SUBool::PCLearnCompOptions::InitialNegatives() const
return mInitialNegatives;
}
inline auto
SUBool::PCLearnCompOptions::CandidatesFromNegativePolicy() const
-> PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY
{
return mCandidatesFromNegativePolicy;
}
inline bool
SUBool::PCCompPreprocessOptions::NoBackbonePropagation() const
{
......
......@@ -58,8 +58,7 @@ const SUBool::EnumAnnotation<SUBool::PCLearnComp::INITIAL_NEGATIVES>
{//
{PCLearnComp::INITIAL_NEGATIVES::SINGLE_EMPOWERING,
"single_empowering",
"one negative example is produced from every empowering "
"clause "
"one negative example is produced from every empowering clause "
"(the clause C without an empowered literal)"}, //
{PCLearnComp::INITIAL_NEGATIVES::ALL, "all",
"all negative examples from all clauses are produced, i.e. for "
......@@ -79,6 +78,21 @@ const SUBool::EnumAnnotation<SUBool::PCLearnComp::INITIAL_NEGATIVES>
"preprocessed CNF is computed. Its bodies are used as an "
"initial list of negative examples."}});
const SUBool::EnumAnnotation<
SUBool::PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY>
SUBool::PCLearnComp::kCandidatesFromNegativePolicyAnnotation(
"CANDIDATES_FROM_ADDED_CLAUSE",
{//
{PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::NONE, "none",
"No candidates are extracted from the clause added to the "
"hypothesis"}, //
{PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::SEMANTIC, "semantic",
"Semantic closure is computed and compared with the forward "
"chaining closure with respect to the implicational system"}, //
{PCLearnComp::CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP, "unitprop",
"It is only checked if the set of literals is closed under "
"unit propagation in the current CNF hypothesis"}});
SUBool::PCLearnComp::PCLearnComp(CNF cnf, Config conf)
: AbsComp(cnf, conf.minimize_method, conf.impl_system_rebuild),
mConf(std::move(conf)), mNegatives(), mCandidatesWithClosure(),
......@@ -805,11 +819,17 @@ SUBool::PCLearnComp::AddNegativesForImplicate(
logs.TLog(3) << "Considering implicate "
<< mHypothesis.Compressor().UncompressClause(clause)
<< std::endl;
auto c = (find_prime_subimplicate
? *mHypothesis.PrimeSubimplicate(clause, 0, true)
: clause);
logs.TLog(3) << "Found prime subimplicate "
<< mHypothesis.Compressor().UncompressClause(c) << std::endl;
Clause c;
if (find_prime_subimplicate)
{
c = *mHypothesis.PrimeSubimplicate(clause, 0, true);
logs.TLog(3) << "Found prime subimplicate "
<< mHypothesis.Compressor().UncompressClause(c) << std::endl;
}
else
{
c = clause;
}
c.NegateLiterals();
unsigned candidates_cnt = 0;
for (const auto &lit : c)
......@@ -952,7 +972,7 @@ SUBool::PCLearnComp::AddNegativeToHypothesis(const LitImpl &e)
{
++mClausesAddedToHypothesis;
++mAddedClausesSinceMinimization;
mCandidatesFromNegativesCount += AddNegativesForImplicate(*c, false);
mCandidatesFromNegativesCount += AddCandidatesForAddedClause(*c);
}
}
......@@ -960,6 +980,30 @@ SUBool::PCLearnComp::AddNegativeToHypothesis(const LitImpl &e)
<< std::endl;
}
unsigned
SUBool::PCLearnComp::AddCandidatesForAddedClause(const Clause &clause)
{
switch (mConf.candidates_from_negative_policy)
{
case CANDIDATES_FROM_NEGATIVE_POLICY::NONE:
return 0;
case CANDIDATES_FROM_NEGATIVE_POLICY::SEMANTIC:
return AddNegativesForImplicate(clause, false);
case CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP:
return AddCandidatesForAddedClauseUnitProp(clause);
}
throw BadParameterException("PCLearnComp::AddCandidatesForAddedClause",
"Unknown candidates_from_negative_policy");
}
unsigned
SUBool::PCLearnComp::AddCandidatesForAddedClauseUnitProp(
const Clause &clause [[maybe_unused]])
{
throw NotImplementedException(
"PCLearnComp::AddCandidatesForAddedClauseUnitProp", "");
}
void
SUBool::PCLearnComp::MinimizeHypothesis()
{
......
......@@ -47,6 +47,18 @@ namespace SUBool
static const EnumAnnotation<INITIAL_NEGATIVES>
kInitialNegativesAnnotation;
enum class CANDIDATES_FROM_NEGATIVE_POLICY
{
NONE, // No candidates extracted from the clause added to the
// hypothesis
SEMANTIC, // Semantic closure is used to determine if the set of
// literals is a negative example
UNITPROP // Only UP closures of the hypothesis with the implication
// system are compared
};
static const EnumAnnotation<CANDIDATES_FROM_NEGATIVE_POLICY>
kCandidatesFromNegativePolicyAnnotation;
struct Config : public BaseConfig
{
bool hypothesis_minimize{true};
......@@ -57,6 +69,9 @@ namespace SUBool
unsigned pccheck_random_budget_inc{1};
double cache_time_logging_threshold{0.001};
INITIAL_NEGATIVES initial_negatives{INITIAL_NEGATIVES::BODY_MINIMAL};
CANDIDATES_FROM_NEGATIVE_POLICY candidates_from_negative_policy{
CANDIDATES_FROM_NEGATIVE_POLICY::UNITPROP};
Config() noexcept {}
PCEncoder::Config EncoderConfig();
......@@ -164,6 +179,8 @@ namespace SUBool
// still negative, otherwise none.
std::optional<LitImpl> UpdateCandidate(const LitImpl &neg);
bool AddCandidateIfNegative(const LitImpl &candidate);
unsigned AddCandidatesForAddedClause(const Clause &clause);
unsigned AddCandidatesForAddedClauseUnitProp(const Clause &clause);
NECache::const_iterator CachedClosure(
const std::vector<Literal> &body) const;
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment