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.