Skip to content

Instantly share code, notes, and snippets.

@ssardina

ssardina/AOPROGRAMMING.md Secret

Last active October 14, 2022 09:26
Show Gist options
  • Save ssardina/25ec9fce066562c124a1e590e19569c3 to your computer and use it in GitHub Desktop.
Save ssardina/25ec9fce066562c124a1e590e19569c3 to your computer and use it in GitHub Desktop.
Download ZIP
Planners and Synthesis
Raw
AOPROGRAMMING.md

Agent Programming

BDI-type Systems

  • JACK: a comercial BDI programming language and development platform.
  • JADEX (and GitHub repo): The Jadex Active Components Framework provides programming and execution facilities for distributed and concurrent systems.
  • GOAL.
  • 3APL and 2APL: programming languages for implementing cognitive agents.

Golog-like systems

  • Golog++: an interfacing and development framework for GOLOG languages.
  • IndiGolog: an incremental version of ConGolog with a local search operator.

Others

  • SARL: a general purpose agent-oriented programming language.
Raw
CONSTRAINTS.md

Constraint Programming

SAT Solvers

  • z3: Z3 is a theorem prover from Microsoft Research. Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.
  • MiniSAT: MiniSat is a minimalistic, open-source SAT solver.
  • CryptoMiniSAT: an online solver.
  • SAT4j: SAT solver in Java.

ASP Solvers

About Answer Set Programming:

Systems:

Model Counters

Model counting is the problem of determining the number of assignments satisfying a given propositional formula (typically represented as a CNF). Model counting, and weighted model counting, are central to many AI problems including probabilistic inference. Model counting is #P-complete, and hard to approximate. It is also often supported by knowledge compilers.

Check http://beyondnp.org/pages/solvers/model-counters-exact/

Kowledge Compilation

Knowledge compilation is concerned with converting general types of knowledge into tractable forms, which allows certain hard tasks to be performed efficiently on the compiled forms. For example, one may compile a CNF into an OBDD, allowing one to count the models of the CNF efficiently and under different variable settings. Many of the compiled forms are based on subsets of Negation Normal Form (NNF) including, for example, Ordered Binary Decision Diagrams (OBDD), Sentential Decsion Diagrams (SDD), and Decomposable Negation Normal Form (DNNF).

See here: http://beyondnp.org/pages/solvers/knowledge-compilers/

Optimizers

  • SMT-RAT: Satisfiability-Modulo-Theories Real Algebra Toolbox.
Raw
PLANNING.md

Planning & Synthesis Information, Tools, and Systems

Automated Planning is a core AI technique to automatically synthesize goal-oriented plans (for a robot or a video game character). It is a type of program synthesis.

Much of the information and link below overlap with the Planning Wiki; in particular the Wiki has:

There is also an open and very active Slack Planning Community.

This list is being compiled by Sebastian Sardina (ssardina@gmail.com), mostly as self-reference and as a bookmark. If you know of something that could be listed here, please send it to me and I will add it!

PDDL Info & Documentation

Some general intro coverage of planning:

More specific:

Community and Research Groups & Events

Benchmarks

  • PDDL Instances @ Potsasco: IPC domains from 1998-2014. It includes for example numeric domains in IPC-02.
  • Classical Domains: This repository is a simple collection of PDDL files. Currently only classical problems are included.
  • PDDL Generators: This repository is a collection of PDDL generators, some of which have been used to generate benchmarks for the International Planning Competition (IPC). C

Classical

  • Fastdownward: a platform, which has become the canonical -- highly efficient-- implementation basis for classical AI Planning research.
  • FF Planner Family.
  • PASAR: SAT-based planner with Abstraction Refinement. Presented first at SOCS 2019 here.
    • It does not take PDDL files but SAS files. These can be generated with FD Translator
  • LTL goals Classical Planner: Infinite Plans for LTL Goals Using a Classical Planner is a work by F. Patrizi, N. Lipovetzky, G. De Giacomo, H. Geffner.
  • Planners @ LAPKT: Lightweight Automated Planning Toolkit. Also see Wiki. It contains a collection of planners that can be compiled and used almost on-the-spot. It supports some planners on both the FF parser and the (more involved) FD parser. Check the various planners here.
    • The library includes a number of Width/Novelty-based planning systems (SIW). Thoe library ignores cost by default, but one can switch-off the ignore-cost flag, making sure that the main.cxx of the planner doesn't set this flag to true: ff-parser and fd-parser
  • BFWS: Best First Width Search Planner. A very simple and high-performance planner based on novelty. Uses LAPKT library.
  • Pyperplan is a lightweight STRIPS planner written in Python. Please note that Pyperplan deliberately prefers clean code over fast code. It is designed to be used as a teaching or prototyping tool. If you use it for paper experiments, please state clearly that Pyperplan does not offer state-of-the-art performance.

Numeric

  • Metric-FF: The system is an extension of the FF planner to (ADL combined with) numerical state variables, more precisely to PDDL 2.1 level 2,
  • FS: a planner that uses Functional STRIPS and can handle metrics and also external calls (via '@' annotations). It uses novelty-based search, no heuristics.
  • ENHSP: This is an expressive classical, linear and non linear numeric heuristic serach planner. It reads PDDL problems and es (time stamped) sequence of actions to achieve goals starting from some description of the initial state of the system.

Temporal & Parallel

  • POPF: forwards-chaining temporal planner. Its name derives from the fact that it incorporates ideas from partial-order planning — during search, when applying an action to a state, it seeks to introduce only the ordering constraints needed to resolve threats, rather than insisting the new action occurs after all of those already in the plan.
  • Madagascar SAT-based planner: Planning using Satisfiability (SAT). The paper Madagascar: Scalable Planning with SAT explains the three different implementations of Madagascar (M, Mp, MpC).

Non-deterministic (FOND, PONDs)

Hybrid Planners

  • LAPKT programmatic interface: avoid parsing and grounding altogether by using the programmatic interface to add the fluents and actions directly.
    • C++ example here
    • Python example here.
    • Use that in your planner as in this example.
    • For example, here's how one can get the output of FD-parser and add an atom to the task.

HTN Planners

A lot of HTN resources can be found at https://hierarchical-task.net/, including links to many planners.

The 2019 workshop on HTN Planning.

  • CHIMP: CHIMP is a hierarchical hybrid planner. It combines HTN-Planning and meta-constraint reasoning and is based on the Meta-CSP Framework. Currently, it supports causal, temporal and resource knowledge as well as knowledge that is provided by an external path planner.
  • SHOP3: An implementation of SHOP in LISP.
  • PANDA: A planning system is a hierarchical planning system that is able to solve several classes of hierarchical planning problems.
  • HyperTensioN: An HTN solver in Ruby.
  • HTN-SAT (previously, T-REX): SAT-based Hierarchical Task Network (HTN) planning system. The T-REX paper.
  • totSAT: Totally-Ordered Hierarchical Planning Through SAT.
  • FLUID: A simple HTN planner based around the principles of the Builder pattern, inspired by Fluid Behaviour Tree.
  • SIADEX.
  • HPDL-Planner: HPDL-Planner is a Hierarchical Task Network planner supporting partial order compound tasks, temporal and numeric planning.

Less recent ones:

  • Pyhop: an HTN planner in Python that is simular to SHOP. HTN are specified in a Python-like language.
  • SHOP/SHOP2/JSHOP: probably the first serious HTN solvers.

HTN and video-games:

Tools

PDDL Development Support

  • PDDL extension for VSCODE: very powerful extension for Visual Studio Code IDE.\
  • Editor at planning.domains: an cloud-based editor with many features at planning.domains
    • A video explaining the editor until 1:30
  • MyPDDL: myPDDL is a highly customizable and extensible modular system, designed for supporting knowledge engineers in the process of writing, analyzing and expanding PDDL files and thereby promoting the collaboration between knowledge engineers and the use of PDDL in real-world applications.
  • To get syntaxt highlighting for PDDL in Jetbrains IDE (e.g., PyCharm), add a new file type and associate keywords under Settings / Editor / File Types:
    • Line comment is ;; and check support paired parens.
    • Keyword 1: define :requirements :types :constants :predicates :action :axiom :constants :objects :constraint :functions :goal :init :process
    • Keyword 2: domain problem :condition :effect :parameters :precondition
    • Keyword 3: and assign decrease increase not or
    • Keyword 4: #t * / <= = >= @ int number object real

Tools & Libraries

  • Unified Planning: The unified_planning library makes it easy to formulate planning problems and to invoke automated planners.
  • Fast-downward translator format: the SAS format generated by the Fast-downard Python translator.
  • Planning Domains: A collection of tools for working with planning domains.
    • Includes PDDL editor and solvers in the cloud.
  • LAPKT: Lightweight Automated Planning Toolkit. Also see Wiki. It contains a collection of planners that can be compiled and used almost on-the-spot.
  • The plan validation system (VAL): includes a PDDL parser and validator. Can be used in Visual Studio Code with its PDDL extension. Main plan validation tool.
  • The Independent Plan Validator (IVAL): a validator to complement VAL.
  • k-Star Planner: Top-k planner integrating the K* algorithm into Fast Downward.
  • Forbid-Iterative (FI): An Automated PDDL based planner that includes planners for top-k, top-quality, and diverse computational tasks.
    • Also check diverseScore that computes diversity score of a set of plans (or its subset) for a given metric.
  • AIPlanningService: A docker configuration file and code that allow fetching, building, and deploying a service with the following open-source planners:
    • Delfi1, the winner of the sequential optimal track of IPC2018
    • Cerberus, participant in satisficing and agile tracks of IPC2018
    • ForbidIterative suite of top-k, top-quality, and diverse planners
    • K* based top-k planner

Parsers & Translators

  • PDDL Parser: simple PDDL parser for classical planning without any dependencies.
  • Unquestionable PDDL: complete parser for PDDL 3.1.
  • pddl-workspace: PDDL syntax tree builder in TypeScript used for VS Code support. Its purpose is to provide language support in VS Code, so more than a parser, it is a syntax tree builder. In other words, the parser does not give access to complete PDDL object model, but works even in incomplete or syntactically incorrect documents. You could however successfully use it to extract predicates, functions, actions from the PDDL files.
  • pddl-parser: a fairly expressive Java-based parser using Antlr 4 grammar.
  • Tarski: framework for the specification, modeling and manipulation of AI planning problems, including parser for PDDL, FSTRIPS, RDDL.
  • pypddl-translator: a PDDL parser and translator in Python3 using ply library. Based on pypddl-parser.
  • adl2strips: translates input from the ADL planning language, which allows arbitrary first-order formulas in operator preconditions and the goal, to the simpler STRIPS language which restricts these to conjunctions of atoms. The tool also features two methods for compiling away conditional effects. It has been used in the 2004 IPC, and in some later editions of the IPC as well. Taken from here
  • Universal PDDL Parser: The Universal PDDL Parser is an algorithm for parsing any planning problem in PDDL format. Developed at UPF, Barcelona. Check here
  • ALD2STRIPS: Converts ADL models to STRIPS one.
  • pddl2smv: Tools to transform planning .pddl files to .smv (model checking) files.

Visualizations

Learning

  • IPC-image-data: this repository provides the data set, named IPC, for the evaluation of machine learning methods on images. It contains two collections of labeled images, presplit for training/validation/testing.
  • PDDLgym: convert PDDL to OpenAI Gym for RL.
Raw
SYNTHESIS.md

Planning & Synthesis Information, Tools, and Systems

This list is being compiled by Sebastian Sardina (ssardina@gmail.com), mostly as self-reference and as a bookmark.

If you know of something that could be listed here, please send it to me and I will add it!

Synthesis

Synthesis of finite state systems has been proven to be a valuable concept for the development of open systems that are correct by construction. It is designed for specifications comprising a set of assumptions (which the system under construction can assume to be correct) and a set of guarantees (which the system needs to fulfill).

General

  • NuGAT: A game solver on top of NuSMV model checker. Originally here.

  • TLV: Temporal Logic Verifier.

    • Good for easy prototyping and teaching, but old and not maintained. It provides a programming language to build new algorithms.

  • Reinforcement Learning framework for Temporal Goals: Reinforcement Learning framework for Temporal Goals

  • SUPREMICA: A tool for formal verification and synthesis of discrete event control functions based on discrete event models of the uncontrolled plant and specifications of the desired closed-loop behavior. Based on Supervisory Control Theory, originally formulated by Ramadge and Wonham.

LTL

  • strix: Strix is a tool for reactive LTL synthesis combining a direct translation of LTL formulas into deterministic parity automata (DPA) and an efficient, multi-threaded explicit state solver for parity games. Winner of 2020 synthesis contest. The repo can be found here
  • Lily: Lily is an LTL synthesizer written in Perl.
  • Acacia+: a tool for LTL realizability and synthesis, based on symbolic antichain techniques.
  • Unbeast: Unbeast builds upon the bounded synthesis approach.

GR(1)

  • Slugs: SmalL bUt Complete GROne Synthesizer
  • Anzu: An Perl synthesizer for GR(1). Last update 2007.

2-player Games

  • SafetySynth: SafetySynth is a tool for synthesizing controllers from safety benchmarks given in the SyntComp AIGER format.
  • pgsolver: A collection of tools for generating, manipulating and - most of all - solving parity games.

DES: Discrete Event Systems

  • Compositional Supervisory Control Benchmark: The benchmark contains six problems, three classical to supervisory control (used in the 9th International Workshop on Discrete Event Systems), and three inspired in existing literature.

Model Checkers

  • NuSMV: symbolic model checker developed in Trento, Italy.
  • Spin: Spin is an open-source software verification tool that was originally developed (starting in 1980) in the Computing Science Research Center of Bell Labs (the Unix group). It is often considered the most widely used formal verification tool.
  • UPPAAL: Uppaal is an integrated tool environment for modeling, validation and verification of real-time systems modeled as networks of timed automata, extended with data types (bounded integers, arrays, etc.).

Auxiliary/Related Tools

  • CUDD: The CUDD package is a package written in C for the manipulation of decision diagrams. It supports binary decision diagrams (BDDs), algebraic decision diagrams (ADDs), and Zero-Suppressed BDDs (ZDDs). Anothe repo for CUDD can be found here.
  • pythomata: A Python package implementing automata
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment