Sequential Decision Making Support

[haz]

Proposal Summary

General idea is to facilitate the creation of planning-like logical theories. Propositions are defined for states and actions (latter are assumed to be (and should be enforced) mutually exclusive, for now). Constraints dictate when a fluent is deleted or added (as a function of the previous state and action), and also the conditions under which an action may be executed. The update rule for fluent F:

S2.F <-> F+ \/ (S1.F /\ ~F-)

where we have,

• S2.F: The updated fluent in successor state S2
• S1.F: The previous value of the fluent
• F+: Formula that dictates when the fluent is added
• F-: Formula that dictate when the fluent is deleted

In other words, S2.F holds when it's made true, or when it's already true and not made false. The formulae F- and F+ must be defined for every class defining state fluent propositions.

Example Usage

Here is a simple theory that keeps track of an agent

from bauhaus import Encoding, proposition, constraint, And, Or
from bauhaus.SAS import stateprop, actionprop

e = Encoding()

LOWER = 0
UPPER = 3

@proposition(e)
@stateprop(e)
class Loc(object):
    def __init__(self, i, j):
        self.x = i
        self.y = j
        
    def _prop_name(self):
        return f"Loc({self.x},{self.y})"
        
    def _delete(self, S, A):
        # Delete if it's true
        return S.Loc(self.x, self.y)
        
    def _add(self, S, A):
        if self.x > LOWER:
            east = S.Loc(self.x-1, self.y) & A.Move('E')
        if self.x < UPPER:
            west = S.Loc(self.x+1, self.y) & A.Move('W')
        if self.y > LOWER:
            north = S.Loc(self.x, self.y-1) & A.Move('N')
        if self.y < UPPER:
            south = S.Loc(self.x, self.y+1) & A.Move('S')
        return east | west | north | south

@proposition(e)
@actionprop(e)
class Move(object):
    def __init__(self, direction):
        assert direction in ['N','S','E','W'], "Can only be N,S,E,W"
        self.direction = direction
	
    def _prop_name(self):
        return f"Move({self.direction})"
	
    def _precond(self, S):
        lowX = LOWER+1 if self.direction == "W" else LOWER
        lowY = LOWER+1 if self.direction == "S" else LOWER
        highX = UPPER if self.direction == "E" else UPPER+1
        highY = UPPER if self.direction == "N" else UPPER+1
		
        for i in range(lowX, highX):
            for j in range(lowY, highY):
                props.append(S.Loc(i,j))
		
        return Or(props)

def init(S):
    props = [S.Loc(LOWER, LOWER)]
    for i in range(LOWER, UPPER):
        for j in range(LOWER, UPPER):
            if i != 0 or j != 0:
                props.append(~(S.Loc(i,j)))
    return And(props)

def goal(S):
    return S.Loc(UPPER, UPPER)

locs = {i: {j: Loc(i,j) for j in range(2)} for i in range(2)}
actions = {Act(d) for d in 'NSEW'}

e.compile(init=init, goal=goal, horizon=5)

Implementation Details

Every new instance of @stateprop and @actionprop propositions can be logged as they are created. The .compile(...) will create a single version of all props, and these need to be cloned for every state in the horizon (and actions in between them). Prop names can be the original with @Si added for each layer i. Then all of the constraints need to be created for each state/action in the horizon (using the class-defined procedures).

Unclear if the use of bauhaus.And and bauhaus.Or inside those methods will work, as they likely need to be nnf variables by the time those constraints start to be formed. Flattening is also something that should probably be done automagically, as chains of conjunctions or disjunctions may be quite common.