Planning as Quantified Boolean Formulae

Research output: ThesisDoctoral Thesis

Abstract

This work explores the idea of classical Planning as Quantified Boolean Formulae. Planning as Satisfiability (SAT) is a popular approach to Planning and has been explored in detail producing many compact and efficient encodings, Planning-specific solver implementations and innovative new constraints. However, Planning as Quantified Boolean Formulae (QBF) has been relegated to conformant Planning approaches, with the exception of one encoding that has not yet been investigated in detail. QBF is a promising setting for Planning given that the problems have the same complexity. This work introduces two approaches for translating bounded propositional reachability problems into QBF. Both exploit the expressivity of the binarytree structure of the QBF problem to produce encodings that are as small as logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. The first approach builds on the iterative squaring formu lation of Rintanen; the intuition behind the idea is to recursively fold the plan around the midpoint, reducing the number of time-steps that need to be described from n to log2n. The second approach exploits domain-level lifting to achieve significant improvements in efficiency. Experimentation was performed to compare our formulation of the first approach with the previous formulation, and to compare both approaches with comparative and state-of-the-art SAT approaches. Results presented in this work show that our formulation of the first approach is an improvement over the previous, and that both approaches produce encodings that are indeed much smaller than corresponding SAT encodings, in both terms of encoding size and memory used during solving. Evidence is also provided to show that the first approach is feasible, if not yet competitive with the state-of-the-art, and that the second approach produces superior encodings to the SAT encodings when the domain is suited to domain-level lifting.
LanguageEnglish
QualificationPhD
Awarding Institution
  • University Of Strathclyde
Supervisors/Advisors
  • Fox, Maria, Supervisor
  • Long, Derek, Supervisor
Publisher
Publication statusPublished - 2013

Fingerprint

Planning
Data storage equipment

Keywords

  • planning
  • Quantified Boolean Formulae
  • Satisfiability (SAT)

Cite this

Cashmore, M. (2013). Planning as Quantified Boolean Formulae. University of Strathclyde.
Cashmore, Michael. / Planning as Quantified Boolean Formulae. University of Strathclyde, 2013. 114 p.
@phdthesis{be4a32da502b4fafb896c275290b998a,
title = "Planning as Quantified Boolean Formulae",
abstract = "This work explores the idea of classical Planning as Quantified Boolean Formulae. Planning as Satisfiability (SAT) is a popular approach to Planning and has been explored in detail producing many compact and efficient encodings, Planning-specific solver implementations and innovative new constraints. However, Planning as Quantified Boolean Formulae (QBF) has been relegated to conformant Planning approaches, with the exception of one encoding that has not yet been investigated in detail. QBF is a promising setting for Planning given that the problems have the same complexity. This work introduces two approaches for translating bounded propositional reachability problems into QBF. Both exploit the expressivity of the binarytree structure of the QBF problem to produce encodings that are as small as logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. The first approach builds on the iterative squaring formu lation of Rintanen; the intuition behind the idea is to recursively fold the plan around the midpoint, reducing the number of time-steps that need to be described from n to log2n. The second approach exploits domain-level lifting to achieve significant improvements in efficiency. Experimentation was performed to compare our formulation of the first approach with the previous formulation, and to compare both approaches with comparative and state-of-the-art SAT approaches. Results presented in this work show that our formulation of the first approach is an improvement over the previous, and that both approaches produce encodings that are indeed much smaller than corresponding SAT encodings, in both terms of encoding size and memory used during solving. Evidence is also provided to show that the first approach is feasible, if not yet competitive with the state-of-the-art, and that the second approach produces superior encodings to the SAT encodings when the domain is suited to domain-level lifting.",
keywords = "planning, Quantified Boolean Formulae, Satisfiability (SAT)",
author = "Michael Cashmore",
year = "2013",
language = "English",
publisher = "University of Strathclyde",
school = "University Of Strathclyde",

}

Cashmore, M 2013, 'Planning as Quantified Boolean Formulae', PhD, University Of Strathclyde.

Planning as Quantified Boolean Formulae. / Cashmore, Michael.

University of Strathclyde, 2013. 114 p.

Research output: ThesisDoctoral Thesis

TY - THES

T1 - Planning as Quantified Boolean Formulae

AU - Cashmore, Michael

PY - 2013

Y1 - 2013

N2 - This work explores the idea of classical Planning as Quantified Boolean Formulae. Planning as Satisfiability (SAT) is a popular approach to Planning and has been explored in detail producing many compact and efficient encodings, Planning-specific solver implementations and innovative new constraints. However, Planning as Quantified Boolean Formulae (QBF) has been relegated to conformant Planning approaches, with the exception of one encoding that has not yet been investigated in detail. QBF is a promising setting for Planning given that the problems have the same complexity. This work introduces two approaches for translating bounded propositional reachability problems into QBF. Both exploit the expressivity of the binarytree structure of the QBF problem to produce encodings that are as small as logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. The first approach builds on the iterative squaring formu lation of Rintanen; the intuition behind the idea is to recursively fold the plan around the midpoint, reducing the number of time-steps that need to be described from n to log2n. The second approach exploits domain-level lifting to achieve significant improvements in efficiency. Experimentation was performed to compare our formulation of the first approach with the previous formulation, and to compare both approaches with comparative and state-of-the-art SAT approaches. Results presented in this work show that our formulation of the first approach is an improvement over the previous, and that both approaches produce encodings that are indeed much smaller than corresponding SAT encodings, in both terms of encoding size and memory used during solving. Evidence is also provided to show that the first approach is feasible, if not yet competitive with the state-of-the-art, and that the second approach produces superior encodings to the SAT encodings when the domain is suited to domain-level lifting.

AB - This work explores the idea of classical Planning as Quantified Boolean Formulae. Planning as Satisfiability (SAT) is a popular approach to Planning and has been explored in detail producing many compact and efficient encodings, Planning-specific solver implementations and innovative new constraints. However, Planning as Quantified Boolean Formulae (QBF) has been relegated to conformant Planning approaches, with the exception of one encoding that has not yet been investigated in detail. QBF is a promising setting for Planning given that the problems have the same complexity. This work introduces two approaches for translating bounded propositional reachability problems into QBF. Both exploit the expressivity of the binarytree structure of the QBF problem to produce encodings that are as small as logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. The first approach builds on the iterative squaring formu lation of Rintanen; the intuition behind the idea is to recursively fold the plan around the midpoint, reducing the number of time-steps that need to be described from n to log2n. The second approach exploits domain-level lifting to achieve significant improvements in efficiency. Experimentation was performed to compare our formulation of the first approach with the previous formulation, and to compare both approaches with comparative and state-of-the-art SAT approaches. Results presented in this work show that our formulation of the first approach is an improvement over the previous, and that both approaches produce encodings that are indeed much smaller than corresponding SAT encodings, in both terms of encoding size and memory used during solving. Evidence is also provided to show that the first approach is feasible, if not yet competitive with the state-of-the-art, and that the second approach produces superior encodings to the SAT encodings when the domain is suited to domain-level lifting.

KW - planning

KW - Quantified Boolean Formulae

KW - Satisfiability (SAT)

M3 - Doctoral Thesis

PB - University of Strathclyde

ER -

Cashmore M. Planning as Quantified Boolean Formulae. University of Strathclyde, 2013. 114 p.