Engine for unified-planning, implementing a SMT solver.
Reason this release was yanked:
The issue is being caused by a z3 bug
Project description
SMT based engine implementation for unified-planning
Introduction
An engine using satisfiability modulo theories to solve planning problems. This engine uses z3 as an out of the box solver.
Status
pip integration incomplete Solver tested and functional Solver capable of sequential, ForAll, ThereExists and relaxed relaxed ThereExists parallelism Solver accepts and returns the expected unified-planning problem and PlanGenerationResult
Planning approaches of UP supported
- Problem kind: Numeric planning with instantaneous actions
- Operative mode: One shot planning
Engine Options
max_length
Read known user-options and store them for using in the solve
method
Set a maximum plan length bound
parallelism
Option choosing the type of parallalelism. Chooses between 'sequential', 'ForAll', 'ThereExists' and 'relaxed_relaxed_ThereExists' 'sequential' corresponds to a traditional approach, choosing one action per timestep 'ForAll' corresponds to temporal parallelism, choosing a set of non-interfering actions per timestep 'ThereExists' chooses a set of actions for each timestep such that there is at least one valid sequential ordering. This corresponds to sequential plans and aims to improve performance 'relaxed_relaxed_ThereExists' is a relaxation of ThereExists, and aims to increase the number of possible actions per step further, at the cost of individual steps becoming more expensive
ForAll_get_sets
Option choosing whether to output a partial order plan for ForAll parallelism to see the parallel action sets
use_incremental_solving
Option choosing the whether to use SMT's incremental solving or not Incremental solving preserves learned clauses after a plan length has been found unsatisfiable, reducing search for the next step at the cost of requiring more clauses maintained
stats_output
If a string is provided then generate statistics, and save to file, using stats_output as filepath
unit_test
Get action sequence for unit tests
Installing
TODO implement pip method
Clone from https://gitlab.com/BPat123/up-smt-engine Dependencies: unified-planning, z3
Usage
See 'test_runner.py' and 'unit_tests.py' for usage examples
To run all options against a PDDL file use this command: python3 test_runner.py -timeout "$TIMEOUT_VAL" -test_all -use_PDDL -domain_path "$domain_string" -problem_path "$problem_string" -solution_path "$problem_results_path"
$TIMEOUT_VAL: timeout in seconds $domain_string: PDDL domain file path $problem_string: PDDL problem file path $problem_string: PDDL problem file path $problem_results_path: Plan output path n.b. the plan output is in PDDL format, and can be verified using programs such as VAL
e.g. python3 up-smt-engine/test_runner.py -timeout 100 -test_all -use_PDDL -domain_path tests/counters/domain.pddl -problem_path tests/counters/problem.pddl -solution_path counters/solution.txt
Documentation
Documentation (generated by code Docstring)
License
MIT
CHANGELOG
Project details
Release history Release notifications | RSS feed
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for upSmtEngine-2023.6.26.2-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | cdc00ff6061c5520e0a44da402a7ac2816950cc90e07428aae6b155afa8e4fbc |
|
MD5 | ab0ea630b24d4b471d95ebf13224374b |
|
BLAKE2b-256 | fb0151ab7882c0a4af502e5ef01ddab7f13c4aa81402eb30930f722c1b813e04 |