arXiv cs/04090302004-09-14cs.LOcs.PL

Automatic Generation of CHR Constraint Solvers

Slim Abdennadher, Christophe Rigotti

备注：: to be published in Theory and Practice of Logic Programming, 16 pages, 2 figures

英文摘要：

In this paper, we present a framework for automatic generation of CHR solvers given the logical specification of the constraints. This approach takes advantage of the power of tabled resolution for constraint logic programming, in order to check the validity of the rules. Compared to previous works where different methods for automatic generation of constraint solvers have been proposed, our approach enables the generation of more expressive rules (even recursive and splitting rules) that can be used directly as CHR solvers.

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

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

英文摘要相关论文

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

继续探索

相关论文

证明器和求解器的验证

Verification of Provers and Solvers

University of Innsbruck（因斯布鲁克大学）

介绍自动推导工具与证明助手的连接方法，通过认证和验证等方式，回顾比较现有方法并提及成功应用。

2026-07-29cs.LOcs.SC

给定计算时间限制下伪布尔优化的自动算法选择

Automatic Algorithm Selection for Pseudo-Boolean Optimization with Given Computational Time Limits

Universidad de Concepción（康塞普西翁大学）；University of California, Berkeley（加州大学伯克利分校）；Universidad Técnica Federico Santa María（费德里科圣玛丽亚理工大学）

本研究针对伪布尔优化问题，设计了一种考虑用户指定计算时间限制的随时元求解器，通过广泛的实证证明其性能大幅优于组合中最佳单求解器Gurobi。

2023-09-07cs.AIcs.LO

A CHR-based Implementation of Known Arc-Consistency

In classical CLP(FD) systems, domains of variables are completely known at the beginning of the constraint propagation process. However, in systems interacting with an external environment, acquiring the whole domains of variables before the beginning of constraint propagation may cause waste of computation time, or even obsolescence of the acquired data at the time of use. For such cases, the Interactive Constraint Satisfaction Problem (ICSP) model has been proposed as an extension of the CSP model, to make it possible to start constraint propagation even when domains are not fully known, per…

2004-08-24cs.AIcs.LO

GUBS Upper Bound Solver (Extended Abstract)

In this extended abstract we present the GUBS Upper Bound Solver. GUBS is a dedicated constraint solver over the naturals for inequalities formed over uninterpreted function symbols and standard arithmetic operations. GUBS now forms the backbone of HoSA, a tool for analysing space and time complexity of higher-order functional programs automatically. We give insights about the implemen- tation and report different case studies.

2017-04-19cs.LO

加速傅里叶SAT (AFSAT)：完全实现基于GPU的对称伪布尔SAT求解器

Accelerated Fourier SAT (AFSAT): Fully Realising a GPU-based Symmetric Pseudo-Boolean SAT Solver

School of Computing, Australian National University（澳大利亚国立大学计算机学院）

提出AFSAT，一个基于连续局部搜索的GPU加速伪布尔SAT求解器，通过JAX编译器实现大规模并行化，显著提升数值稳定性、运行速度和内存效率。

2026-06-04cs.AIcs.LO

用图回溯泛化CDCL

Generalizing CDCL with Graph Backtracking

TU Wien（维也纳工业大学）

提出一种基于图回溯的细粒度回溯方案，通过用户自定义权重函数优化冲突修复，减少文字传播次数，提升SAT求解器性能。

2026-05-27cs.LO

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

使用SAT求解器自动寻找硬度归约

Finding hardness reductions automatically using SAT solvers

Freie Universität Berlin（柏林自由大学）；Technische Universität Berlin（柏林工业大学）；Charles University（查理大学）

本文提出一种基于SAT的自动化框架，用于构造归约小工具，并证明多种组合结构（包括内部三元系统及其高维推广）的完备性问题为NP完全。

2024-02-09cs.AIcs.CCcs.DS

Efficiently Coupling the I-DLV Grounder with ASP Solvers

We present I-DLV+MS , a new Answer Set Programming (ASP) system that integrates an efficient grounder, namely I-DLV, with an automatic selector that inductively chooses a solver: depending on some inherent features of the instantiation produced by I-DLV, machine learning techniques guide the selection of the most appropriate solver. The system participated in the latest (7th) ASP competition, winning the regular track, category SP (i.e., one processor allowed). Under consideration in Theory and Practice of Logic Programming (TPLP).

2018-10-04cs.LO

Handling Conflicts in Depth-First Search for LTL Tableau to Debug Compliance Based Languages

Providing adequate tools to tackle the problem of inconsistent compliance rules is a critical research topic. This problem is of paramount importance to achieve automatic support for early declarative design and to support evolution of rules in contract-based or service-based systems. In this paper we investigate the problem of extracting temporal unsatisfiable cores in order to detect the inconsistent part of a specification. We extend conflict-driven SAT-solver to provide a new conflict-driven depth-first-search solver for temporal logic. We use this solver to compute LTL unsatisfiable cores…

2011-09-13cs.LO

On the Expressive Power of Multiple Heads in CHR

Constraint Handling Rules (CHR) is a committed-choice declarative language which has been originally designed for writing constraint solvers and which is nowadays a general purpose language. CHR programs consist of multi-headed guarded rules which allow to rewrite constraints into simpler ones until a solved form is reached. Many empirical evidences suggest that multiple heads augment the expressive power of the language, however no formal result in this direction has been proved, so far. In the first part of this paper we analyze the Turing completeness of CHR with respect to the underneath c…

2011-01-18cs.DCcs.LO