| 1. |
- Arafailova, Ekaterina, et al.
(author)
-
Systematic Derivation of Bounds and Glue Constraints for Time-Series Constraints
- 2016
-
In: Principles and Practice of Constraint Programming. - Cham : Springer Publishing Company. - 9783319449524 - 9783319449531 ; , s. 13-29
-
Conference paper (peer-reviewed)abstract
- Integer time series are often subject to constraints on the aggregation of the integer features of all occurrences of some pattern within the series. For example, the number of inflexions may be constrained, or the sum of the peak maxima, or the minimum of the peak widths. It is currently unknown how to maintain domain consistency efficiently on such constraints. We propose parametric ways of systematically deriving glue constraints, which are a particular kind of implied constraints, as well as aggregation bounds that can be added to the decomposition of time-series constraints [5]. We evaluate the beneficial propagation impact of the derived implied constraints and bounds, both alone and together.
|
|
| 2. |
- Beldiceanu, Nicolas, et al.
(author)
-
Linking Prefixes and Suffixes for Constraints Encoded Using Automata with Accumulators
- 2014. - 7
-
In: Principles and Practice of Constraint Programming. - Cham : Springer International Publishing. - 9783319104270 ; , s. 142-157
-
Conference paper (peer-reviewed)abstract
- Consider a constraint on a sequence of variables functionally determining a result variable that is unchanged under reversal of the sequence. Most such constraints have a compact encoding via an automaton augmented with accumulators, but it is unknown how to maintain domain consistency efficiently for most of them. Using such an automaton for such a constraint, we derive an implied constraint between the result variables for a sequence, a prefix thereof, and the corresponding suffix. We show the usefulness of this implied constraint in constraint solving, both by local search and by propagation-based systematic search.
|
|
| 3. |
- Beldiceanu, Nicolas, et al.
(author)
-
On matrices, automata, and double counting
- 2010
-
In: Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems. - Berlin : Springer-Verlag. ; , s. 10-24
-
Conference paper (peer-reviewed)
|
|
| 4. |
|
|
| 5. |
- Beldiceanu, Nicolas, et al.
(author)
-
On the reification of global constraints
- 2013
-
In: Constraints. - : Springer Science and Business Media LLC. - 1383-7133 .- 1572-9354. ; 18:1, s. 1-6
-
Journal article (peer-reviewed)
|
|
| 6. |
- Carlsson, Mats, et al.
(author)
-
Modelling and verification of user interactions using constraint programming
- 2017
-
In: Proc. 3rd International Conference on Software Quality, Reliability and Security. - : IEEE Computer Society. - 9781538620724 - 9781538620731 ; , s. 541-547
-
Conference paper (peer-reviewed)abstract
- Graphical user interfaces are important components of today's software. User interfaces often require checking correctness of user interactions. In web applications such checks can be a part of the JavaScript code. User interfaces in web applications can evolve, some elements can be removed and new elements can be added. To check JavaScript code covers all possible incorrect scenarios in user interactions in web application, constraint programming is used. We use the MiniZinc constraint modelling language to model incorrect user behaviour and to convert JavaScript code into a constraint model. Then we perform an equivalence check to find deviations in JavaScript code. The approach was applied to design user interface of an industrial software product.
|
|
| 7. |
- Dekker, Jip J., et al.
(author)
-
Auto-tabling for subproblem presolving in MiniZinc
- 2017
-
In: Constraints. - : Springer Science and Business Media LLC. - 1383-7133 .- 1572-9354. ; 22:4, s. 512-529
-
Journal article (peer-reviewed)abstract
- A well-known and powerful constraint model reformulation is to compute the solutions to a model part, say a custom constraint predicate, and tabulate them within an extensional constraint that replaces that model part. Despite the possibility of achieving higher solving performance, this tabling reformulation is often not tried, because it is tedious to perform; further, if successful, it obfuscates the original model. In order to encourage modellers to try tabling, we extend the MiniZinc toolchain to perform the automatic tabling of suitably annotated predicate definitions, without requiring any changes to solvers, thereby eliminating both the tedium and the obfuscation. Our experiments show that automated tabling yields the same tables as manual tabling, and that tabling is beneficial for solvers of several solving technologies.
|
|
| 8. |
- Dubois, Catherine, et al.
(author)
-
Exploring Properties of a Telecommunication Protocol with Message Delay Using Interactive Theorem Prover
- 2018
-
In: International Conference on Software Engineering and Formal Methods. - Cham : Springer International Publishing. - 9783319929699 - 9783319929705 ; , s. 239-253
-
Conference paper (peer-reviewed)abstract
- An important task of testing a telecommunication protocol consists in analysing logs. The goal of log analysis is to check that the timing and the content of transmitted messages comply with specification. In order to perform such checks, protocols can be described using a constraint modelling language. In this paper we focus on a complex protocol where some messages can be delayed. Simply introducing variables for possible delays for all messages in the constraint model can drastically increase the complexity of the problem. However, some delays can be calculated, but this calculation is difficult to do by hand and to justify. We present an industrial application of the Coq proof assistant to prove a property of a 4G protocol and validate a constraint model. By using interactive theorem proving we derived constraints for message delays of the protocol and found missing constraints in the initial model.
|
|
| 9. |
- Forghani, Kamran, et al.
(author)
-
Maximizing value yield in wood industry through flexible sawing and product grading based on wane and log shape
- 2024
-
In: Computers and Electronics in Agriculture. - : Elsevier. - 0168-1699 .- 1872-7107. ; 216
-
Journal article (peer-reviewed)abstract
- The optimization of sawing processes in the wood industry is critical for maximizing efficiency and profitability. The introduction of computerized tomography scanners provides sawmill operators with three-dimensional internal models of logs, which can be used to assess value and yield more accurately. We present a methodology for solving the sawing optimization problem employing a flexible sawing scheme that allows greater flexibility in cutting logs into products while considering product quality classes influenced by wane defects. The methodology has two phases: preprocessing and optimization. In the preprocessing phase, two alternative algorithms are given that generate and evaluate the potential sawing positions of products by considering the 3D surface of the log, product size requirements, and product quality classes. In the optimization phase, a maximum set-packing problem is solved for the preprocessed data using mixed-integer programming (MIP), aiming to obtain a feasible cut pattern that maximizes value yield. This is implemented in a system named FlexSaw, which takes advantage of parallel computation during the preprocessing phase and utilizes a MIP solver during the optimization phase. The proposed sawing methods are evaluated on the Swedish Pine Stem Bank. Additionally, FlexSaw is compared with an existing tool that utilizes cant sawing. Results demonstrate the superiority of flexible sawing. While the practical feasibility of implementing a flexible way of sawing logs is constrained by the limitations of current sawmill machinery, the potential increase in yield promotes the exploration of alternative machinery in the wood industry.
|
|
| 10. |
- Grinchtein, Olga, et al.
(author)
-
A Constraint Optimisation Model for Analysis of Telecommunication Protocol Logs
- 2015. - 6
-
In: Tests and Proofs. - Cham : Springer International Publishing. - 9783319212142 - 9783319212159 ; , s. 137-154
-
Conference paper (peer-reviewed)abstract
- Testing a telecommunication protocol often requires protocol log analysis. A protocol log is a sequence of messages with timestamps. Protocol log analysis involves checking that the content of messages and timestamps are correct with respect to the protocol specification. We model a protocol specification using constraint programming (MiniZinc), and we present an approach where a constraint solver is used to perform protocol log analysis. Our case study is the Public Warning System service, which is a part of the Long Term Evolution (LTE) 4G standard. We were able to analyse logs containing more than 3000 messages with more than 4000 errors.
|
|
