Wyniki wyszukiwania - BazTech

1

Selective Unification in (Constraint) Logic Programming

Mesnard Fred, Payet Étienne, Vidal Germán

Fundamenta Informaticae

|

2020

|

Vol. 177, nr 3/4

359--383

EN

Concolic testing is a well-known validation technique for imperative and object oriented programs. In a previous paper, we have introduced an adaptation of this technique to logic programming. At the heart of our framework lies a specific procedure that we call “selective unification”. It is used to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. In this paper, we show that the existing algorithm for selective unification is not complete in the presence of non-linear atoms. We then prove soundness and completeness for a restricted version of the problem where some atoms are required to be linear. We also consider concolic testing in the context of constraint logic programming and extend the notion of selective unification accordingly.

2

Dischargeable Obligations in the SCIFF Framework

Alberti Marco, Gavanelli Marco, Lamma Evelina, Riguzzi Fabrizio, Satoh Ken, Zese Riccardo

Fundamenta Informaticae

|

2020

|

Vol. 176, nr 3/4

321--348

EN

Abductive Logic Programming (ALP) has been proven very effective for formalizing societies of agents, commitments and norms, in particular by mapping the most common deontic operators (obligation, prohibition, permission) to abductive expectations. In our previous works, we have shown that ALP is a suitable framework for representing norms. Normative reasoning and query answering were accommodated by the same abductive proof procedure, named SCIFF. In this work, we introduce a defeasible flavour in this framework, in order to possibly discharge obligations in some scenarios. Abductive expectations can also be qualified as dischargeable, in the new, extended syntax. Both declarative and operational semantics are improved accordingly, and proof of soundness is given under syntax allowedness conditions. Moreover, the dischargement itself might be proved invalid, or incoherent with the rules, due to new knowledge provided later on. In such a case, a discharged expectation might be reinstated and hold again after some evidence is given. We extend the notion of dischargement to take into consideration also the reinstatement of expectations. The expressiveness and power of the extended framework, named SCIFFD, is shown by modeling and reasoning upon a fragment of the Japanese Civil Code. In particular, we consider a case study concerning manifestations of intention and their rescission (Section II of the Japanese Civil Code).

3

Constraint Logic Programming with Polynomial Constraints over Finite Domains

Bergenti F., Monica S., Rossi G.

Fundamenta Informaticae

|

2018

|

Vol. 161, nr 1/2

9--27

EN

This paper introduces an instantiation of the constraint logic programming scheme called CLP(PolyFD) in which variables take values from finite subsets of the integers and constraints are expressed as equalities, inequalities, and disequalities of polynomials with integer coefficients. Such constraints, which we call polynomial constraints over finite domains, can be treated effectively by means of a specific solver under the assumption that initial approximations of the domains of variables are available. The proposed solver deals with constraints in a canonical form and it uses the modified Bernstein form of polynomials to detect the satisfiability of constraints. The solver is complete and a preliminary assessment of its performance is reported.

4

Program Verification using Constraint Handling Rules and Array Constraint Generalizations

De Angelis E., Fioravanti F., Pettorossi A., Proietti M.

Fundamenta Informaticae

|

2017

|

Vol. 150, nr 1

73--117

EN

The transformation of constraint logic programs (CLP programs) has been shown to be an effective methodology for verifying properties of imperative programs. By following this methodology, we encode the negation of a partial correctness property of an imperative program prog as a predicate incorrect defined by a CLP program T, and we show that prog is correct by transforming T into the empty program (and thus incorrect does not hold) through the application of semantics preserving transformation rules. We can also show that prog is incorrect by transforming T into a program with the fact incorrect (and thus incorrect does hold). Some of the transformation rules perform replacements of constraints that are based on properties of the data structures manipulated by the program prog. In this paper we show that Constraint Handling Rules (CHR) are a suitable formalism for representing and applying constraint replacements during the transformation of CLP programs. In particular, we consider programs that manipulate integer arrays and we present a CHR encoding of a constraint replacement strategy based on the theory of arrays. We also propose a novel generalization strategy for constraints on integer arrays that combines CHR constraint replacements with various generalization operators on integer constraints, such as widening and convex hull. Generalization is controlled by additional constraints that relate the variable identifiers in the imperative program prog and the CLP representation of their values. The method presented in this paper has been implemented and we have demonstrated its effectiveness on a set of benchmark programs taken from the literature.

5

Portfolio selection of new product projects: a product reliability perspective

Relich M.

Eksploatacja i Niezawodność

|

2016

|

Vol. 18, no. 4

613--620

EN

Portfolio selection of new product development projects is one of the most important decisions in an enterprise that impact future business profits, competitiveness and survival. Ensuring reliability in a new product is costly but it increases customer satisfaction and reduces the potential warranty cost, contributing to product success. This paper aims to develop an approach for designing decision support system of selecting portfolio of new product development projects, taking into account the aspect of ensuring the desired reliability of products. A portfolio selection problem is formulated in terms of a constraint satisfaction problem that is a pertinent framework for designing a knowledge base. A set of admissible solutions referring to the new product alternatives is obtained with the use of constraint logic programming. The proposed approach is dedicated for enterprises that modernise existing products to develop new products.

PL

Wybór portfela projektów nowych produktów jest jedną z najistotniejszych decyzji podejmowanych w przedsiębiorstwie, wpływającą na przyszłą wartość zysków oraz konkurencyjność i rozwój przedsiębiorstwa. Zapewnienie niezawodności produktu jest kosztowne, ale zwiększa satysfakcję klienta z używanego produktu i redukuje koszty potencjalnych napraw gwarancyjnych, przyczyniając się do sukcesu rynkowego produktu. Celem artykułu jest opracowanie podejścia umożliwiającego budowę systemu wspomagania decyzji dotyczących wyboru portfela projektów nowych produktów do rozwinięcia, z uwzględnieniem aspektu zapewnienia wymaganej niezawodności produktu. Problem wyboru portfela projektów nowych produktów został wyrażony w postaci problemu spełniania ograniczeń, co umożliwia zaprojektowanie systemu opartego na bazie wiedzy. Zbiór rozwiązań dopuszczalnych dotyczący alternatywnych projektów rozwoju nowych produktów jest otrzymywany z wykorzystaniem technik programowania w logice z ograniczeniami. Opracowane podejście jest dedykowane dla przedsiębiorstw, które realizują strategię modernizacji wytwarzanego produktu.

6

A Two-stage approach for an optimum solution of the car assembly scheduling problem. Part 2. CLP solution and real-world example

Mazur M., Niederliński A.

Archives of Control Sciences

|

2015

|

Vol. 25, no. 3

367--375

EN

A Constraint Logic Programming (CLP) tool for solving the problem discussed in Part 1 of the paper has been designed. It is outlined and discussed in the paper. The program has been used for solving a real-world car assembly scheduling problem.

7

A hybrid method for multi-objective optimization of supply chain

Sitek P.

Logistyka

|

2014

|

nr 6

9522--9536

EN

This paper presents a hybrid approach to solving multi-objective optimization problems in supply chain. The proposed approach consists of the integration and hybridization of two modeling and solving environments, i.e., mathematical programming (MP) and constraint logic programming (CLP), to obtain a programming framework that offers significant advantages over the classical approach derived from operational research. The strongest points of both components are combined in the hybrid framework, which by introducing transformation allows a significant reduction in size of a problem and the optimal solution is found a lot faster. This is particularly important in the multi-objective optimization where problems have to be solved over and over again to find a set of Pareto-optimal solutions. An over two thousand-fold reduction in size was obtained for the illustrative examples together with a few hundred-fold reduction in the speed of finding the solution. In addition, the proposed approach allows the introduction of logical constraints that are difficult or impossible to model in operational research environments.

PL

W artykule przedstawiono podejście hybrydowe do optymalizacji wielokryterialnej problemów łańcucha dostaw. Proponowane podejście składa się z dwóch środowisk: programowania matematycznego oraz programowania w logice z ograniczeniami. Przedstawiona integracja pozwala na modelowanie i bardziej efektywne rozwiązywanie problemów optymalizacji występujących w łańcuchach dostaw. Wynika to z redukcji rozmiarów kombinatorycznych problemów. Zaproponowana metoda hybrydowa została przetestowana na modelu ilustracyjnym, który dotyczy optymalizacji wielokryterialnej kosztów operacyjnych łańcucha dostaw z jednej strony oraz kosztów środowiskowych z drugiej. Uzyskane wyniki potwierdzają efektywność zastosowanej metody, która jest wielokrotnie szybsza od podejścia opartego jedynie na programowaniu matematycznym.

8

Modele dla potrzeb rozwiązywania zadań optymalizacji taryf

Pytlak R., Stecz W.

Gospodarka Materiałowa i Logistyka

|

2014

|

nr 7

24--32

PL

W artykule zaprezentowano metody optymalizacji stawek taryfowych telefonii komórkowej z punktu widzenia klienta. Klient stara się minimalizować swoje miesięczne obciążenia rachunkami poprzez dobór optymalnej taryfy telekomunikacyjnej. Zaprezentowano model przydatny dla klientów firm telekomunikacyjnych, które są większymi spółkami, i dla których konstrukcje taryf są bardziej złożone. Opisano przykładowe modele całkowitoliczbowe (MIP) i ich rozszerzenia na programowanie z ograniczeniami (CLP). Podano przykłady w językach ECLiPSe i ILOG CLP.

EN

We present the methods of telecommunication tariff optimization from a point of client’s view. A client which wants to minimize his monthly fees tries to choose a proper tariff model. In case of large companies these models are more complicated and the optimization models should be used. We describe a simple MIP models and their modifications solved with CLP solvers. All the examples were solved with ILOG and ECLiPSe MIP and CLP solvers.

9

Proving Theorems by Program Transformation

Fioravanti F., Pettorossi A., Proietti M., Senni V.

Fundamenta Informaticae

|

2013

|

Vol. 127, nr 1-4

115--134

EN

In this paper we present an overview of the unfold/fold proof method, a method for proving theorems about programs, based on program transformation. As a metalanguage for specifying programs and program properties we adopt constraint logic programming (CLP), and we present a set of transformation rules (including the familiar unfolding and folding rules) which preserve the semantics of CLP programs. Then, we show how program transformation strategies can be used, similarly to theorem proving tactics, for guiding the application of the transformation rules and inferring the properties to be proved. We work out three examples: (i) the proof of predicate equivalences, applied to the verification of equality between CCS processes, (ii) the proof of first order formulas via an extension of the quantifier elimination method, and (iii) the proof of temporal properties of infinite state concurrent systems, by using a transformation strategy that performs program specialization.

10

Controlling Polyvariance for Specialization-based Verification

Fioravanti F., Pettorossi A., Proietti M., Senni V.

Fundamenta Informaticae

|

2013

|

Vol. 124, nr 4

483--502

EN

Program specialization has been proposed as a means of improving constraint-based analysis of infinite state reactive systems. In particular, safety properties can be specified by constraint logic programs encoding (backward or forward) reachability algorithms. These programs are then transformed, before their use for checking safety, by specializing them with respect to the initial states (in the case of backward reachability) or with respect to the unsafe states (in the case of forward reachability). By using the specialized reachability programs, we can considerably increase the number of successful verifications. An important feature of specialization algorithms is the so called polyvariance, that is, the number of specialized variants of the same predicate that are introduced by specialization. Depending on this feature, the specialization time, the size of the specialized program, and the number of successful verifications may vary. We present a specialization framework which is more general than previous proposals and provides control on polyvariance. We demonstrate, through experiments on several infinite state reactive systems, that by a careful choice of the degree of polyvariance we can design specialization-based verification procedures that are both efficient and precise.

11

Koncepcja systemu wspomagania decyzji logistycznych

Sitek P., Wikarek J.

Studia Informatica

|

2011

|

Vol. 32, nr 2B

513-522

PL

W artykule przedstawiono koncepcję systemu wspomagania decyzji logistycznych. Zaproponowano dodatkową warstwę informacyjno-funkcjonalną, która umożliwia współpracę ze standardowymi strukturami systemu zarządzania klasy ERP oraz solverami optymalizacyjnymi. Szczegółowo opisano jeden z problemów decyzyjnych – wieloetapowy problem transportowy. Przedstawiono model matematyczny i jego implementację. Omówiono podstawową strukturę informacyjną systemu wspomagania decyzji.

EN

The concept of decision support system for logistic problems has been presented. Additional layer for information and functionality structures which enable to cooperate with ERP and optimization solvers has been described. The mathematical model for the transportation problem with distribution centers and implementation of them have been presented. The article discusses the basic information structure of the system.

12

Models and tools for improving efficiency in Constraint Logic Programming

Ligęza A.

Decision Making in Manufacturing and Services

|

2011

|

Vol. 5, no. 1-2

69-78

EN

Constraint Satisfaction Problems typically exhibit strong combinatorial explosion. In this paper we present some models and techniques aimed at improving efficiency in Constraint Logic Programming. A hypergraph model of constraints is presented and an outline of strategy planning approach focused on entropy minimization is put forward. An example cryptoaritmetic problem is explored in order to explain the proposed approach.

13

Koncepcja systemu do wspomagania decyzji zarządzania centrum dystrybucyjnym

Sitek P., Wikarek J.

Studia Informatica

|

2010

|

Vol. 31, nr 2B

205-214

PL

W pracy przedstawiono koncepcje systemu wspomagania decyzji dla centrum dystrybucji. Zaproponowano dodatkową warstwę informacyjno-funkcjonalną która umożliwia współpracę ze standardowymi strukturami systemu zarządzania klasy ERP oraz solverami optymalizacyjnymi. Szczegółowo opisano jeden z problemów decyzyjnych dotyczący rozdziału palet, zaproponowano model matematyczny i jego implementację w dwóch środowiskach - programowania matematycznego i programowania w logice z ograniczeniami.

EN

The concept of decision support system for distribution center has been presented. Additional layer for information and functionality structures which enable to cooperate with ERP and optimization solvers has been described. The mathematical model for the detailed problem of palette allocation in distribution center and implementation of them have been used in two environments - mathematical programming and logic constraint programming.

14

Knowledge based and CP-driven approach applied to multi product small-size production flow

Bach I., Bocewicz G., Banaszak Z. A., Muszyński W.

Control and Cybernetics

|

2010

|

Vol. 39, no 1

69-95

EN

Constraint Programming (CP) is an emergent software technology for declarative description and effective solving of large combinatorial problems, especially in the area of integrated production planning. In this context, CP can be considered an appropriate framework for development of decision making software, supporting scheduling of multi-robots in a multi-product job shop. The paper deals with the multi-resource problem, in which more than one shared renewable and non-renewable resource type may be required by a manufacturing operation and the availability of each type is time-windows limited. The problem is NP-complete. The aim of the paper is to present a knowledge based and CP-driven approach to multi-robot task allocation providing prompt service to a set of routine queries, stated both in direct and reverse way. Provided examples illustrate the cases with consideration of accurate and uncertain specification of robot and worker operation time.

15

CLP approach to optimal instruction scheduling for VLIW processors

Domagała Ł.

Archives of Control Sciences

|

2009

|

Vol. 19, no. 2

127-149

EN

Along with modern processor architectures where multiple functional units can execute instructions in parallel and numerous resources have to be managed, there is a need for efficient tools facilitating code generation and enhancing development. The aim is to achieve maximal instruction throughput. This is a place where automatic optimization techniques should be employed due to high complexity of the real life problems. This article presents an approach to optimal instruction scheduling for very long instruction word (VLIW) processors using a constraint logic programming (CLP) solver with particular emphasis on the modulo scheduling technique. Modulo scheduling is an optimization technique used to achieve greater instruction level parallelism than one achievable by just optimally scheduling code basic blocks.

16

CLP-based approach to decision support for SCM systems

Tomczuk-Piróg I., Mądry M., Banaszak Z

Systems Science

|

2007

|

Vol. 33, no 1

39-51

EN

The paper focuses on a selected class of decision problems related with the waste distribution network in SMEs. High efficiency in solving large combinatorial problems offered by implementation of the Constraints Satisfaction Problem (CSP) concept constitute an alternative for the currently available systems based on simulation techniques and operation research. Possible ways of the CSP decomposition as well as possibility of different programming languages application lead then to a problem aimed at searching for a distribution strategy allowing one to interact in an on-line model. The results obtained are implemented in a software package supporting waste distribution network in the SMEs. Illustrative example of the Mozart-based software application is provided.

17

Techniki programowania z ograniczeniami w zarządzaniu wiedzą MŚP

Bach I., Bocewicz G., Banaszek Z.

Pomiary Automatyka Robotyka

|

2007

|

R. 11, nr 2

PL

Proponowane w pracy podejście zakłada, że rozważane przedsiębiorstwo klasy MŚP zadane jest bazą wiedzy opisującą zarówno specyfikujące go dane dokładne i niepewne, a także łączące je relacje (ograniczenia). Przyjęte założenie oznacza, że istnienie odpowiedzi na zbiór pytań rutynowych warunkowane jest spójnością tak rozumianej bazy (istnieniem łańcuchów wnioskowań prowadzących do odpowiedzi), a ich wypracowywanie (uwzględniając skalę zadań) jest z kolei uwarunkowane dostępnością do odpowiednio szybkich (umożliwiających prace w trybie „on-line”) strategii wnioskowania. Proponowane podejście zakłada wykorzystanie metody logiczno-algebraiczne jako języka specyfikacji bazy wiedzy oraz technik programowania z ograniczeniami jako mechanizmu wnioskowania. Przedstawiony przykład ilustruje efektywność potencjalnych, opartych na tym podejściu, systemów wspomagania decyzji.

EN

In this contribution a class of SME is considered, and their specification through the relevant knowledge bases consisting of accurate and uncertain data as well as linking those relations (constraints) is assumed. That means, the responses to a set of routine requests are guaranteed under a condition the knowledge base is consistent, and a decision-making (driven by an inference process) is an interactive one is guaranteed under condition the relevant inference strategies are available. The approach proposed employs the logic-algebraic method as providing a knowledge base representation, and constraints programming techniques as providing inference processes platform. The way of possible approach implementation is illustrated in the example enclosed.

18

Risk assessement in multi-project environment

Tomczuk-Piróg I., Banaszak Z.

Applied Computer Science

|

2007

|

Vol. 3, no 1

73--93

EN

Decision making supported by task-oriented software tools plays a pivotal role in a modern enterprise. That is because commercially available ERP systems are not able to respond in an interactive on-line/real-time mode. It opens a new generation of DSS that enable a fast prototyping of production flows in multi-project environment as well as an integrated approach to project execution evaluation. In that context our goal is to provide a knowledge base approach allowing one to be independent on a context or representation of particular data as well as allowing designing an interactive and task-oriented decision support system (DSS). The assumed knowledge base mode of specifying a production system leads to solving a logic-algebraic method (LAM) decision problem. The approach proposed complements the decision system with an additional module (evaluation module) and facilitates searching for possible solutions meeting company production programme execution evaluation criteria. The results obtained are implemented in a software package supporting project management in the SMEs. Illustrative example of the ILOG-based software application is provided.

19

Zastosowanie programowania ograniczeniowego w logice dla problemu aukcji kombinatorycznych

Tatoń T.

Zeszyty Naukowe. Automatyka / Politechnika Śląska

|

2006

|

z. 145

217-224

PL

Artykuł przedstawia główne założenia aukcji kombinatorycznej. Umieszczono w nim opis modelu matematycznego dla aukcji kombinatorycznej wielu jednostek wielu towarów. Przedstawiono rozwiązanie problemu w CHIP'ie za pomocą programowania ograniczeniowego w logice. Rozwiązanie to zilustrowano na konkretnym przykładzie oraz omówiono otrzymane wyniki. Autor zwraca uwagę na zagadnienia ograniczeń występujących w aukcjach kombinatorycznych, a w szczególności ograniczeń komplementarnych i substytucyjnych.

EN

A combinatorial auction problem is formulated and solved using constraint logic programming in CHIP. Building of own declarative application, pointing out the optimum combination of bids in multi-unit combinatorial auction has been discused in detail. The received results were introduced the concrete example of auction, and talked over

20

Zastosowanie programowania ograniczeniowego w logice dla problemu konfigurowania zespołów pracowników

Tatoń T.

Zeszyty Naukowe. Automatyka / Politechnika Śląska

|

2006

|

z. 145

209-216

PL

Przedstawiono sformułowanie problemu konfiguracji zespołu pracowników. Zaprezentowano rozwiązanie tego problemu za pomocą programowania ograniczeniowego w logice, zaimplementowanego w języku CHIP. Przedyskutowano możliwość wprowadzenia dodatkowych ograniczeń.

EN

The paper starts with a formulation of a team management problem. Next, the problem is solved using constraint logic programming implemented in CHIP. Obtained results were interpreted.