Last modified 3 years ago Last modified on 17/09/18 15:52:58

CLIPS-based SMT Planning approach plugin

The plugin clips-smt offers the functionality to generate a plan for an order and a world state in the RCLL domain (which is encoded in an instance of the protobuf message llsf_msgs/ClipsSmtData.proto). Internally it uses the z3 SMT solver to encode and solve a FOL formula and returns the desired sequential/concurrent plan. On the agent side this plan has to be extracted from a protobuf message and distributed to all participating robots.


We use the plugin navgraph to obtain distances between the machines and provide the possibility to communicate with the plugin via CLIPS after loading it.


After passing an instance of src/libs/llsf_msgs/ClipsSmtData.proto data describing the current world state the plugin clips-smt generates a plan for the given order and returns it to the caller.

Compilation and Runtime Requirements

We make use of the z3 SMT solver to encode and solve the formula describing the domain. The required packages can be build manually following the instructions on the website or be installed via the command:

dnf install z3-devel

Usage Instructions

After loading, beside some initialization, the plugin does nothing unless it is called via the CLIPS environment with the fact

(smt-request "smt-plan" ?data)

and used via the function

(bind ?plans (smt-get-plan ?handle))

after the plugin generated a plan. Details on how to use the plugin clips-smt and how the protobuf message looks like can be found here.


The plugin offers the functionality to expand a order connected to some goal. Once it is called via some rule in CLIPS a loop function ClipsSmtThread::loop() is activated.

  1. Clear data of previous calls and preprocess data given via a protobuf datastructure consisting of the current worldstate with ClipsSmtThread::clips_smt_init_game().
  2. Encode a formula based on the extracted data with ClipsSmtThread::clips_smt_encoder().
  3. Solve the formula and store the plan information of the model with ClipsSmtThread::clips_smt_solve(z3::expr formula).
  4. Tell the agent that the loop reached its end via
    envs_[data_env]->assert_fact_f("(smt-plan-complete \"%s\")", data_handle.c_str());

Now the agent has the possibility to demand a protobuf datastructure consisting of the plan by calling following method

ClipsSmtThread::clips_smt_request(std::string env_name, std::string handle, void *msgptr)

The principles of the encoder can be found here.