b’8536a7573645ed5a187b25536a99102e0aa980′
blob 23722�# COMP3620/6320 Artificial Intelligence
# The Australian National University – 2021
# Authors: COMP3620 team
“”” Student Details
Student Name: Boxuan Yang
Student ID: u6778195
Email: u6778195@anu.edu.au
Date: May 26, 2021
“””
“”” This file contains the methods you need to implement to create a basic
(non-split) encoding of planning as SAT.
You can work your way through the exercises below to build up the encoding.
We strongly recommend that you test as you go on some of the smaller
benchmark problems.
Here is a simple example to run the problem on the smallest Miconics
instance:
python3 planner.py benchmarks/miconic/domain.pddl benchmarks/miconic/problem01.pddl miconic1 4
You might want to implement the plan extraction method after you implement
the method to create the CNF variables. You will then be able to generate
(probably incorrect) plans as you add more constraints.
To test the fluent mutex axioms and reachable action axioms you will need
to turn on the plangraph computation “-p true”.
Remember, it is relatively easy to figure out where you have gone wrong if
the SAT solver finds invalid plans. For example if the plan validator
indicates that an action has an unsatisfied precondition, then there is
probably something wrong with your precondition clauses or your frame
axioms. However, if the SAT instance is unsatisfiable, then you will likely
have to start removing constraints to figure out where you went wrong.
To help you debug your encoding, you can use the argument “-d true” to
write an annotated CNF file with the clauses you are generating. Warning:
Looking through this for large problems will be nearly impossible, so test
on the small instances.
Sometimes SAT encodings of planning problems can end up BIG because there
are just so many actions. Either use the argument “-r true” or clear out
your tmp_files directory periodically and manually.
This system is designed to run on either Linux or Mac machines. This is
unavoidable because we need to call and run external grounding and SAT
solving programs.
This software will NOT work on Windows. We suggest using a virtual machine,
or working in the labs if you do not have a linux installation.
“””
from typing import Dict, List, Tuple
from strips_problem import Action, Proposition
from utilities import encoding_error_code
from .encoding_base import Encoding, EncodingException
import time
encoding_class = ‘BasicEncoding’
class BasicEncoding(Encoding):
“”” A simple basic encoding along the lines of SatPlan06 with full frame
axioms.
Variables and clauses are created once
“””
################################################################################
# You need to implement the following methods #
################################################################################
def make_variables(self, horizon: int) -> None:
“”” Make the variables (state and action fluents) for the problem.
Exercise 1 – 5 Marks
The method self.new_cnf_code(step, name, object) will return an int
representing a new CNF variable for you to use in your encoding.
Let k be the horizon which is passed as a parameter. Use the above
method to make one variable for each Proposition at each step 0..k
and one variable for each Action at each step from 0..k-1.
Access the actions and propositions from the lists
self.problem.actions and self.problem.propositions.
Use str(proposition) to get name of a proposition and str(action)
to get the name of an action when calling self.new_cnf_code.
For object, you should just pass either the Proposition or Action
object.
So, self.new_cnf_code(4, str(a), a) will create a new variable and
return a code (an int) representing the CNF variable for action a,
at step 4.
Since you will need to use these variables to make your constraints
later, you should store them in self.action_fluent_codes and
self.proposition_fluent_codes.
These should map each (Action, step) pair and each (Proposition,
step) pair to the appropriate code.
Once you have made the variables, you can get the step, name, and
object (Action or Proposition) with the following:
– self.cnf_code_steps[code]
– self.cnf_code_names[code]
– self.cnf_code_objects[code]
You shouldn’t need to use these until you come to extract the plan
generated by the SAT solver, but they might be useful for
debugging!
“””
self.action_fluent_codes: Dict[Tuple[Action, int], int] = {}
self.proposition_fluent_codes: Dict[Tuple[Proposition, int], int] = {}
“”” YOUR CODE HERE “””
for k in range(horizon):
for action in self.problem.actions:
code = self.new_cnf_code(k, str(action), action)
self.action_fluent_codes[(action, k)] = code
for k in range(horizon + 1):
for proposition in self.problem.propositions:
code = self.new_cnf_code(k, str(proposition), proposition)
self.proposition_fluent_codes[(proposition, k)] = code
def make_initial_state_and_goal_axioms(self, horizon: int) -> None:
“”” Make clauses representing the initial state and goal.
Exercise 2 – 5 Marks
In this method, add clauses to the encoding which ensure that the
initial state of the problem holds at step 0. The Propositions
which must be true are in self.problem.pos_initial_state and the
Propositions which must be false are in
self.problem.neg_initial_state.
Every Proposition in the problem will be in one of these two sets.
Also add clauses which ensure that the goal holds at the horizon.
Similarly to the start state, the goal clauses are in
self.problem.goal.
Not every Proposition will be in the goal. The truth values of
other Propositions should remain unconstrained.
A clause is a list of positive or negative integers (representing
positive and negative literals) using the variables you created
for Q1. Get the variables from self.proposition_fluent_codes).
Every clause has a type, which is represented by a string.
Add clauses to the encoding with self.add_clause(clause,
clause_type).
The type of the start state clauses should be “start” and the type
of the goal clauses should be “goal”.
“””
“”” *** YOUR CODE HERE *** “””
start_count = 0
goal_count = 0
for pos_proposition in self.problem.pos_initial_state:
code = self.proposition_fluent_codes[(pos_proposition, 0)]
start_count += 1
self.add_clause([code], “start”)
for neg_proposition in self.problem.neg_initial_state:
code = self.proposition_fluent_codes[(neg_proposition, 0)]
start_count += 1
self.add_clause([-code], “start”)
for goal_proposition in self.problem.goal:
code = self.proposition_fluent_codes[(goal_proposition, horizon)]
goal_count += 1
self.add_clause([code], “goal”)
print(“start: “, start_count)
print(“goal: “, goal_count)
def make_precondition_and_effect_axioms(self, horizon: int) -> None:
“”” Make clauses representing action preconditions and effects.
Exercise 3 – 5 Marks
In this method, add clauses to the encoding which ensure that
If an action is executed at step t = 0..k-1:
– its preconditions hold at step t and
– its effects hold at step t+1.
(No action will both add and delete the same proposition)
Add clauses with self.add_clause(clause, clause_type).
In your clauses use the variables from self.action_fluent_codes and
self.proposition_fluent_codes.
Precondition clauses have the type ‘pre’ and effect clauses have the
type “eff”.
Don’t forget to look in strips_problem.py for the data structures
you need to use!
“””
“”” *** YOUR CODE HERE *** “””
pre_count = 0
eff_count = 0
for action in self.problem.actions:
for k in range(horizon):
action_code = self.action_fluent_codes[(action, k)]
for precondition in action.preconditions:
precondition_code = self.proposition_fluent_codes[(precondition, k)]
pre_count += 1
self.add_clause([-action_code, precondition_code], “pre”)
for pos_effect in action.pos_effects:
pos_effect_code = self.proposition_fluent_codes[(pos_effect, k + 1)]
eff_count += 1
self.add_clause([-action_code, pos_effect_code], “eff”)
for neg_effect in action.neg_effects:
neg_effect_code = self.proposition_fluent_codes[(neg_effect, k + 1)]
eff_count += 1
self.add_clause([-action_code, -neg_effect_code], “eff”)
print(“pre: “, pre_count)
print(“eff: “, eff_count)
def make_explanatory_frame_axioms(self, horizon: int) -> None:
“”” Make clauses representing explanatory frame axioms.
Exercise 4 – 10 Marks
In this method, add clauses to the encoding which ensure that
If a proposition p is true at step t = 1..k:
– either p is true at t-1 or
– an action is executed at t-1 which added p.
If a proposition p is false at step t = 1..k:
– either p is false at t-1 or
– an action is executed at t-1 which deletes p
Add clauses with self.add_clause(clause, clause_type).
In your clauses use the variables from self.action_fluent_codes
and self.proposition_fluent_codes.
These clauses have the type “frame”.
To make this process easier, Proposition objects have lists of
the actions
which have them as positive and negative and effects.
“””
“”” *** YOUR CODE HERE *** “””
frame_count = 0
for proposition in self.problem.propositions:
for k in range(horizon):
l = []
l.append(self.proposition_fluent_codes[(proposition, k)])
l.append(-self.proposition_fluent_codes[(proposition, k + 1)])
for action in self.problem.actions:
if proposition in action.pos_effects:
l.append(self.action_fluent_codes[(action, k)])
self.add_clause(l, “frame”)
frame_count += 1
l = []
l.append(-self.proposition_fluent_codes[(proposition, k)])
l.append(self.proposition_fluent_codes[(proposition, k + 1)])
for action in self.problem.actions:
if proposition in action.neg_effects:
l.append(self.action_fluent_codes[(action, k)])
self.add_clause(l, “frame”)
frame_count += 1
print(“frame: “, frame_count)
def make_serial_mutex_axioms(self, horizon: int) -> None:
“”” Make clauses representing serial mutex.
Exercise 5 – 10 Marks
In this method, add clauses to the encoding which ensure that at
most one action is executed at each step t = 0..k-1. (It could be
the case that no actions are executed at some steps).
To get full marks, you should add as few clauses as possible.
Notice that actions with conflicting effects are already prevented
from being executed in parallel.
Add clauses with self.add_clause(clause, clause_type).
In your clauses use the variables from self.action_fluent_codes.
These clauses have the type “mutex”.
“””
“”” *** YOUR CODE HERE *** “””
mutex_count = 0
actions = self.problem.actions.copy()
for action in actions:
if set(action.pos_effects) & set(action.neg_effects) != set():
actions.remove(action)
for i in range(len(actions)):
a1 = actions[i]
for j in range(i + 1, len(actions)):
a2 = actions[j]
if a1 == a2:
continue
if set(a1.pos_effects) & set(a2.neg_effects) != set(): # if they have inconsistent effects
continue
if set(a2.pos_effects) & set(a1.neg_effects) != set(): # if they have inconsistent effects
continue
for t in range(horizon):
a1_code = self.action_fluent_codes[(a1, t)]
a2_code = self.action_fluent_codes[(a2, t)]
self.add_clause([-a1_code, -a2_code], “mutex”)
mutex_count += 1
print(“mutex_q5: “, mutex_count)
def make_interference_mutex_axioms(self, horizon: int) -> None:
“”” Make clauses preventing interfering actions from being executed in parallel.
Exercise 6 – 10 Marks
In this method, add clauses to the encoding which ensure that two
actions cannot be executed in parallel at a step t = 0..k-1 if they
interfere.
Two actions a1 and a2 interfere if there is a Proposition p such
that p in EFF-(a1) and p in PRE(a2).
To get full marks, you should not add clauses for interfering
actions if their parallel execution is already prevented by
conflict due to effect clauses. Also, careful not to add duplicate
clauses!
If you find your encoding time to be slow, it might be due to an
inefficient implementation of this function. As a hint to make it
faster, make use of the `neg_effects` and `preconditions`
attributes stored in Proposition objects, instead of the
`neg_effects` and `preconditions` attributes in Action objects.
Add clauses with self.add_clause(clause, clause_type).
In your clauses use the variables from self.action_fluent_codes.
These clauses have the type “mutex”.
“””
“”” *** YOUR CODE HERE *** “””
mutex_count = 0
added = set()
for proposition in self.problem.propositions:
for a1 in set(proposition.preconditions):
for a2 in set(proposition.neg_effects):
if a1 == a2:
continue
if set(a1.pos_effects) & set(a2.neg_effects) != set(): # if they have inconsistent effects
continue
if set(a2.pos_effects) & set(a1.neg_effects) != set(): # if they have inconsistent effects
continue
if (a1, a2) in added:
continue
added.add((a1, a2))
added.add((a2, a1))
for t in range(horizon):
a1_code = self.action_fluent_codes[(a1, t)]
a2_code = self.action_fluent_codes[(a2, t)]
self.add_clause([-a1_code, -a2_code], “mutex”)
mutex_count += 1
print(“mutex_q6: “, mutex_count)
def make_reachable_action_axioms(self, horizon: int) -> None:
“”” Make unit clauses preventing actions from being executed before they
become available in the plangraph.
Exercise 7 – 5 Marks
In this method, add clauses to the encoding which ensure that an
action is not executed before the first step it is available in
self.problem.action_first_step.
For example, if self.problem.action_first_step[action1] == 5, then
you would introduce clauses stopping action1 from being executed at
steps 0..4.
These clauses are not required for correctness, but may improve
performance.
Add clauses with self.add_clause(clause, clause_type).
In your clauses use the variables from self.action_fluent_codes.
These clauses have the type “reach”.
“””
“”” *** YOUR CODE HERE *** “””
reach_count = 0
for action in self.problem.actions:
first = min(horizon, self.problem.action_first_step[action]) # or min???
for t in range(first):
self.add_clause([-self.action_fluent_codes[(action, t)]], “reach”)
reach_count += 1
print(“reach: “, reach_count)
def make_fluent_mutex_axioms(self, horizon: int) -> None:
“”” Make clauses representing fluent mutex as computed by the plangraph.
Exercise 8 – 5 Marks
In this method, add clauses to the encoding which ensure that pairs
of propositions cannot both be true at the same time. These
constraints are computed when the plangraph is generated.
These clauses are not required for correctness, but usually make
planning faster by causing the SAT solver to backtrack earlier.
The dictionary self.problem.fluent_mutex maps integers representing
planning steps to lists of proposition mutex relationships at each
step from 1…n, where n is the step that the plangraph levels off.
Note that the dictionary doesn’t contain steps greater than n,
because the relationships at step n also hold for every step
greater than n. Thus you can get those mutex relationships by
querying the dictionary with step n.
You can get n by getting the largest key in
self.problem.fluent_mutex maps.
It is possible that the current horizon is less than n. In this
case, mutex relationships larger than the horizon should, of
course, be ignored.
As the initial state clauses completely determine the truth values
of fluents at step 0, there is no need for fluent mutex clauses
there.
Each list of mutex relationships in self.problem.fluent_mutex will
be as follows:
[(f1, f2), ….]
Say, we have (f1, f2), then there should be a clause [-f1, -f2]
(obviously substituting the appropriate CNF codes for f1 and f2,
depending on the step.
Add clauses with self.add_clause(clause, clause_type).
In your clauses use the variables from
self.proposition_fluent_codes.
These clauses have the type “fmutex”.
“””
“”” *** YOUR CODE HERE *** “””
fmutex_count = 0
n = max(self.problem.fluent_mutex.keys())
for t in range(1, horizon + 1):
if t > n:
mutex = self.problem.fluent_mutex[n]
for pair in mutex:
prop1, prop2 = pair
prop1_code = self.proposition_fluent_codes[(prop1, t)]
prop2_code = self.proposition_fluent_codes[(prop2, t)]
self.add_clause([-prop1_code, -prop2_code], “fmutex”)
fmutex_count += 1
else:
mutex = self.problem.fluent_mutex[t]
for pair in mutex:
prop1, prop2 = pair
prop1_code = self.proposition_fluent_codes[(prop1, t)]
prop2_code = self.proposition_fluent_codes[(prop2, t)]
self.add_clause([-prop1_code, -prop2_code], “fmutex”)
fmutex_count += 1
print(“fmutex: “, fmutex_count)
def build_plan(self, horizon: int) -> None:
“””Build a plan from the true variables in a satisfying valuation found
by the SAT solver.
Exercise 9 – 5 marks
self.true_vars is a set with the codes of the CNF variables which the
SAT solver has set to true in the satisfying valuation it found.
You can get the step, name, and object (Action/Proposition) of each variable
(state or action fluent) with:
– self.cnf_code_steps[code]
– self.cnf_code_names[code]
– self.cnf_code_objects[code]
You can check if an object is an Action or Proposition with
– isinstance(obj, Action) and
– isinstance(obj, Proposition)
You should add the plan to self.plan, which has the structure
[action_list, action_list, …].
For each step t = 0..k-1, it has a (possibly empty) list of the
actions which were executed at that step.
So, if we have a0 and a1 at step 0 and a2 at step 2, then self.plan
will be:
[[a0, a1], [], [a2]]
where a0, a1, a2, etc. are Action objects (not just their names).
The system will validate the plans you generate, so make sure you
test your encodings on a number of different problems.
“””
self.plan: List[List[Action]] = []
“”” *** YOUR CODE HERE *** “””
self.plan = [[] for i in range(horizon)]
for code in self.true_vars:
obj = self.cnf_code_objects[code]
if isinstance(obj, Action):
step = self.cnf_code_steps[code]
self.plan[step].append(obj)
################################################################################
# Do not change the following method #
################################################################################
def encode(self, horizon: int, exec_semantics: str, plangraph_constraints: str) -> None:
“”” Make an encoding of self.problem for the given horizon.
For this encoding, we have broken this method up into a number
of sub-methods that you need to implement.
“””
self.make_variables(horizon)
self.make_initial_state_and_goal_axioms(horizon)
self.make_precondition_and_effect_axioms(horizon)
self.make_explanatory_frame_axioms(horizon)
if exec_semantics == “serial”:
self.make_serial_mutex_axioms(horizon)
elif exec_semantics == “parallel”:
self.make_interference_mutex_axioms(horizon)
else:
assert False
if self.problem.fluent_mutex is not None:
# These constraints will only be included if the plangraph was computed
if plangraph_constraints == “both”:
self.make_reachable_action_axioms(horizon)
self.make_fluent_mutex_axioms(horizon)
elif plangraph_constraints == “fmutex”:
self.make_fluent_mutex_axioms(horizon)
elif plangraph_constraints == “reachable”:
self.make_reachable_action_axioms(horizon)