首页/论文/2109.08293

arXiv 2109.082932021-09-17cs.AIcs.PL

基于SAT编码可达性约束的图综合问题在Picat中的建模与求解

Modeling and Solving Graph Synthesis Problems Using SAT-Encoded Reachability Constraints in Picat

CUNY Brooklyn College & Graduate Center（纽约市立大学布鲁克林学院及研究生中心）

Neng-Fa Zhou

备注：: In Proceedings ICLP 2021, arXiv:2109.07914
发表信息：: EPTCS 345, 2021, pp. 165-178
DOI：: 10.4204/EPTCS.345.30

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

许多约束满足问题涉及合成满足某些可达性约束的子图。本文介绍了四个问题，从最近的LP/CP编程比赛中选择的Picat程序。这些程序展示了Picat语言的建模能力和具有有效编码的尖端SAT求解器的求解效率。

英文摘要：

Many constraint satisfaction problems involve synthesizing subgraphs that satisfy certain reachability constraints. This paper presents programs in Picat for four problems selected from the recent LP/CP programming competitions. The programs demonstrate the modeling capabilities of the Picat language and the solving efficiency of the cutting-edge SAT solvers empowered with effective encodings.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

用顶点消去法对无环性和可达性的命题编码

Propositional Encodings of Acyclicity and Reachability by using Vertex Elimination

Aalto University（阿尔托大学）

我们介绍了新的方法编码的无环性和s-t-可达性约束的命题公式与底层有向图。它们基于顶点消除图，这使得它们适用于底层图稀疏的情况。与求解器与ad hoc约束传播的非循环性和可达性约束，如GraphSAT，我们的方法编码这些约束作为标准的命题子句，使它们直接适用于任何SAT求解器。一项实证研究表明，我们的方法与一个有效的SAT求解器可以优于这些约束的早期编码以及GraphSAT，特别是当底层图形稀疏。

2021-05-27cs.AI

POMDPs中小策略几乎必然可达的符号SAT算法

A Symbolic SAT-based Algorithm for Almost-sure Reachability with Small Strategies in POMDPs

IST Austria（奥地利科学技术研究所）

POMDPs是概率规划问题的标准模型，其中代理与不确定环境交互。我们研究的问题几乎肯定的可达性，在给定的一组目标状态，问题是要决定是否有一个政策，以确保达到目标集的概率为1（几乎肯定）。虽然一般来说这个问题是EXPTIME完全的，但在许多实际情况下，具有少量内存的策略就足够了。此外，现有的解决方案的问题是明确的，这首先需要明确地构造一个指数约简的信念支持MDP。在这项工作中，我们首先研究的存在性观察平稳的策略，这是NP完全的，然后小记忆策略。我们提出了一个符号算法的有效编码SAT和使用SAT求解器的问题。我们报告的实验结果表明，我们的符号（SAT为基础的）方法的可扩展性。

2015-11-26cs.AI

基于可满足性模理论与可达性分析的交通规则合规轨迹修复

Traffic-Rule-Compliant Trajectory Repair via Satisfiability Modulo Theories and Reachability Analysis

针对自动驾驶轨迹违反交通规则需从头重规划耗时的问题，提出结合可满足性模理论与可达性分析的轨迹修复方法，实验验证其能高效可靠修复违规轨迹，使车辆实时恢复合法安全运行。

2025-09-10cs.AIcs.RO

利用SMT求解器求解混合网络可达性问题

Instrumenting an SMT Solver to Solve Hybrid Network Reachability Problems

SIFT, LLC.（SIFT有限责任公司）；IST Austria（奥地利科学技术学院）；University of Freiburg（弗莱堡大学）

PDDL+规划的语义植根于混合自动机（HA），最近的工作表明，它可以建模为一个网络的HA。解决复杂的非线性PDDL+规划的HA需要空间和时间效率的推理。不幸的是，现有的求解器要么不解决非线性动力学，要么不支持自动机网络。我们提出了一种新的算法，称为HNSolve，它指导dReal可满足性模理论（SMT）求解器的变量选择，同时推理网络编码的非线性PDDL+规划作为HA。HNSolve通过解决HA网络的离散抽象与dReal紧密集成。HNSolve在HA网络上查找忽略连续变量但尊重模式跳转和同步标签的复合运行。HNSolve可允许地检测离散抽象中的死胡同，并发布冲突子句来修剪SMT求解器的搜索。我们评估我们的HNSolve算法的好处PDDL+基准问题，并证明其性能相对于以前的工作。

2016-09-13cs.AI

论网格图可达性与益智游戏

On Grid Graph Reachability and Puzzle Games

Universitat de Girona（赫罗纳大学）；Universitat de Vic - Universitat Central de Catalunya（维克大学-加泰罗尼亚中央大学）；University of St Andrews（圣安德鲁斯大学）

针对益智游戏中以物体操作数衡量关卡难度的问题，本文研究CP与SAT求解方法，提出新的可达性编码，实验证明其适配规划即SAT范式的益智问题求解，尤其适用于多操作并行场景。

2023-10-02cs.AI

具有可达性目标的POMDP传感器综合

Sensor Synthesis for POMDPs with Reachability Objectives

IST Austria（奥地利科学技术研究所）；University of Texas at Austin（德克萨斯大学奥斯汀分校）

部分可观测马尔可夫决策过程（POMDPs）被广泛应用于概率规划问题中，其中智能体与环境交互使用噪声和不精确的传感器。我们研究的设置中，传感器只有部分定义和目标是合成“最弱”的额外传感器，这样，在由此产生的POMDP，有一个小内存的代理，几乎肯定（概率~1）满足可达性目标的政策。我们证明了该问题是NP完全的，并通过将问题编码成SAT实例，给出了一个符号算法。我们说明了一个简单的例子上的策略的内存量和额外的传感器的数量之间的权衡。我们已经实现了我们的方法，并考虑三个经典的POMDP的例子，从文献中，并表明，在所有的例子中，传感器的数量可以显着减少（与文献中现有的解决方案相比），而不会增加政策的复杂性。

2017-09-29cs.AI

更多相关论文收起更多论文

可达性约束的强化学习

Reachability Constrained Reinforcement Learning

Tsinghua University（清华大学）；Harvard University（哈佛大学）；Shanghai Qizhi Institute（上海期智研究院）

约束强化学习（CRL）最近得到了极大的兴趣，因为安全约束的满足是现实世界中的问题的关键。然而，现有的CRL方法约束贴现累积成本一般缺乏严格的定义和安全性的保证。相反，在安全控制研究中，安全被定义为持续满足某些状态约束。这种持久安全性只在状态空间的一个子集上是可能的，称为可行集，其中对于给定的环境存在最优的最大可行集。最近的研究将可行集纳入CRL与基于能量的方法，如控制障碍函数（CBF），安全指数（SI），并利用可行集的先验保守估计，这损害了学习策略的性能。针对这一问题，本文提出了可达性CRL（RCRL）方法，通过可达性分析建立新的自洽条件，刻画可行集。可行集由安全价值函数表示，该函数在CRL中用作约束。我们使用多时间尺度随机逼近理论证明了该算法收敛到局部最优，在那里可以保证最大的可行集。在不同基准上的实验结果验证了RCRL的学习可行集，策略性能和约束满足，与CRL和安全控制基线相比。

2022-06-07cs.AIcs.LGcs.RO

逻辑程序的结构难性特征：是什么使得树宽的循环和可达性难？

Characterizing Structural Hardness of Logic Programs: What makes Cycles and Reachability Hard for Treewidth?

答案集编程（ASP）是一个问题建模和解决框架的几个问题，在KR与日益增长的工业应用。ASP也是近年来研究计算复杂性和深入理解计算难度及其来源的一个热点。这些研究导致了富有成效的表征方面的复杂性类，细粒度的见解形式的二分法风格的结果，以及详细的参数化的复杂性景观。最近，这导致了一个新的结果，建立的措施树宽，它捕获的程序的结构密度，评估的知名类正常的程序预计将稍微困难比决定可满足性（SAT）。然而，目前还不清楚如何利用ASP的这种结构性力量。本文论述了一种新的减少SAT到正常的ASP，超越了众所周知的编码：我们明确利用ASP的结构功率，从而我们次线性地减少树的宽度，这可能无法显着改善。然后，与现有的结果相比，这通过建立依赖图的周期长度（SCC大小）对树宽的所需函数依赖来以细粒度的方式表征硬度。

2023-01-18cs.AIcs.DMcs.LO

安全可达POMDPs的有界策略综合

Bounded Policy Synthesis for POMDPs with Safe-Reachability Objectives

Rice University（莱斯大学）

在不确定性下规划鲁棒执行是构建自主机器人的基本挑战。部分可观测马尔可夫决策过程（POMDP）为许多应用中的不确定性建模提供了一个标准框架。在这项工作中，我们研究POMDPs的安全可达性的目标，这需要一个概率高于一定的阈值，最终达到一个目标状态，同时保持访问不安全状态的概率低于一定的阈值。这POMDP制定是不同于传统的POMDP模型的最优性目标，我们表明，在某些情况下，安全可达性目标的POMDP可以提供更好的保证安全性和可达性比现有的POMDP模型通过一个例子。POMDP的一个关键算法问题是策略综合，这需要在一个巨大的信念空间（概率分布）上进行推理。为了解决这一挑战，我们引入了一个目标约束的信念空间的概念，其中只包含信念可达到的初始信念下所需的执行，可以实现给定的安全可达性目标。我们的方法competently表示这个空间在一个有界的地平线上使用符号约束，并采用增量可满足性模理论（SMT）求解器，有效地搜索一个有效的policy.We评估我们的方法使用的案例研究，涉及部分可观察的机器人领域与不确定的障碍。结果表明，我们的方法可以合成政策在大的信念空间与少量的SMT求解器调用集中在目标约束的信念空间。

2018-05-09cs.AIcs.RO

通过自我视觉上的近似可达性实现安全的自主赛车

Safe Autonomous Racing via Approximate Reachability on Ego-vision

Carnegie Mellon University（卡内基梅隆大学）；Bosch Research Pittsburgh（博世研究院匹兹堡）；University of California, San Diego（加州大学圣地亚哥分校）

赛车要求每辆车都能在其物理极限下行驶，任何安全违规都可能导致灾难性的故障。在这项工作中，我们研究了安全的强化学习（RL）的自主赛车的问题，使用车辆的自我摄像头的看法和速度作为输入。鉴于任务的性质，自主智能体需要能够1）识别和避免复杂车辆动力学下的不安全场景，2）在快速变化的环境中做出亚秒级的决策。为了满足这些标准，我们建议将汉密尔顿-雅可比（HJ）可达性理论，一般非线性系统的安全验证方法，到约束马尔可夫决策过程（CMDP）的框架。HJ可达性不仅提供了一种了解安全性的控制理论方法，而且还实现了低延迟的安全验证。虽然HJ的可达性传统上是不可扩展的高维系统，我们证明了神经近似，HJ的安全值可以直接学习的视觉上下文-最高维的问题，通过该方法研究，到目前为止。我们在几个基准任务上评估了我们的方法，包括安全健身房和学习比赛（L2 R），这是最近发布的高保真自动驾驶赛车环境。与安全健身房中的其他约束RL基线相比，我们的方法具有更少的约束违反，并在L2 R基准测试任务上实现了新的最先进的结果。我们在以下匿名论文网站上提供了代理行为的额外可视化：https://sites.google.com/view/safeautonomousracing/home

2021-11-30cs.AIcs.LGcs.RO

基于反例引导的非精化抽象的多Agent路径搜索

Counterexample Guided Abstraction Refinement with Non-Refined Abstractions for Multi-Agent Path Finding

Czech Technical University in Prague（捷克布拉格技术大学）

反例引导的抽象精化（CEGAR）是一种强大的符号技术，用于各种任务，如模型检验和可达性分析。最近，CEGAR结合布尔可满足性（SAT）已被应用于多智能体路径查找（MAPF），任务是导航代理从他们的开始位置到给定的个人目标位置，使代理不相互碰撞的问题。最近的CEGAR方法使用了MAPF问题的初始抽象，其中代理之间的冲突被忽略，并在随后的抽象细化中被消除。在这项工作中，我们提出了一种新的CEGAR式求解器的MAPF SAT的基础上，其中一些抽象故意留下非精制。这增加了对从底层SAT求解器获得的答案进行后处理的必要性，因为这些答案与正确的MAPF解决方案略有不同。然而，非细化产生的数量级较小的SAT编码比以前的方法，并加快了整体求解过程，使基于SAT的求解器的MAPF竞争力再次在相关的基准。

2023-01-20cs.AI