scholarly journals Decidable linear list constraints

10.29007/d7t4 ◽  
2018 ◽  
Author(s):  
Sabine Bauer ◽  
Martin Hofmann
Keyword(s):  
Constraint Satisfaction ◽  
Constraint Satisfaction Problem ◽  
Object Oriented ◽  
Type Inference ◽  
Additional Restriction ◽  
Original Formulation ◽  
Amortized Analysis ◽  
Infinite Tree ◽  
Linear List

We present new results on a constraint satisfaction problem arising from the inference of resource types in automatic amortized analysis for object-oriented programs by Rodriguez and Hofmann.These constraints are essentially linear inequalities between infinite lists of nonnegative rational numbers which are added and compared pointwise. We study the question of satisfiability of a system of such constraints in two variants with significantly different complexity. We show that in its general form (which is the original formulation presented by Hofmann and Rodriguez at LPAR 2012) this satisfiability problem is hard for the famous Skolem-Mahler-Lech problem whose decidability status is still open but which is at least NP-hard. We then identify a subcase of the problem that still covers all instances arising from type inference in the aforementioned amortized analysis and show decidability of satisfiability in polynomial time by a reduction to linear programming. We further give a classification of the growth rates of satisfiable systems in this format and are now able to draw conclusions about resource bounds for programs that involve lists and also arbitrary data structures if we make the additional restriction that their resource annotations are generated by an infinite list (rather than an infinite tree as in the most general case). Decidability of the tree case which was also part of the original formulation by Hofmann and Rodriguez still remains an open problem.

A classification and constraint-based framework for configuration

1998 ◽  
Vol 12 (4) ◽  
pp. 383-397 ◽  
Author(s):  
DANIEL MAILHARRO
Keyword(s):  
Constraint Satisfaction ◽  
Domain Knowledge ◽  
Constraint Satisfaction Problem ◽  
Object Oriented ◽  
Classification Problem ◽  
Single Model ◽  
Arc Consistency ◽  
Configuration Problem ◽  
Taxonomic Reasoning ◽  
New Framework

One of the main difficulties with configuration problem solving lies in the representation of the domain knowledge because many different aspects, such as taxonomy, topology, constraints, resource balancing, component generation, etc., have to be captured in a single model. This model must be expressive, declarative, and structured enough to be easy to maintain and to be easily used by many different kind of reasoning algorithms. This paper presents a new framework where a configuration problem is considered both as a classification problem and as a constraint satisfaction problem (CSP). Our approach deeply blends concepts from the CSP and object-oriented paradigms to adopt the strengths of both. We expose how we have integrated taxonomic reasoning in the constraint programming schema. We also introduce new constrained variables with nonfinite domains to deal with the fact that the set of components is previously unknown and is constructed during the search for solution. Our work strongly focuses on the representation and the structuring of the domain knowledge, because the most common drawback of previous works is the difficulty to maintain the knowledge base that is due to a lack of structure and expressiveness of the knowledge representation model. The main contribution of our work is to provide an object-oriented model completely integrated in the CSP schema, with inheritance and classification mechanisms, and with specific arc consistency algorithms.

Revisiting dynamic constraint satisfaction for model-based planning

2016 ◽  
Vol 31 (5) ◽  
pp. 429-439
Author(s):  
Jeremy Frank
Keyword(s):  
Constraint Satisfaction ◽  
Optimization Problems ◽  
Constraint Satisfaction Problem ◽  
Automated Planning ◽  
Planning Models ◽  
Constraint Reasoning ◽  
Dynamic Constraint ◽  
Mixed Initiative ◽  
Planning Problems

AbstractAs planning problems become more complex, it is increasingly useful to integrate complex constraints on time and resources into planning models, and use constraint reasoning approaches to help solve the resulting problems. Dynamic constraint satisfaction is a key enabler of automated planning in the presence of such constraints. In this paper, we identify some limitations with the previously developed theories of dynamic constraint satisfaction. We identify a minimum set of elementary transformations from which all other transformations can be constructed. We propose a new classification of dynamic constraint satisfaction transformations based on a formal criteria, namely the change in the fraction of solutions. This criteria can be used to evaluate elementary transformations of a constraint satisfaction problem as well as sequences of transformations. We extend the notion of transformations to include constrained optimization problems. We discuss how this new framework can inform the evolution of planning models, automated planning algorithms, and mixed-initiative planning.

scholarly journals Permutation groups with small orbit growth

2021 ◽  
Vol 0 (0) ◽  
Author(s):  
Manuel Bodirsky ◽  
Bertalan Bodor
Keyword(s):  
Automorphism Group ◽  
Constraint Satisfaction ◽  
Constraint Satisfaction Problem ◽  
Permutation Groups ◽  
First Order ◽  
Finite Covers

Abstract Let K exp + \mathcal{K}_{{\operatorname{exp}}{+}} be the class of all structures 𝔄 such that the automorphism group of 𝔄 has at most c ⁢ n d ⁢ n cn^{dn} orbits in its componentwise action on the set of 𝑛-tuples with pairwise distinct entries, for some constants c , d c,d with d < 1 d<1 . We show that K exp + \mathcal{K}_{{\operatorname{exp}}{+}} is precisely the class of finite covers of first-order reducts of unary structures, and also that K exp + \mathcal{K}_{{\operatorname{exp}}{+}} is precisely the class of first-order reducts of finite covers of unary structures. It follows that the class of first-order reducts of finite covers of unary structures is closed under taking model companions and model-complete cores, which is an important property when studying the constraint satisfaction problem for structures from K exp + \mathcal{K}_{{\operatorname{exp}}{+}} . We also show that Thomas’ conjecture holds for K exp + \mathcal{K}_{{\operatorname{exp}}{+}} : all structures in K exp + \mathcal{K}_{{\operatorname{exp}}{+}} have finitely many first-order reducts up to first-order interdefinability.

Sign in / Sign up

Export Citation Format

Share Document