This paper introduces the 2019 version of \us{}, a novel Constraint Programming framework for floating point verification problems expressed with the SMT language of SMTLIB. SMT solvers decompose their task by delegating to specific theories (e.g., floating point, bit vectors, arrays, ...) the task to reason about combinatorial or otherwise complex constraints for which the SAT encoding would be cumbersome or ineffective. This decomposition and encoding processes lead to the obfuscation of the high-level constraints and a loss of information on the structure of the combinatorial model. In \us{}, constraints over the floats are first class objects, and the purpose is to expose and exploit structures of floating point domains to enhance the search process. A symbolic phase rewrites each SMTLIB instance to elementary constraints, and eliminates auxiliary variables whose presence is counterproductive. A diversification technique within the search steers it away from costly enumerations in unproductive areas of the search space. The empirical evaluation demonstrates that the 2019 version of \us{} is competitive on computationally challenging floating point benchmarks that induce significant search efforts even for other CP solvers. It highlights that the ability to harness both inference and search is critical. Indeed, it yields a factor 3 improvement over Colibri and is up to 10 times faster than SMT solvers. The evaluation was conducted over 214 benchmarks (The Griggio suite) which is a standard within SMTLIB.
Lazy Modeling of Variants of Token Swapping Problem and Multi-agent Path Finding through Combination of Satisfiability Modulo Theories and Conflict-based Search
Continuous Optimization for Satisfiability Modulo Theories on Linear Real Arithmetic
Department of Electrical and Computer Engineering, National University of Singapore, Singapore（电子与计算机工程系，新加坡国立大学）；School of Computing and Data Science, The University of Hong Kong, Hong Kong, China（计算与数据科学学院，香港大学）
A Comparative Study of SMT and MILP for the Nurse Rostering Problem
Division of Systems and Control, Department of Electrical Engineering, Chalmers University of Technology（系统与控制系，电气工程系，查尔姆斯理工大学）；Research and Technology Development, Group Trucks Operations, Volvo AB（研发与技术发展，卡车运营组，沃尔沃公司）
Exploiting Binary Floating-Point Representations for Constraint Propagation: The Complete Unabridged Version
BUGSENG srl（BUGSENG有限责任公司）；University of Parma（帕尔马大学）；INRIA Rennes Bretagne Atlantique（法国国家信息与自动化研究所雷恩-布列塔尼-大西洋研究中心）；University of Pisa（比萨大学）；SIMULA Research Laboratory（SIMULA研究所）
College of Computer Science and Technology, Jilin University（吉林大学计算机科学与技术学院）；Key Laboratory of Symbolic Computation and Knowledge Engineering Ministry of Education, Jilin University（吉林大学符号计算与知识工程教育部重点实验室）；School of Software, Beihang University（北航软件学院）
Hybrid Probabilistic Inference with Logical Constraints: Tractability and Message Passing
University of California, LA（加利福尼亚大学洛杉矶分校）；AMSS（数学与系统科学研究院）；Chinese Academy of Sciences（中国科学院）；DISI（信息工程与计算机科学系）；University of Trento（特伦托大学）
加权模型集成（Weighted Model Integration，简称WMM）是一个非常吸引人的概率推理框架：它允许通过可满足性模理论（Satisfiability Modulo Theories，简称SMT）的语言来表达真实世界混合场景的复杂依赖关系，其中变量在本质上是异构的（包括连续和离散）;以及计算具有任意复杂逻辑约束的概率查询。最近的工作表明，在某些假设下，可简化的模型集成（MI）问题，从而有效地允许混合概率推理的体积计算。在本文中，我们介绍了一种新的制定MI通过消息传递计划，允许有效地计算的边际密度和统计矩的所有变量在线性时间。因此，当任意丰富的MI查询符合问题结构时，我们能够摊销推理，这里表示为与SMT公式相关联的原始图。此外，我们从理论上跟踪的易处理边界的确切MI。事实上，我们证明，在原始图的结构要求，使我们的MI算法易于处理-边界的直径和树宽-边界不仅是足够的，但通过MI易于推理的必要条件。
Constraint Answer Set Programming: Integrational and Translational (or SMT-based) Approaches
University of Nebraska Omaha（内布拉斯加大学奥马哈分校）
约束回答集编程（英语：Constraint answer set programming，缩写为CASP）是一种自动推理的混合方法，它综合了回答集编程、约束处理和可满足性模理论等不同研究领域的进展。约束答案集编程展示了有希望的结果，包括开发了大量的求解器：acsolver，clingcon，ezcsp，idp，inca，dingo，mingo，aspmt，clingo[l，dl]和ezsmt。它为声明式编程应用程序（如解决复杂的训练调度问题）开辟了新的视野。系统的设计，以找到解决方案，约束答案集程序可以分组，根据他们的建设，我们称之为，整合或翻译的方法。本文的重点是一个概述的关键成分的设计约束答案集求解器之间的区别和平行的集成和翻译的方法。本文还提供了一个一瞥，其用户开发的程序，利用CASP编码的旅行推销员问题的说明。此外，我们把CASP技术在地图上的自动推理同行之间，以及讨论未来的可能性，CASP的发展。
SMT-based Weighted Model Integration with Structure Awareness
University of Trento（特伦托大学）；KU Leuven（鲁汶大学）
加权模型集成（Weighted Model Integration，简称WMO）是一种流行的形式主义，旨在统一混合域中的概率推理方法，涉及逻辑和代数约束。尽管最近有大量的工作，但允许并行算法随着混合问题的复杂性而扩展仍然是一个挑战。在本文中，我们突出了一些现有的国家的最先进的解决方案的实质性限制，并开发了一种算法，结合SMT为基础的枚举，一种有效的技术，在形式化验证，与有效的编码的问题结构。这使得我们的算法可以避免生成冗余模型，从而节省大量的计算。对合成和真实世界数据集的广泛实验评估证实了所提出的解决方案优于现有的替代方案。
Neuro-Symbolic Compliance: Integrating LLMs and SMT Solvers for Automated Financial Legal Analysis
Department of Management Information Systems, National ChengChi University, Taipei, Taiwan（管理信息系，中华大学，台北，台湾）；Department of Electrical Engineering, National Taiwan University, Taipei, Taiwan（电子工程系，台湾大学，台北，台湾）
