Skip to main content

Engine for unified-planning, implementing a SMT solver.

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


Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

upSmtEngine-2023.6.27.5.tar.gz (1.8 MB view details)

Uploaded Source

Built Distribution

upSmtEngine-2023.6.27.5-py3-none-any.whl (43.5 kB view details)

Uploaded Python 3

File details

Details for the file upSmtEngine-2023.6.27.5.tar.gz.

File metadata

  • Download URL: upSmtEngine-2023.6.27.5.tar.gz
  • Upload date:
  • Size: 1.8 MB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/4.0.2 CPython/3.10.6

File hashes

Hashes for upSmtEngine-2023.6.27.5.tar.gz
Algorithm Hash digest
SHA256 c96ca3c224a09828fbfea4b98399faf53ba91e994da7103fc402b4f60e9ca29c
MD5 e33fffe9f3e161253a6a397ded1d3320
BLAKE2b-256 270b51a3b1f7c7b3271df6d6609159ff026b0e8a129b90350bb1222989d6242c

See more details on using hashes here.

File details

Details for the file upSmtEngine-2023.6.27.5-py3-none-any.whl.

File metadata

File hashes

Hashes for upSmtEngine-2023.6.27.5-py3-none-any.whl
Algorithm Hash digest
SHA256 d8cfc0bc9a6208d11c5f57a7241e627e006fbede55662074926474ad8d5a22f0
MD5 b76739bf790218387408aba084e3a32e
BLAKE2b-256 ca0c935d0a0a1b87d0f649f0d3067a7c9f3b6f74afea91cf5d9fe145f390e35e

See more details on using hashes here.

Supported by

AWS AWS Cloud computing and Security Sponsor Datadog Datadog Monitoring Fastly Fastly CDN Google Google Download Analytics Microsoft Microsoft PSF Sponsor Pingdom Pingdom Monitoring Sentry Sentry Error logging StatusPage StatusPage Status page