NDLI: Conformant planning as a case study of incremental QBF solving

Content Provider	Springer Nature Link
Author	Egly, Uwe Kronegger, Martin Pfandler, Andreas Lonsing, Florian
Copyright Year	2016
Abstract	We consider planning with uncertainty in the initial state as a case study of incremental quantified Boolean formula (QBF) solving. We report on experiments with a workflow to incrementally encode a planning instance into a sequence of QBFs. To solve this sequence of successively constructed QBFs, we use our general-purpose incremental QBF solver DepQBF. Since the generated QBFs have many clauses and variables in common, our approach avoids redundancy both in the encoding phase as well as in the solving phase. We also present experiments with incremental preprocessing techniques that are based on blocked clause elimination (QBCE). QBCE allows to eliminate certain clauses from a QBF in a satisfiability preserving way. We implemented the QBCE-based techniques in DepQBF in three variants: as preprocessing, as inprocessing (which extends preprocessing by taking into account variable assignments that were fixed by the QBF solver), and as a novel dynamic approach where QBCE is tightly integrated in the solving process. For DepQBF, experimental results show that incremental QBF solving with incremental QBCE outperforms incremental QBF solving without QBCE, which in turn outperforms nonincremental QBF solving. For the first time we report on incremental QBF solving with incremental QBCE as inprocessing. Our results are the first empirical study of incremental QBF solving in the context of planning and motivate its use in other application domains.
Ending Page	45
Page Count	25
Starting Page	21
File Format	PDF
ISSN	10122443
e-ISSN	15737470
Journal	Annals of Mathematics and Artificial Intelligence
Issue Number	1
Volume Number	80
Language	English
Publisher	Springer International Publishing
Publisher Date	2016-03-24
Publisher Place	Cham
Access Restriction	One Nation One Subscription (ONOS)
Subject Keyword	Preprocessing Problem solving (heuristics, search strategies, etc.) Logic in artificial intelligence Complex Systems Conformant planning Computer Science Artificial Intelligence (incl. Robotics) Mathematics Incremental solving Theorem proving (deduction, resolution, etc.) Quantified Boolean formulas (QBFs) Blocked clause elimination
Content Type	Text
Resource Type	Article
Subject	Applied Mathematics Artificial Intelligence

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Conformant planning as a case study of incremental QBF solving

Solving quantified verification conditions using satisfiability modulo theories

Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search

Dialogues for proof search

Set-structured and cost-sharing heuristics for classical planning

Bagging strategies for learning planning policies

Conformant Planning as a Case Study of Incremental QBF Solving

Quantifier Reordering for QBF

Inductive proof search modulo

Conformant planning as a case study of incremental QBF solving

Similar Documents

Conformant planning as a case study of incremental QBF solving

Solving quantified verification conditions using satisfiability modulo theories

Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search

Dialogues for proof search

Set-structured and cost-sharing heuristics for classical planning

Bagging strategies for learning planning policies

Conformant Planning as a Case Study of Incremental QBF Solving

Quantifier Reordering for QBF

Inductive proof search modulo

Conformant planning as a case study of incremental QBF solving