Previous  Up  Next

Module Heuristic

module Heuristic: sig .. end
Generate a heuristic from a payoff.

Input: a set of relations F whose instances can be altered duirng a game; initial state structure S of the game; payoff of the game for a player; advancement value ratio AR.

Return a homomorphic image of the payoff which transforms Char(Phi) into H(Phi).

H(Phi) = Alg(FFNF(promote relations F) of Phi', true) where Phi' = Phi if not SuggestExpansion(Phi, S) otherwise Phi' = ExpandedForm(F, S, FFNF(promote relations F) of Phi)

**********

SuggestExpansion(Phi, S) is true iff Phi has a universal quantifier or if the number of existential quantifiers in Phi is smaller than the square root of the number of elements in S.

Tentative compact specification of ExpandedDescription:

ExpandedDescription(S, T) of a set of substitutions T(x1,...,xn) (which can be seen as a set of n-tuples interpreting T in S) over elements a structure S is built from minimal sets of atoms Psi over variables (x1,...,xn,y1,...,yk) as "\/ ex y1,...,yk /\Psi" such that every "ex y1,...,yk /\Psi" is equivalent to T(x1,...,xn) in S (minimality means that for no proper subset Psi' of Psi is "ex y1,...,yk /\Psi'" equivalent to T(x1,...,xn) in S). ExpandedDescription may not exist for some pairs (S,T).

Maximal expanded description is an expanded description which cannot be extended with a disjunct nonequivalent to disjuncts actually present in it. The algorithm falls short of maximality because of parts marked as GREEDY (for the same reason the algorithm is not complete).

By ExpandedDescription(F, S, psi) (where psi is a formula not containing relations from F) we will denote ExpandedDescription(S',T) where T is a set of substitutions satisfying psi in S', and S' is S truncated to relations outside F.

Algorithm for finding the ExpandedForm(F,S,Phi):

Let Phi=CDE(psi_1,...,psi_m) be a conjunctive-disjunctive-existential combination of (psi_1,...,psi_m), where each psi_i is either an atom, or has a conjunction, a negation or a quantification as its root.

ExpandedForm(F,S,Phi) = CDE(ED(psi_1), ..., ED(psi_m)), where "ED(psi) = ExpandedDescription(F,S,psi)" if psi does not contain relations from F and ExpandedDescription(F,S,psi) exists, otherwise "ED(psi_1 and ... and psi_n) = ED(psi_1) and ... and ED(psi_n)", "ED(ex x psi) = ex x ED(psi)", in other cases "ED(psi) = psi". (Where psi is either a formula or a set of all satisfying substitutions for psi in S, depending on context.)

val use_monotonic : bool Pervasives.ref

Generate a heuristic from a payoff.

Input: a set of relations F whose instances can be altered duirng a game; initial state structure S of the game; payoff of the game for a player; advancement value ratio AR.

Return a homomorphic image of the payoff which transforms Char(Phi) into H(Phi).

H(Phi) = Alg(FFNF(promote relations F) of Phi', true) where Phi' = Phi if not SuggestExpansion(Phi, S) otherwise Phi' = ExpandedForm(F, S, FFNF(promote relations F) of Phi)

**********

SuggestExpansion(Phi, S) is true iff Phi has a universal quantifier or if the number of existential quantifiers in Phi is smaller than the square root of the number of elements in S.

Tentative compact specification of ExpandedDescription:

ExpandedDescription(S, T) of a set of substitutions T(x1,...,xn) (which can be seen as a set of n-tuples interpreting T in S) over elements a structure S is built from minimal sets of atoms Psi over variables (x1,...,xn,y1,...,yk) as "\/ ex y1,...,yk /\Psi" such that every "ex y1,...,yk /\Psi" is equivalent to T(x1,...,xn) in S (minimality means that for no proper subset Psi' of Psi is "ex y1,...,yk /\Psi'" equivalent to T(x1,...,xn) in S). ExpandedDescription may not exist for some pairs (S,T).

Maximal expanded description is an expanded description which cannot be extended with a disjunct nonequivalent to disjuncts actually present in it. The algorithm falls short of maximality because of parts marked as GREEDY (for the same reason the algorithm is not complete).

By ExpandedDescription(F, S, psi) (where psi is a formula not containing relations from F) we will denote ExpandedDescription(S',T) where T is a set of substitutions satisfying psi in S', and S' is S truncated to relations outside F.

Algorithm for finding the ExpandedForm(F,S,Phi):

Let Phi=CDE(psi_1,...,psi_m) be a conjunctive-disjunctive-existential combination of (psi_1,...,psi_m), where each psi_i is either an atom, or has a conjunction, a negation or a quantification as its root.

ExpandedForm(F,S,Phi) = CDE(ED(psi_1), ..., ED(psi_m)), where "ED(psi) = ExpandedDescription(F,S,psi)" if psi does not contain relations from F and ExpandedDescription(F,S,psi) exists, otherwise "ED(psi_1 and ... and psi_n) = ED(psi_1) and ... and ED(psi_n)", "ED(ex x psi) = ex x ED(psi)", in other cases "ED(psi) = psi". (Where psi is either a formula or a set of all satisfying substitutions for psi in S, depending on context.)

val print_heur : string -> Formula.real_expr array array -> unit
Simple heuristic print helper.
val force_competitive : bool Pervasives.ref
Irrespective of the shape of payoffs, take the difference of heuristics as the final heuristic for each player (in Heuristic.default_heuristic_old).
val expanded_description : int ->
       Aux.Strings.t -> Structure.structure -> Formula.formula -> Formula.formula
Returns a disjunction of existentially quantified conjunctions of atoms each disjunct being equivalent to the given formula in the given model. Testing purposes mostly.
val expanded_form : int ->
       Aux.Strings.t -> Structure.structure -> Formula.formula -> Formula.formula
Apply a variant of Heuristic.expanded_description to subformulas for which it succeeds.
val cache_expanded_form : Formula.formula ->
       Structure.structure -> string list -> Formula.formula -> unit
This function allows to add cached expanded forms; for speed only!
val suggest_expansion : Structure.structure -> Formula.formula -> bool
Whether a formula should be considered for expansion: has a universal quantifier or the number of its existential quantifiers is smaller than suggest_expansion_coef times the square root of the number of elements in the structure.
val of_payoff : ?force_parsimony:int ->
       ?max_alt_descr:int ->
       ?struc:Structure.structure ->
       ?fluent_preconds:(string * (string list * Formula.formula)) list ->
       float ->
       ?posi_frels:Aux.Strings.t ->
       ?nega_frels:Aux.Strings.t ->
       Aux.Strings.t -> Formula.real_expr -> Formula.real_expr
Heuristic of payoff expression.
val map_constants : (float -> float) -> Formula.real_expr -> Formula.real_expr
Rewrite numeric constants inside an expression.
val mix_heur : Formula.real_expr array array ->
       float -> Formula.real_expr array array -> Formula.real_expr array array
Various constructed heuristics.
val default_heuristic : ?struc:Structure.structure ->
       ?advr:float -> Arena.game -> Formula.real_expr array array
val default_heuristic_old : ?struc:Structure.structure ->
       ?advr:float -> Arena.game -> Formula.real_expr array array
val fluents_heuristic : Arena.game -> Formula.real_expr array array
val is_constant_sum_one : Formula.real_expr array -> bool
val is_constant_sum : Formula.real_expr array array -> bool
val compute_heuristic : Arena.game * Arena.game_state -> Formula.real_expr array array
Helper function to do the full computation.