From a238b29ee6e5afd16d6f439d7ea5d48577bbc6c3 Mon Sep 17 00:00:00 2001 From: Jorge Fandinno Date: Wed, 23 Oct 2024 16:43:34 -0500 Subject: [PATCH] fixing strong negation --- src/eclingo/solver/base_program.lp | 28 +++++ src/eclingo/solver/generator.py | 103 +++++------------- .../solver/generator_opt_common_program.lp | 12 ++ .../solver/generator_opt_fact_program.lp | 5 + 4 files changed, 71 insertions(+), 77 deletions(-) create mode 100644 src/eclingo/solver/base_program.lp create mode 100644 src/eclingo/solver/generator_opt_common_program.lp create mode 100644 src/eclingo/solver/generator_opt_fact_program.lp diff --git a/src/eclingo/solver/base_program.lp b/src/eclingo/solver/base_program.lp new file mode 100644 index 0000000..2400a9b --- /dev/null +++ b/src/eclingo/solver/base_program.lp @@ -0,0 +1,28 @@ +conjunction(B) :- literal_tuple(B), hold(L) : literal_tuple(B, L), L > 0; + not hold(L) : literal_tuple(B, -L), L > 0. + +body(normal(B)) :- rule(_, normal(B)), conjunction (B). + +body(sum(B, G)) :- rule (_, sum(B,G)), + #sum { W,L : hold(L), weighted_literal_tuple(B, L, W), L>0; + W,L : not hold(L), weighted_literal_tuple(B, -L, W), L>0} >= G. + +hold(A) : atom_tuple(H,A) :- rule(disjunction(H), B), body(B). + +{hold(A) : atom_tuple(H,A)} :- rule(choice(H), B), body(B). + +fact(SA) :- output(SA, LT), #count {L : literal_tuple(LT, L)} = 0. + +atom_map(SA, A) :- output(SA,LT), #count{LL : literal_tuple(LT, LL)} = 1, literal_tuple(LT, A). + +hold_symbolic_atom(SA) :- atom_map(SA, A), hold(A). +hold_symbolic_atom(SA) :- fact(SA). +:- hold_symbolic_atom(u(-SA)), hold_symbolic_atom(u(SA)). + +positive_candidate(k(A)) :- fact(k(A)). +positive_candidate(k(A)) :- output(k(A), B), conjunction(B). +negative_candidate(k(A)) :- output(k(A), B), not conjunction(B). + +#show positive_candidate/1. +#show negative_candidate/1. + diff --git a/src/eclingo/solver/generator.py b/src/eclingo/solver/generator.py index e97a848..1516186 100644 --- a/src/eclingo/solver/generator.py +++ b/src/eclingo/solver/generator.py @@ -1,4 +1,4 @@ -import sys +from pathlib import Path from typing import Iterator, Optional, Sequence, Tuple, cast import clingo @@ -13,49 +13,30 @@ # from clingox.solving import approximate +current_script_path = Path(__file__).parent -base_program = """\ -conjunction(B) :- literal_tuple(B), hold(L) : literal_tuple(B, L), L > 0; - not hold(L) : literal_tuple(B, -L), L > 0. -body(normal(B)) :- rule(_, normal(B)), conjunction (B). +with open(current_script_path / "base_program.lp") as f: + base_program = f.read() -body(sum(B, G)) :- rule (_, sum(B,G)), - #sum { W,L : hold(L), weighted_literal_tuple(B, L, W), L>0; - W,L : not hold(L), weighted_literal_tuple(B, -L, W), L>0} >= G. +with open(current_script_path / "generator_opt_common_program.lp") as f: + common_opt_program = f.read() -hold(A) : atom_tuple(H,A) :- rule(disjunction(H), B), body(B). +# common_opt_program = """\ +# symbolic_atom(SA) :- atom_map(SA, _). -{hold(A) : atom_tuple(H,A)} :- rule(choice(H), B), body(B). +# symbolic_epistemic_atom(k(A)) :- symbolic_atom(k(A)). +# symbolic_objective_atom(OSA) :- symbolic_atom(OSA), not symbolic_epistemic_atom(OSA). -fact(SA) :- output(SA, LT), #count {L : literal_tuple(LT, L)} = 0. +# epistemic_atom_map(KSA, KA) :- atom_map(KSA, KA), symbolic_epistemic_atom(KSA). +# objective_atom_map(OSA, OA) :- atom_map(OSA, OA), symbolic_objective_atom(OSA). -positive_candidate(k(A)) :- fact(k(A)). -positive_candidate(k(A)) :- output(k(A), B), conjunction(B). -negative_candidate(k(A)) :- output(k(A), B), not conjunction(B). +# epistemic_atom_int(KA) :- epistemic_atom_map(_, KA). +# objective_atom_int(A) :- objective_atom_map(_, A). -atom_map(SA, A) :- output(SA,LT), #count{LL : literal_tuple(LT, LL)} = 1, literal_tuple(LT, A). -strong_negatation_complement(A, B) :- atom_map(u(SA), A), atom_map(u(-SA), B). -:- hold(A), hold(B), strong_negatation_complement(A, B). +# epistemic_map(KA,OA) :- epistemic_atom_map(KSA, KA), objective_atom_map(OSA, OA), KSA = k(OSA). +# """ -#show positive_candidate/1. -#show negative_candidate/1. -""" - -common_opt_program = """\ -symbolic_atom(SA) :- atom_map(SA, _). - -symbolic_epistemic_atom(k(A)) :- symbolic_atom(k(A)). -symbolic_objective_atom(OSA) :- symbolic_atom(OSA), not symbolic_epistemic_atom(OSA). - -epistemic_atom_map(KSA, KA) :- atom_map(KSA, KA), symbolic_epistemic_atom(KSA). -objective_atom_map(OSA, OA) :- atom_map(OSA, OA), symbolic_objective_atom(OSA). - -epistemic_atom_int(KA) :- epistemic_atom_map(_, KA). -objective_atom_int(A) :- objective_atom_map(_, A). - -epistemic_map(KA,OA) :- epistemic_atom_map(KSA, KA), objective_atom_map(OSA, OA), KSA = k(OSA). -""" preprocessing_program = """\ :- cautious(SA), atom_map(SA, A), not hold(A). @@ -70,13 +51,17 @@ # cautious_epistemic(KSA) :- cautious(KSA), symbolic_epistemic_atom(KSA). # :- epistemic_atom_map(KSA, KA), cautious_epistemic(KSA), not hold(KA). -fact_optimization_program = """\ -% Propagate facts into epistemic facts -:- fact(OSA), epistemic_atom_map(k(OSA), KA), not hold(KA). -positive_extra_assumptions(OSA) :- fact(OSA), symbolic_epistemic_atom(k(OSA)). -#show positive_extra_assumptions/1. -""" +with open(current_script_path / "generator_opt_fact_program.lp") as f: + fact_optimization_program = f.read() + +# fact_optimization_program = """\ +# % Propagate facts into epistemic facts + +# :- fact(OSA), epistemic_atom_map(k(OSA), KA), not hold(KA). +# positive_extra_assumptions(OSA) :- fact(OSA), symbolic_epistemic_atom(k(OSA)). +# #show positive_extra_assumptions/1. +# """ propagation_program = """\ :- kp_hold(OA), epistemic_map(KA, OA), not hold(KA). @@ -181,48 +166,12 @@ def __call__(self) -> Iterator[Candidate]: if not self._config.propagate: yield from self._candidates() else: - # return self._candidates() self.control.assign_external(Function("only_proved_candidates"), True) self.control.assign_external(Function("only_unproved_candidates"), False) yield from self._candidates() self.control.assign_external(Function("only_proved_candidates"), False) self.control.assign_external(Function("only_unproved_candidates"), True) yield from self._candidates() - # # with cast(clingo.SolveHandle, self.control.solve(yield_=True)) as handle: - # # for model in handle: - # # # print("*" * 50) - # # # print(model) - # # # print("\n".join(sorted(str(a) for a in model.symbols(atoms=True)))) - # # candidate = self._model_to_candidate(model) - # # self.num_candidates += 1 - # # yield candidate - # self.control.assign_external(Function("only_proved_candidates"), True) - # self.control.assign_external(Function("only_unproved_candidates"), False) - # candidates = [] - # with cast(clingo.SolveHandle, self.control.solve(yield_=True)) as handle: - # for model in handle: - # # print("*" * 50) - # # print(model) - # # print("\n".join(sorted(str(a) for a in model.symbols(atoms=True)))) - # candidate = self._model_to_candidate(model) - # self.num_candidates += 1 - # candidates.append((frozenset(candidate.pos), frozenset(candidate.neg))) - # yield candidate - # self.control.assign_external(Function("only_proved_candidates"), False) - # self.control.assign_external(Function("only_unproved_candidates"), True) - # seen_candidates = frozenset(candidates) - # with cast(clingo.SolveHandle, self.control.solve(yield_=True)) as handle: - # for model in handle: - # # print("*" * 50) - # # print(model) - # # print("\n".join(sorted(str(a) for a in model.symbols(atoms=True)))) - # candidate = self._model_to_candidate(model) - # self.num_candidates += 1 - # # if ( - # # frozenset(candidate.pos), - # # frozenset(candidate.neg), - # # ) not in seen_candidates: - # yield candidate def _candidates(self) -> Iterator[Candidate]: with cast(clingo.SolveHandle, self.control.solve(yield_=True)) as handle: diff --git a/src/eclingo/solver/generator_opt_common_program.lp b/src/eclingo/solver/generator_opt_common_program.lp new file mode 100644 index 0000000..0b1a865 --- /dev/null +++ b/src/eclingo/solver/generator_opt_common_program.lp @@ -0,0 +1,12 @@ +symbolic_atom(SA) :- atom_map(SA, _). + +symbolic_epistemic_atom(k(A)) :- symbolic_atom(k(A)). +symbolic_objective_atom(OSA) :- symbolic_atom(OSA), not symbolic_epistemic_atom(OSA). + +epistemic_atom_map(KSA, KA) :- atom_map(KSA, KA), symbolic_epistemic_atom(KSA). +objective_atom_map(OSA, OA) :- atom_map(OSA, OA), symbolic_objective_atom(OSA). + +epistemic_atom_int(KA) :- epistemic_atom_map(_, KA). +objective_atom_int(A) :- objective_atom_map(_, A). + +epistemic_map(KA,OA) :- epistemic_atom_map(KSA, KA), objective_atom_map(OSA, OA), KSA = k(OSA). \ No newline at end of file diff --git a/src/eclingo/solver/generator_opt_fact_program.lp b/src/eclingo/solver/generator_opt_fact_program.lp new file mode 100644 index 0000000..662233c --- /dev/null +++ b/src/eclingo/solver/generator_opt_fact_program.lp @@ -0,0 +1,5 @@ +% Propagate facts into epistemic facts + +:- fact(OSA), epistemic_atom_map(k(OSA), KA), not hold(KA). +positive_extra_assumptions(OSA) :- fact(OSA), symbolic_epistemic_atom(k(OSA)). +#show positive_extra_assumptions/1. \ No newline at end of file