人工智能代写 | COMP3620/6320 Articial Intelligence Assignment 3: SAT-Based Planning

本次澳洲代写主要为python AI SAT计划系统的assignment

1 Background
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 files) 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
fluent 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 figure at the top of this handout is a graphical representation of the precondition and effect clauses
in a five-step encoding of a small logistics problem. The blue nodes represent fluents and the red nodes
represent actions. There is an arc between an action and a fluent if they appear in a precondition or
effect 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 specified as a domain PDDL file and a problem PDDL file. 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 satisfiable, the
system extracts and attempts to validate a plan from the satisfying assignment returned by the SAT
solver.
Due to the dependence on pre-compiled binaries for grounding and SAT solving and Unix-specific system
calls to run these binaries and manage the temporary files 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
the command:
python3 planner.py DOMAIN PROBLEM EXPNAME HORIZON [options]
where
• DOMAIN is the PDDL domain file.
• PROBLEM is the PDDL problem file.
• EXPNAME is an arbitrary string used to store temporary files of the experiment.
• HORIZONS is used to set a maximum number of time steps. Different 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 specifies the file in which the resulting plan is stored (default: None).
• -q QUERY specifies 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:
false).
• -l PGCONS specifies 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 fluent mutex axioms (Exercise 8).
– reachable includes just reachable action axioms (Exercise 7).
– both includes both sets of axioms.
• -x EXECSEM specifies the execution semantics (default: parallel):
– serial means that at most one action can be executed per time step (Exercise 5).

– parallel means that multiple actions per time step can be selected as long as any order is
a valid one (Exercise 6).
• -e ENCODING specifies the CNF encoding to be used (default: basic). You can also select lo-
gistics to activate the advanced exercise.
• -s SOLVER selects the SAT solver to use. There is only one installed with the system currently, so
ignore this option.
• -t TIMEOUT specifies an optional timeout (in seconds) for each run of the SAT solver (default:
None).
• -d DBGCNF is a boolean that specifies if the system should generate a CNF file annotated with
variable names for you to use to debug your encodings. If set to true, it outputs a .cnf_dbg file
into the tmp_files directory. If there’s an error in your implementation and you’re not sure what
the problem is, turn this flag to true and manually examine the debug file. (default: false).
• -r REMOVETMP is a boolean that specifies whether the system has to remove the temporary files
generated (default: false).


程序代写代做C/C++/JAVA/安卓/PYTHON/留学生/PHP/APP开发/MATLAB


blank

本网站支持淘宝 支付宝 微信支付  paypal等等交易。如果不放心可以用淘宝交易!

E-mail: itcsdx@outlook.com  微信:itcsdx


如果您使用手机请先保存二维码,微信识别。如果用电脑,直接掏出手机果断扫描。

blank

发表评论