A Study of Operations Research Solutions Techniques in Combinatorial Problem towards Constraint Programming

INTRODUCTION

In this article we show a formal display that closely follows the appropriate combinatorial arguments, which proves this identity. After presenting formal notes and their fundamental algebraic transformations, we show how, in practice, combination arguments used in the literature to demonstrate a selection of identities with binomial coefficients and permutations can be formally interpreted. We shall give the typical combination proof of the theorem Inclusion Exclusion in particular in a formal version. Furthermore, some of these calculations illustrate how a recursive definition can be reached for resolving a counter problem, i.e. formally derived a recursive algorithm to solve the problem. The official tool used is known as an operational instrument. In the main, the Sigma (Σ) notation, used to express and manipulate summations and numbers, is an abstract and axiomatic generalization. Operations enable various natural operations with combinatorial significance because of their algebraic properties. Among these algebraic properties are: a way of splitting summaries with different divided separation criteria (a measure called conditioning) and the ability to map or transform the counted elements in a bijection to a variety of elements (basically, count and summation indices) (the essence of a combinatorial argument). In terms of graphical, symbolic and material object count, combinational arguments are generally expressed, such as paths along the rims of a grid, 'montane ranges," matched parenthetic parentheses, grid tiling by blocks, beaded necklaces etc. We modell these objects with discreet mathematical structures like the finite numbers, strings and finite sequences of numbers in order to officially formalize these concepts (possibly considered as circular). This formal device not only offers official support for expressing and reasoning ideas and evidence, but also enables the deduction of recursive functions to identify solutions to count problems. This method can be widespread to produce formal derivations of recursive algorithmic solutions through gradual refining of certain specifications. We also find this approach feasible to make automated evidence control of combinatorial evidence easier.

methods may be imported into CP. In order to reduce variable domains, the most obvious function of an OR method is to apply it to a constraint or subset of limits. If the restrictions include certain linear inequalities, a variable subject to such inequalities can be minimized or maximized, thus possibly reducing the domain of the variable. The problem of minimizing or maximizing is a linear programming (LP) issue, an OR staple. This is one example of OR's most common scheme: to relax the CP problem, in the form of an OR model, like an LP model. Relaxation solution helps to reduce the domain or guide the search. Other OR models that can play this role include linear (MILP) models (which can be relaxed by themselves), relaxation from Lagrangean and dynamic programming models. OR has also developed expert relieves for a wide range of ordinary situations and offers tools to relax globally. A CP solver has several advantages of relaxation. (a) it may tighten a variable boundary. (b) In the original problem, its solution may become feasible. (c) If not, the solution may be a promising guide for the search. (d) One solution can allow domains to be filtered in other ways, for example through cost reduction or Lagrange multipliers, or by dynamical programming examinations of state space. (e) The solution can deliver a binding value for optimal pruning of the search tree for optimisation problems. (e) More generally, by combining several limitations relaxed in a single OR-based relaxation process, global problems that are only partly captured by constraint propagation can be taken advantage of. The problem is broken down by other hybridisation schemes, so the CP and OR can attack the parts of the problem they most suit. To date, branch and price algorithms and generalizations of Benders degradation have been the most important schemes. Branch and price based on CP generate a column, i.e., the variables that are to be dynamically added to enhance the solution during a branch search. For the "row generation," decomposition is often done using CP; in other words, restrictions (goods) are generated that guide the main search method.

Throughout this text, a one-argument function application over a variable or a constant is denoted by an infix dot ‗.‘. To denote multiplications, generally, we will avoid the usual juxtaposition convention by using an explicit infix dot sign (·) due to the confusion caused by naming variables with more than one letter. By true and f alse , we denote, besides the boolean values, the obvious 0-ary constant predicates. The following logical connectives are listed in order of decreasing binding power (those listed as a pair has the same precedence): ¬ denotes negation, ∨ and ∧ denote disjunction and conjunction respectively, and ≡ and 6≡ denote equivalence and discrepancy respectively. As usual, the symbols ∀ and ∃ denote the universal and the existential quantifier respectively. For set operations, we use the usual symbols for union (∪), intersection (∩), membership (∈) and inclusion (⊆). All other notations will be defined in the place where they are used.

Summations may be interpreted as iterations of the addition operation. This view of iterated sums can be generalized to any associative and commutative operator ⊕ with advantages of unified notation and calculation through their generalized axiomatic description. The expression denotes the iteration of ⊕ over the values of the expression P.i for all the values of i belonging to the domain (or type) D and satisfying the range condition R.i. We call this kind of expression an operational on ⊕. These expressions are also known as quantifications. Observe that in order to avoid an accumulation of parenthesis, we sometimes write (when it does not lead to confusion) R.i to denote application of expression R (considered as a function) to argument i. In order to keep some resemblance with the traditional notation we allow to write instead of instead of . To deal with a false range R.i, it becomes necessary that operator ⊕ has an identity in addition to the symmetry and associativity properties. The table above illustrates the unifying effect of this notation. type to indicate the range of values it may assume; however, to avoid cumbersome repetitions, we may state just once the type of a certain index in the context of a calculation. In addition, the range is sometimes omitted when it is refers to the entire domain of variation of i; formally, this correspond to have the predicate true as a range. In this case the form of the operational is One more thing, the counting operational is somewhat different from the others. We introduce it as follows. could be considered ‗syntactic sugar‘ for Similarly, (#i ∈ D :: R.i) is defined as (Σi ∈ D : R.i : 1) or |{i ∈ D | R.i}| (the cardinal of the set of elements in D that fulfill property R).

The operational unifying effect is not limited to notation. It is possible to give operations an abstract treatment in accordance with calculation style in order to easily manipulate the algebraic. Due to the fact that operations are defined as iterating applications of an associative and switched binary operator, properties are generalized which are generally only summaries. These properties are achieved every time the operations are well defined, even if an endless number of operations are involved. For example, if they converge in the case of summations. Being ⊕ an arbitrary associative commutative binary operator defined and taking values on a domain D, the following properties are valid for operationals of the form (⊕i : R : T) (with R, S Boolean expressions, and T an expression taking values on D). In the following, we suppose as understood that indices i, j take all their values on D. Splitting. whenever ranges R and S are disjoint. Formally,. Mapping. whenever f is a bijective function from E to D such

Nesting. This requires index j not appearing in R as a free (unbound) variable. Empty Range. This rule requires ⊕ to have an identity element u. One Point. is the expression obtained from substituting K for all occurrences of i in T. For the counting operational fulfills similar properties, here R, S, T must be Boolean expressions. Splitting. whenever ranges R and S are disjoint.

In this section we present different examples of calculational proofs of numerical identities inspired by the corresponding combinatorial proofs as they appear in the literature. For the sake of easing human reading, these proofs are rigorous but not entirely formal. For instance, the mention of the axioms for operationals in the explanations for each step of our calculations just hints the main ideas to justify them. In particular, we leave to the reader to justify that in the mapping steps, the corresponding transformations are in fact bijections from one range of values to the other.

We define Pn as the number of permutations of the elements in [n]. Formally, we represent a permutation in as a non-repeating sequence q in sq[n] of length n, that encodes a bijection mapping any . Consequently, we define pm[n] as where nrep.s means that the sequence s does not repeat its elements. For the sake of easy manipulation of permutations, we define, for a (finite) sequence s of integers, its normalization with respect to the deletion of its element in position as follows meaning that s.i is removed from s, elements of s less than s.i are left unchanged, and elements bigger than s.i are subtracted by 1. Here, t=sb1(s, m), with m a value not occurring at s, is equivalent to the formal expression To remove an element of a permutation p of the elements of [n] in position i implies to shift, one position to the left, the elements to the right of the element removed, as well as subtracting 1 from all the elements bigger than it. This way, we bijectively obtain a permutation of [n−1]. Expressing it is easy to calculate. Clearly P1 = 1. For n>1 we have Observing the obtained recursive equation, we conclude that . We have proved the following proposition. Proposition 1:

We define the arithmetic function as the only solution to the functional equation on X a It is not hard to prove that n k corresponds to the number of subsets of size k, of a set of n elements (for instance [n], the set of integers from 1 to n). This shows the existence of a solution, its uniqueness is easily proved by induction. Proof : Let Considering the cases defining equation (0), we note that the cases k >n, k= 0 and k=n are pretty simple, since in those cases, there is just one subset or none at a This proves that is a solution for X in equation (0), and therefore, The two previous propositions show how to formally obtain a recursive definition for the solution of a counting problem. Next proposition correspond to Identity

This study was to demonstrate how to give the combinatorial arguments the formal content which we believe to have achieved. We did this to find ways to facilitate their automatic testing. We do not propose this formalization to replace informal arguments as alternative evidence. We believe, in fact, that the formal evidence can be read easily only by taking into account the informal ideas behind its original counterparts.

[1] Achterberg, T. (2016): SCIP: Solving constraint integer programs. Mathematical Programming Computation 1, pp. 1–41. [2] Aggoun, A., Beldiceanu, N. (2014): Extending CHIP in order to solve complex scheduling and placement problems. Mathematical and Computer Modelling 17, pp. 57–73 River, NJ [4] Althaus, E., Bockmayr, A., Elf, M., Kasper, T., J¨uenger, M., Mehlhorn, K. (2012): SCIL— Symbolic constraints in integer linear programming. In: 10th European symposium on Algorithms, Lecture Notes in Computer Science, vol. 2461, pp. 75–87. Springer [5] Andersen, H.R. (2017): An introduction to binary decision diagrams. Lecture notes, available online, IT University of Copenhagen [6] Andersen, H.R., Hadˇzi´c, T., Hooker, J.N., Tiedemann, P. (2017): A constraint store based on multivalued decision diagrams. In: C. Bessiere (ed.) Principles and Practice of Constraint Programming (CP 2017), Lecture Notes in Computer Science, vol. 4741, pp. 118–132. Springer [7] Appa, G., Magos, D., Mourtos, I. (2015): A polyhedral approach to the alldifferent system. Mathematical Programming 124, pp. 1–52 [8] Appa, G., Mourtos, I., Magos, D. (2012): Integrating constraint and integer programming for the orthogonal Latin squares problem. In: P. Van Hentenryck (ed.) Principles and Practice of Constraint Programming (CP 2012), Lecture Notes in Computer Science, vol. 2470, pp. 17–32. Springer [9] Aron, I., Hooker, J.N., Yunes, T.H. (2014): SIMPL: A system for integrating optimization techniques. In: J.C. R´egin, M. Rueher (eds.) CPAIOR Proceedings, Lecture Notes in Computer Science, vol. 3011, pp. 21–36. Springer . [10] Bacchus, F., Dalmao, S., Pitassi, T. (2014): Relaxation search: A simple way of managing optional clauses. In: AAAI Conference on Artificial Intelligence, pp. 835–841 [11] Bajestani, M.A., Beck, J.C. (2016): Scheduling a dynamic aircraft repair shop with limited repair resources. Journal of Artificial Intelligence Research 47, pp. 35–70 [12] Bajgiran, O., Cire, A., Rousseau, L.M. (2017): A first look at picking dual variables for maximizing reduced-cost based fixing. In: M. Lombardi, D. Salvagnin (eds.) CPAIOR Proceedings, Lecture Notes in

Research Scholar, Himalayan University Itanagar, Arunachal Pradesh