This repository implements the approach from the NFM 2024 paper "SMT-Based Dynamic Multi-Robot Task Allocation". Please see below for instructions for installation and how to run the software.
To install the necessary requirements for this project, enter the following:
$ pip3 install -r requirements.txt
The Bitwuzla Python API is also required to use Bitwuzla as the underlying SMT solver. Check out the above link for installation instructions.
The implementation supports the following options:
$ python3 src/MRTASolver.py --help
usage: MRTASolver.py [-h] --file FILE [--solver {bitwuzla,z3,cvc5}] [--theory {QF_UFBV,QF_UFLIA}] [--capacity CAPACITY] [--timeout TIMEOUT] [--num_aps NUM_APS]
[--export EXPORT] [--incremental] [--verbose] [--fidelity FIDELITY] [--deadline DEADLINE] [--keep_aps]
SMT-based approach to solve the multirobot task allocation (MRTA) problem.
options:
-h, --help show this help message and exit
--file FILE, -f FILE Path to the file containing the MRTA problem instance.
--solver {bitwuzla,z3,cvc5}, -s {bitwuzla,z3,cvc5}
Solver to be used to solve the problem.
--theory {QF_UFBV,QF_UFLIA}, -th {QF_UFBV,QF_UFLIA}
Theory to be used to solve the problem.
--capacity CAPACITY, -c CAPACITY
Capacity of the robots.
--timeout TIMEOUT, -t TIMEOUT
Timeout in seconds.
--num_aps NUM_APS, -n NUM_APS
Number of action points to be used. Default minimum possible used.
--export EXPORT, -e EXPORT
Basename for exported smt file.
--incremental, -i Use incremental solving.
--verbose, -v Prints more information.
--fidelity FIDELITY, -fi FIDELITY
Fidelity of travel time.
--deadline DEADLINE, -d DEADLINE
Default deadline for tasks.
--keep_aps Keep previously allocated action points.
Only the --file
flag is required. The file describes the how tasks arrive and should be in the json
format. Examples of such are stored in the config
directories under the benchmark
.
An example of running a specific setting would be:
python3 src/MRTASolver.py -f benchmark/single/config/t_20_a_10_d_5-0.json
To run SMT files directly, please download z3 and Bitwuzla binaries from their respective repositories. SMT files are stored under the benchmark
directory.