本次澳洲代写主要为Python AI SAT计划系统的assignment
SAT-based planning is a powerful approach to solve planning problems that relies on unrolling a propo-
sitional logic theory over time and checking whether or not a parallel plan exists.
Early SAT encodings of planning problems were generated by hand, but now SAT based planners provides
automatic grounding for the actions, reachability analysis (to prune provably unreachable propositions
or actions), and automatic translation to the corresponding formula.
Today SAT-based planning techniques do best when solving planning problems that allow for a high
degree of parallelism and where the number of time steps to reach a goal state is not very high.
In this assignment you will implement various automatic translations of STRIPS planning instances
(supplied as PDDL ﬁles) into SAT. The tedious part of the work has already been done (grounding the
PDDL into objects representing STRIPS actions and propositions, generating a plangraph that computes
ﬂuent mutex relationships, calling the SAT solver with the encodings you generate, and validating the
resulting plans). This should allow you to focus on the fun parts, that is generating CNF encodings of
planning problems and interpreting the solutions found by the SAT solver.
The ﬁgure at the top of this handout is a graphical representation of the precondition and eﬀect clauses
in a ﬁve-step encoding of a small logistics problem. The blue nodes represent ﬂuents and the red nodes
represent actions. There is an arc between an action and a ﬂuent if they appear in a precondition or
eﬀect clause together.
2 Preliminary: The Planning System
In this assignment you will complete parts of a SAT-based planning system implemented in Python.
This system uses some pre-compiled binaries for grounding the planning problem and solving the SAT
instances your encodings will create.
The planner takes a planning problem speciﬁed as a domain PDDL ﬁle and a problem PDDL ﬁle. It then
uses the selected encoding (and other options) to generate and solve CNF SAT instances with planning
horizons chosen by the selected query (evaluation) strategy. If one of these instances is satisﬁable, the
system extracts and attempts to validate a plan from the satisfying assignment returned by the SAT
Due to the dependence on pre-compiled binaries for grounding and SAT solving and Unix-speciﬁc system
calls to run these binaries and manage the temporary ﬁles created by the system, the system is only
guaranteed to work on x64 Linux and Mac machines. If you are using Windows 10, we suggest doing
this assignment inside the Windows Subsystem for Linux.
If you have trouble with the supplied binaries gringo and precosat, you can obtain other binaries and
source from https://potassco.org/ and http://fmv.jku.at/precosat/.
To display details about how to run the system, use python planner.py -h. The planner is run with
python3 planner.py DOMAIN PROBLEM EXPNAME HORIZON [options]
• DOMAIN is the PDDL domain ﬁle.
• PROBLEM is the PDDL problem ﬁle.
• EXPNAME is an arbitrary string used to store temporary ﬁles of the experiment.
• HORIZONS is used to set a maximum number of time steps. Diﬀerent options can be selected:
– If the fixed query strategy is chosen, then the horizon should be a list of planning horizons
separated by : characters. For example, 1:5:7 would plan for the horizons 1, 5, and 7.
– If the ramp query strategy is chosen, then the horizon should be three numbers start:end:step
– the starting horizon, end horizon, and horizon step size. For example, 2:8:2 would plan at
the horizons 2, 4, 6, and 8.
See below on how to select the query strategy.
• -o OUTPUT speciﬁes the ﬁle in which the resulting plan is stored (default: None).
• -q QUERY speciﬁes the query strategy to be used: either fixed (default) or ramp.
• -p PLANGRAPH is a boolean specifying whether graphplan preprocessing is used or not (default:
• -l PGCONS speciﬁes what constraints should be included in encodings from the plangraph (default:
both). Note that this option only works when you turn plangraph on with -p true):
– fmutex includes just the ﬂuent mutex axioms (Exercise 8).
– reachable includes just reachable action axioms (Exercise 7).
– both includes both sets of axioms.
• -x EXECSEM speciﬁes the execution semantics (default: parallel):
– serial means that at most one action can be executed per time step (Exercise 5).
本网站支持淘宝 支付宝 微信支付 paypal等等交易。如果不放心可以用淘宝交易！
E-mail: firstname.lastname@example.org 微信:itcsdx