Wyniki wyszukiwania - BazTech

1

Candidate Selection and Instance Ordering for Realtime Algorithm Configuration

Fitzgerald Tadhg, O'Sullivan Barry

Fundamenta Informaticae

|

2019

|

Vol. 166, nr 2

141--166

EN

Many modern combinatorial solvers have a variety of parameters through which a user can customise their behaviour. Algorithm configuration is the process of selecting good values for these parameters in order to improve performance. Time and again algorithm configuration has been shown to significantly improve the performance of many algorithms for solving challenging computational problems. Automated systems for tuning parameters regularly out-perform human experts, sometimes but orders of magnitude. Online algorithm configurators, such as ReACTR, are able to tune a solver online without incurring costly offline training. As such ReACTR’s main focus is on runtime minimisation while solving combinatorial problems. To do this ReACTR adopts a one-pass methodology where each instance in a stream of instances to be solved is considered only as it arrives. As such ReACTR’s performance is sensitive to the order in which instances arrive. It is still not understood which instance orderings positively or negatively effect the performance of ReACTR. This paper investigates the effect of instance ordering and grouping by empirically evaluating different instance orderings based on difficulty and feature values. Though the end use is generally unable to control the order in which instances arrive it is important to understand which orderings impact Re-ACTR’s performance and to what extent. This study also has practical benefit as such orderings can occur organically. For example as business grows the problems it may encounter, such as routing or scheduling, often grow in size and difficulty. ReACTR’s performance also depends strongly configuration selection procedure used. This component controls which configurations are selected to run in parallel from the internal configuration pool. This paper evaluates various ranking mechanisms and different ways of combining them to better understand how the candidate selection procedure affects realtime algorithm configuration. We show that certain selection procedures are superior to others and that the order which instances arrive in determines which selection procedure performs best. We find that both instance order and grouping can significantly affect the overall solving time of the online automatic algorithm configurator ReACTR. One of the more surprising discoveries is that having groupings of similar instances can actually negatively impact on the overall performance of the configurator. In particular we show that orderings based on nearly any instance feature values can lead to significant reductions in total runtime over random instance orderings. In addition, certain candidate selection procedures are more suited to certain orderings than others and selecting the correct one can show a marked improvement in solving times.

2

Selection of search strategies for solving 3-SAT problems

Pułka A.

International Journal of Applied Mathematics and Computer Science

|

2014

|

Vol. 24, no. 2

283--297

EN

The paper concerns the problem of Boolean satisfiability checking, which is recognized as one of the most important issues in the field of modern digital electronic system verification and design. The paper analyzes different strategies and scenarios of the proving process, and presents a modified and extended version of the author’s FUDASAT algorithm. The original FUDASAT methodology is an intuitive approach that employs a commonsense reasoning methodology. The main objective of the work is to investigate the SAT-solving process and try to formulate a set of rules controlling the reasoning process of the FUDASAT inference engine. In comparison with the author’s previous works, the paper introduces new mechanisms: hypergraph analysis, multiple variable assignments and search space pruning algorithms. The approach considers only 3-SAT class functions, although a generalization of the method is discussed as well. The presented approach has been tested on various benchmarks and compared with the original pure FUDASAT algorithm as well as with other algorithms known from the literature. Finally, the benefits of the proposed SAT solving technique are summarized.

3

An effective SAT-Solving mechanism with backtrack controlled by FDL

Pułka A.

Elektronika : konstrukcje, technologie, zastosowania

|

2011

|

Vol. 52, nr 12

21-25

EN

This work presents a novel approach to SAT solving problem based on commonsense reasoning methodology. The methodology has been implemented and tested in PROLOG. Discussion of different modern approaches to the satisfiability that have been published recently is presented. A parallelism between the SAT solving problem and non-monotonic extensions verifying is given. The new algorithm of SAT solving based on fuzzy default reasoning (FDL) theory FUDASAT and cumulativity of CNF formulas is defined. Optimal backtracking search methodology is explained on examples. Some experiments on various benchmarks show the efficiency and advantages of the proposed methodology.

PL

Artykuł przedstawia nowe podejście do problemu badania spełnialności formuł logicznych oparte na metodzie wnioskowania zdroworozsądkowego. Zaproponowana metoda została zaimplementowana i przetestowana w środowisku języka PROLOG. Przeprowadzono szczegółową dyskusję dotyczącą istniejących nowoczesnych technik sprawdzania spełnialności formuł logicznych, które zostały opublikowane w ostatnich latach. Przedstawiono podobieństwa między problemem badania spełnialności formuł logicznych a weryfikacją rozszerzeń w logice niemonotonicznej. Sformułowano podstawowe założenia nowego algorytmu FUDASAT badania spełnialności formuł logicznych opartego na wnioskowaniu FDL oraz zdefiniowano problem kumulacyjności formuł w postaci normalnej CNF. Metoda optymalnego przeszukiwania podczas nawrotów została opisana na przykładach. Eksperymenty przeprowadzone na zestawach wzorcowych pokazują zalety proponowanej metody.

4

A SAT-based Method for Solving the Two-dimensional Strip Packing Problem

Soh T., Tamura N., Banbara M., Inouey K., Nabeshima H.

Fundamenta Informaticae

|

2010

|

Vol. 102, nr 3/4

467-487

EN

We propose a satisfiability testing (SAT) based exact approach for solving the twodimensional strip packing problem (2SPP). In this problem, we are given a set of rectangles and one large rectangle called a strip. The goal of the problem is to pack all rectangles without overlapping, into the strip by minimizing the overall height of the packing. Although the 2SPP has been studied in Operations Research, some instances are still hard to solve. Our method solves the 2SPP by translating it into a SAT problem through a SAT encoding called order encoding. The translated SAT problems tend to be large; thus, we apply several techniques to reduce the search space by symmetry breaking and positional relations of rectangles. To solve a 2SPP, that is, to compute the minimum height of a 2SPP, we need to repeatedly solve similar SAT problems. We thus reuse learned clauses and assumptions from the previously solved SAT problems. To evaluate our approach, we obtained results for 38 instances from the literature and made comparisons with a constraint satisfaction solver and an ad-hoc 2SPP solver.