We study anti-unification for unranked terms and hedges that may contain term hedge variables. The problem of two ${\tilde{s}}_1$ ${\tilde{s}}_2$ is concerned with finding their generalization, a ${\tilde{q}}$ such both are instances under some substitutions. Hedge variables help to fill in gaps generalizations, while abstract single (sub)terms different top function symbols. First, we design complete minimal algorithm compute least general generalizations. Then, improve the efficiency by...

The Business-to-Business Meeting Scheduling problem consists of scheduling a set meetings between given pairs participants to an event, while taking into account participants’ availability and accommodation capacity. A crucial aspect this is that breaks in schedules should be avoided as much possible. It constitutes challenging combinatorial needs solved for many real world brokerage events.
 In paper we present comparative study Constraint Programming (CP), MixedInteger (MIP) Maximum...

Nominal Unification is an extension of first-order unification where terms can contain binders and performed modulo α equivalence. Here we prove that the existence nominal unifiers be decided in quadratic time. First, linearly-reduce problems to a sequence freshness equalities between atoms, permutation, using ideas as Paterson Wegman for unification. Second, solvability these reduced may checked Finally, point out how Brown Tarjan unbalanced merging, could solve more efficiently

There is a relatively large number of papers dealing with complexity and proof theory issues infinitely-valued logics. Nevertheless, little attention has been paid so far to the development efficient solvers for such In this paper we show how technology Satisfiability Modulo Theories (SMT) can be used build automated theorem provers relevant logics, including Lukasiewicz, Gödel Product Moreover, define test suite those report on an experimental investigation that evaluates practical...

The Resource-Constrained Project Scheduling Problem (RCPSP) is a paradigmatic scheduling problem where the activities of project have to be scheduled while respecting combination precedence and resource constraints. Precedence constraints are relations between two stating that one cannot start until other has ended, bound amount resources used by running simultaneously. Many generalizations RCPSP been proposed in literature, including multiple execution modes for (MRCPSP), or time varying...

Nominal logic is an extension of first-order with equality, name-binding, renaming via name-swapping and freshness names. Contrarily to lambda-terms, in nominal terms, bindable names, called atoms, instantiable variables are considered as distinct entities. Moreover, atoms capturable by instantiations, breaking a fundamental principle the lambda-calculus. Despite these differences, unification can be seen from higher-order perspective. From this view, we show that quadratically reduced...

We present a rule-based Huet's style anti-unification algorithm for simply typed lambda-terms, which computes least general higher-order pattern generalization. For pair of arbitrary terms the same type, such generalization always exists and is unique modulo α -equivalence variable renaming. With minor modification, works untyped lambda-terms as well. The time complexity both algorithms linear.

Abstract RANTANPLAN is a numeric planning solver that takes advantage of recent advances in satisfiability modulo theories. It extends reduction to SAT approaches with an easy and efficient handling fluents using background In this paper, we describe the design choices features RANTANPLAN, especially, how reasoning integrated system. We also provide experimental results showing competitive existing exact planners.

One aspect that has been poorly studied in multiple-valued logics, and particular Lukasiewicz is the generation of instances varying difficulty for evaluating, comparing improving satisfiability solvers. In this paper we present a new class clausal forms, called (L-)clausal motivate their usefulness, study complexity, report on an empirical investigation shows easy-hard-easy pattern phase transition phenomenon when testing L-clausal forms.

One aspect that has been poorly studied in multiple-valued logics, and particular Łukasiewicz logic, is the generation of instances varying difficulty for evaluating, comparing improving satisfiability solvers. With ultimate goal finding challenging benchmarks solvers, we start by defining a natural intuitive class clausal forms (simple Ł-clausal forms) studying their complexity. Since prove problem simple can be solved linear time, then define two new classes (Ł-clausal restricted truly...

Monadic second-order unification is where all function constants occurring in the equations are unary. Here we prove that problem of deciding whether a set monadic has unifier NP-complete, use technique compressing solutions using singleton context-free grammars. We matching also NP-complete.

The Multi-Mode Resource-Constrained Project Scheduling Problem (MRCPSP) is a generalization of the well known (RCPSP). most common exact approaches for solving this problem are based on branch-and-bound algorithms, mixed integer linear programming and Boolean satisfiability (SAT). In paper, we present new approach problem, using Satisfiability Modulo Theories (SMT). We provide two encodings into SMT several reformulation preprocessing techniques. optimization algorithm that propose uses an...

Bounded Second-Order Unification is a decidable variant of undecidable Unification. Stratified Context restriction Unification, whose decidability long-standing open problem. This paper join two separate previous, preliminary papers on NP-completeness and It clarifies some omissions in these papers, joins the algorithmic parts that construct minimal solution, gives clear account method using singleton tree grammars for compression may have potential usage other questions related areas.

We present a rule-based Huet's style anti-unification algorithm for simply-typed lambda-terms in eta-long beta-normal form, which computes least general higher-order pattern generalization. For pair of arbitrary terms the same type, such generalization always exists and is unique modulo alpha-equivalence variable renaming. The it cubic time within linear space. It has been implemented code freely available.

Pseudo-Boolean (PB) constraints are usually encoded into Boolean clauses using compact Binary Decision Diagram (BDD) representations. Although these appear in many problems, they particularly useful for representing resource scheduling problems. Sometimes, the variables PB have implicit at-most-one relations. In this work we introduce a way to take advantage of relations obtain Multi-Decision (MDD) representation those constraints. We provide empirical evidence usefulness technique some...