Chapter 19. Planning and SAT

2021 ◽  
Author(s):  
Jussi Rintanen
Keyword(s):  
Artificial Intelligence ◽  
Model Checking ◽  
Bounded Model Checking ◽  
Planning Problem ◽  
Ai Planning ◽  
Transition Systems ◽  
Computer Aided ◽  
Sat Solver ◽  
Main Ideas ◽  
Planning Problems

The planning problem in Artificial Intelligence was the first application of SAT to reasoning about transition systems and a direct precursor to the use of SAT in a number of other applications, including bounded model-checking in computer-aided verification. This chapter presents the main ideas about encoding goal reachability problems as a SAT problem, including parallel plans and different forms of constraints for speeding up SAT solving, as well as algorithms for solving the AI planning problem with a SAT solver. Finally, more general planning problems that require the use of QBF or other generalizations of SAT are discussed.

A SAT-Based Planning Approach for Finding Logical Attacks on Cryptographic Protocols

2020 ◽  
Vol 14 (4) ◽  
pp. 1-21
Author(s):  
Noureddine Aribi ◽  
Yahia Lebbah
Keyword(s):  
Model Checking ◽  
State Of The Art ◽  
Cryptographic Protocols ◽  
Protocol Verification ◽  
Planning Problem ◽  
Multiparty Communication ◽  
Planning Approach ◽  
Security Properties ◽  
Sat Solver ◽  
Security Property

Cryptographic protocols form the backbone of digital society. They are concurrent multiparty communication protocols that use cryptography to achieve security goals such as confidentiality, authenticity, integrity, etc., in the presence of adversaries. Unfortunately, protocol verification still represents a critical task and a major cost to engineer attack-free security protocols. Model checking and SAT-based techniques proved quite effective in this context. This article proposes an efficient automatic model checking approach that exemplifies a security property violation. In this approach, a protocol verification is abstracted as a compact planning problem, which is efficiently solved by a state-of-the-art SAT solver. The experiments performed on some real-world cryptographic protocols succeeded in detecting new logical attacks, violating some security properties. Those attacks encompass both “type flaw” and “replay” attacks, which are difficult to tackle with the existing planning-based approaches.

scholarly journals Reduce Artificial Intelligence Planning Effort by using Map-Reduce Paradigm

2021 ◽  
Vol 10 (7) ◽  
pp. 24-32
Author(s):  
Mohamed Elkawkagy* ◽  
Elbeh Heba
Keyword(s):  
Artificial Intelligence ◽  
Search Space ◽  
Processing Technique ◽  
Substantial Improvement ◽  
Domain Model ◽  
Map Reduce ◽  
Planning Problem ◽  
Ai Planning ◽  
Hierarchical Planning ◽  
Artificial Intelligence Planning

While several approaches have been developed to enhance the efficiency of hierarchical Artificial Intelligence planning (AI-planning), complex problems in AI-planning are challenging to overcome. To find a solution plan, the hierarchical planner produces a huge search space that may be infinite. A planner whose small search space is likely to be more efficient than a planner produces a large search space. In this paper, we will present a new approach to integrating hierarchical AI-planning with the map-reduce paradigm. In the mapping part, we will apply the proposed clustering technique to divide the hierarchical planning problem into smaller problems, so-called sub-problems. A pre-processing technique is conducted for each sub-problem to reduce a declarative hierarchical planning domain model and then find an individual solution for each so-called sub-problem sub-plan. In the reduction part, the conflict between sub-plans is resolved to provide a general solution plan to the given hierarchical AI-planning problem. Preprocessing phase helps the planner cut off the hierarchical planning search space for each sub-problem by removing the compulsory literal elements that help the hierarchical planner seek a solution. The proposed approach has been fully implemented successfully, and some experimental results findings will be provided as proof of our approach's substantial improvement inefficiency.

scholarly journals Card-Based Cryptography Meets Formal Verification

2021 ◽  
Author(s):  
Alexander Koch ◽  
Michael Schrempp ◽  
Michael Kirsten
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
State Space ◽  
Lower Bounds ◽  
Bounded Model Checking ◽  
Minimal Length ◽  
State Spaces ◽  
Bounded State ◽  
Sat Solver ◽  
General Translation

AbstractCard-based cryptography provides simple and practicable protocols for performing secure multi-party computation with just a deck of cards. For the sake of simplicity, this is often done using cards with only two symbols, e.g., $$\clubsuit $$ ♣ and $$\heartsuit $$ ♡ . Within this paper, we also target the setting where all cards carry distinct symbols, catering for use-cases with commonly available standard decks and a weaker indistinguishability assumption. As of yet, the literature provides for only three protocols and no proofs for non-trivial lower bounds on the number of cards. As such complex proofs (handling very large combinatorial state spaces) tend to be involved and error-prone, we propose using formal verification for finding protocols and proving lower bounds. In this paper, we employ the technique of software bounded model checking (SBMC), which reduces the problem to a bounded state space, which is automatically searched exhaustively using a SAT solver as a backend. Our contribution is threefold: (a) we identify two protocols for converting between different bit encodings with overlapping bases, and then show them to be card-minimal. This completes the picture of tight lower bounds on the number of cards with respect to runtime behavior and shuffle properties of conversion protocols. For computing AND, we show that there is no protocol with finite runtime using four cards with distinguishable symbols and fixed output encoding, and give a four-card protocol with an expected finite runtime using only random cuts. (b) We provide a general translation of proofs for lower bounds to a bounded model checking framework for automatically finding card- and run-minimal (i.e., the protocol has a run of minimal length) protocols and to give additional confidence in lower bounds. We apply this to validate our method and, as an example, confirm our new AND protocol to have its shortest run for protocols using this number of cards. (c) We extend our method to also handle the case of decks on symbols $$\clubsuit $$ ♣ and $$\heartsuit $$ ♡ , where we show run-minimality for two AND protocols from the literature.

scholarly journals Tuning Parallel SAT Solvers

10.29007/z3g2 ◽  
2019 ◽  
Author(s):  
Thorsten Ehlers ◽  
Dirk Nowotka
Keyword(s):  
Model Checking ◽  
Database Management ◽  
Bounded Model Checking ◽  
Experimental Results ◽  
Massively Parallel ◽  
Sat Solving ◽  
Sat Solvers ◽  
Sat Solver ◽  
The Impact

In this paper we present new implementation details and benchmarking results for our parallel portfolio solver TopoSAT2. In particular, we discuss ideas and implementation details for the exchange of learned clauses in a massively-parallel SAT solver which is designed to run more that 1, 000 solver threads in parallel. Furthermore, we go back to the roots of portfolio SAT solving, and discuss the impact of diversifying the solver by using different restart- , branching- and clause database management heuristics. We show that these techniques can be used to tune the solver towards different problems. However, in a case study on formulas derived from Bounded Model Checking problems we see the best performance when using a rather simple clause exchange strategy. We show details of these tests and discuss possible explanations for this phenomenon.As computing times on massively-parallel clusters are expensive, we consider it especially interesting to share these kind of experimental results.

scholarly journals Property Directed Reachability for Automated Planning

2014 ◽  
Vol 50 ◽  
pp. 265-319 ◽  
Author(s):  
M. Suda
Keyword(s):  
Model Checking ◽  
State Of The Art ◽  
Automated Planning ◽  
The State ◽  
Experimental Comparison ◽  
Specific Procedure ◽  
Transition Systems ◽  
Planning Algorithm ◽  
Sat Solver ◽  
Recent Method

Property Directed Reachability (PDR) is a very promising recent method for deciding reachability in symbolically represented transition systems. While originally conceived as a model checking algorithm for hardware circuits, it has already been successfully applied in several other areas. This paper is the first investigation of PDR from the perspective of automated planning. Similarly to the planning as satisfiability paradigm, PDR draws its strength from internally employing an efficient SAT-solver. We show that most standard encoding schemes of planning into SAT can be directly used to turn PDR into a planning algorithm. As a non-obvious alternative, we propose to replace the SAT-solver inside PDR by a planning-specific procedure implementing the same interface. This SAT-solver free variant is not only more efficient, but offers additional insights and opportunities for further improvements. An experimental comparison to the state of the art planners finds it highly competitive, solving most problems on several domains.

The classical AI planning problems in the mirror of Horn linear logic: semantics, expressibility, complexity

2001 ◽  
Vol 11 (6) ◽  
pp. 689-716 ◽  
Author(s):  
MAX KANOVICH ◽  
JACQUELINE VAUZEILLES
Keyword(s):  
Linear Logic ◽  
Planning Problem ◽  
Ai Planning ◽  
Logical System ◽  
Robot System ◽  
Descriptive Complexity ◽  
Robot Systems ◽  
Finite Set ◽  
Planning Problems ◽  
Finite Domains

We introduce Horn linear logic as a comprehensive logical system capable of handling the typical AI problem of making a plan of the actions to be performed by a robot so that he could get into a set of final situations, if he started with a certain initial situation. Contrary to undecidability of propositional Horn linear logic, the planning problem is proved to be decidable for a reasonably wide class of natural robot systems.The planning problem is proved to be EXPTIME-complete for the robot systems that allow actions with non-deterministic effects. Fixing a finite signature, that is a finite set of predicates and their finite domains, we get a polynomial time procedure of making plans for the robot system over this signature.The planning complexity is reduced to PSPACE for the robot systems with only pure deterministic actions.As honest numerical parameters in our algorithms we invoke the length of description of a planning task ‘from W to Z˜’ and the Kolmogorov descriptive complexity of AxT, a set of possible actions.

scholarly journals Contrastive Explanations of Plans through Model Restrictions

2021 ◽  
Vol 72 ◽  
pp. 533-612
Author(s):  
Benjamin Krarup ◽  
Senka Krivic ◽  
Daniele Magazzeni ◽  
Derek Long ◽  
Michael Cashmore ◽  
...  
Keyword(s):  
Restricted Problem ◽  
Original Problem ◽  
User Study ◽  
Planning Problem ◽  
Ai Planning ◽  
Exploration Process ◽  
Iterative Model ◽  
Contrastive Explanation ◽  
Original Plan ◽  
Planning Problems

In automated planning, the need for explanations arises when there is a mismatch between a proposed plan and the user’s expectation. We frame Explainable AI Planning as an iterative plan exploration process, in which the user asks a succession of contrastive questions that lead to the generation and solution of hypothetical planning problems that are restrictions of the original problem. The object of the exploration is for the user to understand the constraints that govern the original plan and, ultimately, to arrive at a satisfactory plan. We present the results of a user study that demonstrates that when users ask questions about plans, those questions are usually contrastive, i.e. “why A rather than B?”. We use the data from this study to construct a taxonomy of user questions that often arise during plan exploration. Our approach to iterative plan exploration is a process of successive model restriction. Each contrastive user question imposes a set of constraints on the planning problem, leading to the construction of a new hypothetical planning problem as a restriction of the original. Solving this restricted problem results in a plan that can be compared with the original plan, admitting a contrastive explanation. We formally define model-based compilations in PDDL2.1 for each type of constraint derived from a contrastive user question in the taxonomy, and empirically evaluate the compilations in terms of computational complexity. The compilations were implemented as part of an explanation framework supporting iterative model restriction. We demonstrate its benefits in a second user study.

scholarly journals Bounded model checking of Time Petri Nets using SAT solver

2015 ◽  
Vol 12 (2) ◽  
pp. 20141112-20141112 ◽  
Author(s):  
Tomoyuki Yokogawa ◽  
Masafumi Kondo ◽  
Hisashi Miyazaki ◽  
Sousuke Amasaki ◽  
Yoichiro Sato ◽  
...  
Keyword(s):  
Model Checking ◽  
Petri Nets ◽  
Bounded Model Checking ◽  
Time Petri Nets ◽  
Sat Solver

scholarly journals Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse

10.29007/2s1q ◽  
2018 ◽  
Author(s):  
Chuan Jiang ◽  
Gianfranco Ciardo
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Experimental Results ◽  
Propositional Satisfiability ◽  
Propositional Formula ◽  
Branching Time ◽  
Simple Modification ◽  
Complementary Technique ◽  
Computation Tree ◽  
Sat Solver

A complementary technique to decision-diagram-based model checking is SAT-based bounded model checking (BMC), which reduces the model checking problem to a propositional satisfiability problem so that the corresponding formula is satisfiable iff a counterexample or witness exists. Due to the branching time nature of computation tree logic (CTL), BMC for the universal fragment of CTL (ACTL) considers a counterexample in a bounded model as a set of bounded paths. Since the existential fragment of CTL (ECTL) is dual to ACTL, and ACTL formulas are often negated to obtain ECTL ones in practice, we focus on BMC for ECTL and propose an improved translation that generates a possibly smaller propositional formula by reducing the number of bounded paths to be considered in a witness. Experimental results show that the formulas generated by our approach are often easier for a SAT solver to answer. In addition, we propose a simple modification to the translation so that it is also defined for models with deadlock states.

Sign in / Sign up

Export Citation Format

Share Document