This thesis describes a Coq formalization of realizability interpretations of arithmetic. The realizability interpretations are based on partial combinatory algebras—to each partial combinatory algebra there is an associated realizability interpretation. I construct two partial combinatory algebras. One of these gives a realizability interpretation equivalent to Kleene’s original one, without involving the usual recursion-theoretic machinery. / Den här uppsatsen beskriver en Coq-formalisering av realiserbarhetstolkningar av aritmetik. Realiserbarhetstolkningarna baseras på partiella kombinatoriska algebror—för varje partiell kombinatorisk algebra finns det en motsvarande realiserbarhetstolkning. Jag konstruerar två partiella kombinatoriska algebror. En av dessa ger en realiserbarhetstolkning som är ekvivalent med Kleenes ursprungliga tolkning, men dess konstruktion använder inte det sedvanliga rekursionsteoretiska maskineriet.

<p>Med tanke på att offentlig upphandling är ett mycket stort område, främst med tanke på dess ekonomiska värde, är det viktigt att det finns en väl fungerande konkurrens. Syftet med uppsatsen är att se hur marknaden för offentlig upphandling påverkas av ett större deltagande av SME-företag, vilka möjligheter finns att påverka konkurrensen och hur upplever SME-företagen upphandlingsprocessen.</p><p> </p><p>Vi tog en initial kontakt med Svenskt Näringsliv som gav oss information och hjälpte till med avgränsningarna. Tillvägagångssättet i uppsatsen kan sägas tillhöra en abduktivt tillvägagångssätt. Valet gjordes att använda kvalitativ metod och därmed bestod empirinsamlingen av intervjuer med två personer från kommunen och tre företag som deltar vid offentlig upphandling. Därefter började vi jämföra teori med empiri. Utifrån detta har vi svarat på vår frågeställning.</p><p> </p><p>De slutsatser vi dragit i vår uppsats är att inom tjänstesektorn torde företagen ha likartade förutsättningar att delta vid upphandlingar, framför allt genom att många konsultuppdrag upphandlas. Det område som kan anses minst jämlik mellan SME-företag och stora företag är byggentreprenader där det av naturliga skäl blir svårt för mindre företag att vara med och lämna anbud. Här skulle vi vilja se ett ökat användande av kombinatorisk upphandling för att underlätta för SME-företag att lämna anbud och därmed öka konkurrensen på marknaden. Det vi fått fram är att myndigheterna kan göra förfrågningsunderlagen tydligare och dela upp upphandlingarna i mindre delar, för att ytterligare öka konkurrensen.</p><p> </p><p>Intervjuerna med företagen har gett oss att det inte tycker anser att det finns några särskilt krångliga moment vid offentlig upphandling. Samtidigt har dessa företag varit med ganska länge och lämnat anbud vid offentlig upphandling vilket medför att de har byggt upp vissa rutiner för att underlätta det administrativa arbetet vid offentlig upphandling. Dock finns det kritik från företagen att ramavtalsupphandlingar är svårvärderade.</p>

Med tanke på att offentlig upphandling är ett mycket stort område, främst med tanke på dess ekonomiska värde, är det viktigt att det finns en väl fungerande konkurrens. Syftet med uppsatsen är att se hur marknaden för offentlig upphandling påverkas av ett större deltagande av SME-företag, vilka möjligheter finns att påverka konkurrensen och hur upplever SME-företagen upphandlingsprocessen.   Vi tog en initial kontakt med Svenskt Näringsliv som gav oss information och hjälpte till med avgränsningarna. Tillvägagångssättet i uppsatsen kan sägas tillhöra en abduktivt tillvägagångssätt. Valet gjordes att använda kvalitativ metod och därmed bestod empirinsamlingen av intervjuer med två personer från kommunen och tre företag som deltar vid offentlig upphandling. Därefter började vi jämföra teori med empiri. Utifrån detta har vi svarat på vår frågeställning.   De slutsatser vi dragit i vår uppsats är att inom tjänstesektorn torde företagen ha likartade förutsättningar att delta vid upphandlingar, framför allt genom att många konsultuppdrag upphandlas. Det område som kan anses minst jämlik mellan SME-företag och stora företag är byggentreprenader där det av naturliga skäl blir svårt för mindre företag att vara med och lämna anbud. Här skulle vi vilja se ett ökat användande av kombinatorisk upphandling för att underlätta för SME-företag att lämna anbud och därmed öka konkurrensen på marknaden. Det vi fått fram är att myndigheterna kan göra förfrågningsunderlagen tydligare och dela upp upphandlingarna i mindre delar, för att ytterligare öka konkurrensen.   Intervjuerna med företagen har gett oss att det inte tycker anser att det finns några särskilt krångliga moment vid offentlig upphandling. Samtidigt har dessa företag varit med ganska länge och lämnat anbud vid offentlig upphandling vilket medför att de har byggt upp vissa rutiner för att underlätta det administrativa arbetet vid offentlig upphandling. Dock finns det kritik från företagen att ramavtalsupphandlingar är svårvärderade.

Mjukvarutestning har, sedan introduktionen av datorer, varit föremål för forskning. Idag, när datorer och mikroprocessorer alltmer integreras i produkter som omger oss i vårt dagliga liv, så ökar vikten av effektiv och korrekt mjukvarutestning. Tidigare forskning visar att utforskande testning är en effektiv metod för att upptäcka programvarubuggar. Men, med tids- och resursaspekterna i åtanke finns det andra metoder som kan vara effektivare. En möjlig sådan metod är parvis testning. Litteraturen visar att även denna metod har bra potential för att kunna identifiera programvarubuggar. Det finns dock inte så mycket forskning om jämförelsen av dessa två metoder, vilket är anledningen till att denna studie genomfördes. Denna förklarande fallstudie utvärderar hur utforskande testning presterar jämfört med parvis testning. Aspekter som beaktades i utvärderingsprocessen var antalet upptäckta defekter, allvarlighetsgraden av de hittade defekterna och vilka typer av defekter som hittades. Data samlades in genom undersökningar, intervjuer, deltagande observationer och direkta observationer. Med all denna data som samlats in, drogs slutsatsen att svaret på denna rapports forskningsfrågor är tvetydiga. Det finns fördelar med båda teknikerna, och beroende på förutsättningarna för utforskande testning så kan parvis testning prestera likvärdigt. En sak märktes dock under studien som inte var en del av den ursprungliga omfattningen, och det var styrkan som utforskande testning har som ett läroverktyg. / Software testing has been a subject of research since the introduction of computers. Today, when computers and microprocessors are increasingly integrated into the products surrounding us in our daily lives, the importance of effective and accurate software testing increases. Previous research shows that exploratory testing is an effective method for detecting software bugs. Still, with the time and resource aspects considered, there are other potentially more time and resource-effective methods. One such possible method is the pairwise testing method. The literature also shows that this method is effective for finding software bugs. There is, however, not that much research about the comparison of these two methods, which is why this study was conducted. This explanatory case study evaluates how exploratory testing performs compared with pairwise testing. Aspects considered in the evaluation process were the number of detected defects, the severity distribution of the found defects, and what types of defects were found. The data was collected through surveys, interviews, participant observations, and direct observations. With the data collected, it was concluded that the answers to the research questions of this study are ambiguous. There are benefits with both of the techniques, and depending on the exploratory testing conditions, the pairwise technique can perform comparably as the exploratory testing. However, one thing noticed during the study that was not part of the original scope was the strength of exploratory testing as a learning tool. Lastly, some hypotheses were stated, supported by the collected data.

Unmanned flying vehicles (UAVs) are tools that can be used in a variety of scenarios. The most common areas of application are outdoors, where there are not many obstacles to take into consideration when planning a route. In indoor scenarios, the requirements on the path planning system of the UAV becomes stricter, as these scenarios tend to contain more obstacles compared to flying at higher altitude outdoors. Considering a drone with multiple objectives (waypoints to visit), two problems initially come to mind, namely path planning and combinatorial optimization. To finish the objectives in the most effective way, the optimal path between the waypoints needs to be calculated, as well as the order in which the waypoints need to be visited. Another challenge is the fact that the UAV runs on limited battery capacity, and thus might not be able to finish the objectives before running out of battery. Therefore, the combinatorial optimization needs to include visits to a recharging station. The objective of this thesis is to combine and modify methods for path planning and combinatorial optimization in a way that a route can be calculated within a limited time budget, to allow the computation to be executed “on the fly”. The method used for path planning is ANYA, and the two methods used for the combinatorial optimization are ant colony optimization (ACO) as well as the Lin-Kernighan-Helsgaun (LKH) method. The nearest neighbor method (NN) will be used as a baseline for comparison. We propose an algorithm to include the battery constraint in the optimization. To evaluate the algorithms, we measure the computational time, to know if the method works in real-time, and also the estimated time for the UAV to finish the route, which will determine the energy efficiency of the route. We find that the ACO’s solutions improve over time, but require a long computational time, which makes it not suitable for small time budgets. LKH produces better routes than the NN method, and does so within the chosen time budget, as long as the number of waypoints is limited. The algorithm to optimize the trips to the recharging station works better than the previous use of LKH for this specific problem. / Obemannade flygande fordon är verktyg som är användbara inom en mängd områden. Vanligaste miljön för användning av dessa verktyg är i utomhusmiljöer där inte många fysiska hinder existerar. I inomhusscenarion blir kraven på vägplanering större, då dessa miljöer ofta innehåller fler hinder än vid flygning på högre altituder utomhus. Givet ett scenario med en drönare med flera målpunkter att besöka, finns två stora utmaningar, nämligen vägplanering och ruttplanering. För att besöka alla målpunkter behöver vi en metod för att identifiera närmsta, kollisionsfria vägen mellan målpunkterna, men också en metod för att hitta den optimala ordningen att besöka punkterna i. En annan utmaning som uppstår på grund av drönarens begränsade batteritid är att det inte finns någon garanti på att den hinner besöka alla målpunkter innan batteriet tar slut. Därför måste ruttplaneringen innefatta besök till en laddningsstation. Målet med detta examensarbete är att kombinera och modifiera metoder för väg och ruttplanering på ett sätt så en effektiv rutt mellan alla målpunkter kan identifieras, utan att drönaren får slut på batteri, samt med kravet att metoden ska kunna hitta en lösning inom begränsad tid. Metoden som används för vägplanering är ANYA, och de två metoderna som används för ruttplanering är myrkolonioptimering och Lin-Kernighan-Helsgaun-metoden. Närmsta-granne-metoden kommer användas som en baseline för jämförelsen mellan metoderna. Vi föreslår en algoritm som inkluderar batteribegränsningen i ruttplaneringen. För att utvärdera algoritmerna mäter vi beräkningstiden, för att ta reda på om metoden fungerar i realtid. Vi mäter även den uppskattade tiden det tar för drönaren att slutföra rutten, vilket kommer beskriva hur energieffektiv rutten är. Vi finner att myrkolonioptimering ger en bättre och bättre lösning över tid, men kräver en lång beräkningstid, vilket gör den opassande för korta tidsbegränsningar. LKH producerar bättre rutter än närmsta-granne-metoden, och gör det inom den givna tidsramen, så länge antal målpunkter är begränsade. Algoritmen för att optimera besöken till laddstationen fungerar bättre än tidigare appliceringar av LKH på samma problem.

No description available.

Combinatorial optimization include such tasks as finding the quickest route to work, scheduling jobs to specialists, and placing bus stops so as to minimize commuter times. We consider problems where one is given a collection of constraints with the objective of finding an assignment satisfying as many constraints as possible, also known as Constraint Satisfaction Problems (CSPs). Most CSPs are NP-hard to solve optimally and we turn to approximations - a solution is said to be a factor-c approximation if its satisfies at least c times the optimal number of constraints. This thesis presents new results on the approximation limits of CSPs in various settings. In ordering CSPs, one is given constraints which specify the relative order of items, and the objective is order the items so as to satisfy as many constraints as possible. We give improved approximation hardness results for two classical problems: it is NP-hard to approximate Maximum Acyclic Subgraph with a factor better than 14/15 and Maximum Betweenness with a factor better than 1/2. We present ordering problems which are NP-hard to approximate better than random assignments, and that there are ordering problems arbitrarily hard to approximate. Next, Gaussian elimination can efficiently find exact solutions for satisfiable collections of so-called parity constraints. We show that whenever constraints accept at least one assignment in addition to a parity, then the problem is NP-hard to approximate better than random assignments. Finally, we study the uselessness property which basically states that if one is given a collection where almost all constraints are simultaneously satisfiable and one is permitted to relax the constraints to accept or reject additional assignments, then it is still NP-hard to find solutions noticeably better than random assignments. We consider the setting where all variables appear unnegated and provide the first examples of non-trivially useless predicates assuming only P != NP. / Kombinatoriska optimering inkluderar naturliga uppgifter såsom att hitta den snabbaste vägen till sitt arbetet, att schemalägga jobb hos specialister, eller att placera hållplatser för att minimera resenärers restid.Vi begränsar vi oss till de problem i vilket man ges en samling vilkor på variablermed målet att hitta en tilldelning av variablerna uppfyllandes så många som möjligt av vilkoren;så kallade Vilkorsuppfyllningsproblem (eng: Constraint Satisfaction Problems, CSPs).De flesta CSPs är NP-svåra att lösa optimalt och vi beaktar istället approximationer. Specifikt kallas, för 0 &lt;= c &lt;= 1, en lösning för en faktor-c approximation om antalet vilkor uppfyllda av lösningen är minst cgånger det största antalet uppfyllda av någon läsning. Denna avhandling består av tre artiklar som presenterar nya resultat begränsande hurpass väl man kan approximera CSPs i diverse situationer.För paritetsvilkor är en samling konsistenta vilkor enkla att lösa genom Gausselimination. Vi visar att för samtliga vilkor som uppfylls av en paritet och åtminstonde en ytterliggare tilldelning så är det inte bara NP-svårt at lösa utan till och med att ge en icke-trivial approximation.Oanvändarbarhet är en stark svårighetsegenskap som i princip säger att det är NP-svårt att ge icke-triviala approximationer även när man gemensamt för alla vilkor får ändra vad som uppfyller dem eller inte. Vi ger de första exemplen på icke-trivialt oanvändbara vilkor utan negationer betingat endast på P != NP.Vi visar på approximerbarhet för diverse ordningsvilorsproblem. I dessa ges man vilkor på hur objekt ska vara ordnade relativt varandra och målet är att hitta en ordning som uppfyller så många av vilkoren som möjligt. Vi ger bättre svårighetsresultat för de två mest välkända ordningsproblem, visar att det finns problem där det är NP-svårt att approximera bättre än triviala strategier, och att det finns ordningsproblem där godtyckligt dåliga approximationsgarantier är NP-svåra. / <p>NADA är en delad institution mellan SU och KTH där senare nu kallar den CSC.</p> / ApproxNP

This master's thesis investigates the application of Graph Neural Networks (GNNs) to address scalability challenges in combinatorial optimization, with a primary focus on the minimum Total Dominating set Problem (TDP) and additionally the related Carrier Scheduling Problem (CSP) in networks of Internet of Things. The research identifies the NP-hard nature of these problems as a fundamental challenge and addresses how to improve predictions on input graphs of sizes much larger than seen during training phase. Further, the thesis explores the instability in such scalability when leveraging GNNs for TDP and CSP. Two primary measures to counter this scalability problem are proposed and tested: incorporating node degree as an additional feature and modifying the attention mechanism in GNNs. Results indicate that these countermeasures show promise in addressing scalability issues in TDP, with node degree inclusion demonstrating overall performance improvements while the modified attention mechanism presents a nuanced outcome with some metrics improved at the cost of others. Application of these methods to CSP yields bleak results, evincing the challenges of scalability in more complex problem domains. The thesis contributes by detecting and addressing scalability challenges in combinatorial optimization using GNNs and provides insights for further research in refining methodologies for real-world applications. / Denna masteruppsats undersöker tillämpningen av Grafiska Neurala Nätverk (GNN) för att hantera utmaningar inom skalbarhet vid kombinatorisk optimering, med ett primärt fokus på minimum Total Dominating set Problem (TDP) samt även det relaterade Carrier Scheduling Problem (CSP) i nätverk inom Internet of Things. Studien identifierar den NP-svåra karaktären av dessa problem som en grundläggande utmaning och lyfter hur man kan förbättra prediktioner på indatagrafer av storlekar som är mycket större än vad man sett under träningsfasen. Vidare utforskar uppsatsen instabiliteten i sådan skalbarhet när man utnyttjar GNN för TDP och CSP. Två primära åtgärder mot detta skalbarhetsproblem föreslås och testas: inkorporering av nodgrad som ett extra attribut och modifiering av attention-mekanismer i GNN. Resultaten indikerar att dessa motåtgärder har potential för att angripa skalbarhetsproblem i TDP, där inkludering av nodgrad ger övergripande prestandaförbättringar medan den modifierade attention-mekanismen ger ett mer tvetydigt resultat med vissa mätvärden förbättrade på bekostnad av andra. Tillämpning av dessa metoder på CSP ger svaga resultat, vilket antyder om utmaningarna med skalbarhet i mer komplexa problemdomäner. Uppsatsen bidrar genom att upptäcka och adressera skalbarhetsutmaningar i kombinatorisk optimering med hjälp av GNN och ger insikter för vidare forskning i att förfina metoder för verkliga tillämpningar.

In route planning the goal is to obtain the best route between a set of locations, which becomes a very complex task as the number of locations increase. This study will consider the problem of transfer bus route planning and examines the feasibility of applying a reinforcement learning method in this specific real-world context. In recent research, reinforcement learning methods have emerged as a promising alternative to classical optimization algorithms when solving similar problems. This due to their positive properties in terms of scalability and generalization. However, the majority of said research has been performed on strictly theoretical problems, not using real-world data. This study implements an existing reinforcement learning model and adapts it to fit the realms of transfer bus route planning. The model is trained to generate optimized routes in terms of time and cost consumption. Then, routes generated by the trained model are evaluated by comparing them to corresponding manually planned routes. The reinforcement learning model produces routes that outperforms manually planned routes with regards to both examined metrics. However, due to delimitations and assumptions made during the implementation, the explicit differences in consumptions are considered promising but cannot be taken as definite results. The main finding is the overarching behavior of the model, implying a proof of concept; reinforcement learning models are usable tools in the context of real-world transfer bus route planning. / Inom ruttplanering är målet att erhålla den bästa färdvägen mellan en uppsättning platser, vilket blir en mycket komplicerad uppgift i takt med att antalet platser ökar. Denna studie kommer att behandla problemet gällande ruttplanering av transferbussar och undersöker genomförbarheten av att tillämpa en förstärkningsinlärningsmetod på detta verkliga problem. I nutida forskning har förstärkningsinlärningsmetoder framträtt som ett lovande alternativ till klassiska optimeringsalgoritmer för lösandet av liknande problem. Detta på grund utav deras positiva egenskaper gällande skalbarhet och generalisering. Emellertid har majoriteten av den nämnda forskningen utförts på strikt teoretiska problem. Denna studie implementerar en befintlig förstärkningsinlärningsmodell och anpassar den till att passa problemet med ruttplanering av transferbussar. Modellen tränas för att generera optimerade rutter, gällande tids- och kostnadskonsumtion. Därefter utvärderas rutterna, som genererats av den tränade modellen, mot motsvarande  manuellt planerade rutter. Förstärkningsinlärningsmodellen producerar rutter som överträffar de manuellt planerade rutterna med avseende på de båda undersökta mätvärdena. På grund av avgränsningar och antagandet som gjorts under implementeringen anses emellertid de explicita konsumtionsskillnaderna vara lovande men kan inte ses som definitiva resultat. Huvudfyndet är modellens övergripande beteende, vilket antyder en konceptvalidering; förstärkningsinlärningsmodeller är användbara som verktyg i sammanhanget gällande verklig ruttplanering av transferbussar.

Recently, Udwani defined a new class of set functions under monotonicity and subadditivity, called submodular order functions, which is a subfamily of submodular functions. Informally, the submodular order function admits a very limited form of submodularity which is defined over a specific permutation of the ground set. His work pointed out the intriguing connection between streaming submodular maximization and submodular order maximization. Inspired by a 0.25-approximation streaming algorithm for maximizing a monotone submodular function subject to a matroid constraint, Udwani gave a 0.25-approximation algorithm for submodular order functions maximization subject to a matroid constraint. Based on the above results, we would like to explore further in which cases it is feasible to generalize from streaming submodular maximization algorithms to submodular order maximization algorithms. As a more general constraint than matroid, p-matchoid is a collection of p matroids with each matroid defined on some subsets of the ground set. Related work gave a 1/4p-approximation streaming algorithm for monotone submodular functions maximization under a p-matchoid constraint. Inspired by the above algorithms and the intriguing connection, we used some techniques to try to generalize several streaming algorithms for submodular functions to the offline algorithms for submodular order functions, including interleaved partitions and incremental values. Assuming that the objective function f is subadditive and non-negative, we gave a 1/4p-approximation algorithm for monotone submodular order maximization to a p-matchoid constraint. In addition, we summarize the failures of other cases. / Nyligen definierade Udwani en ny klass av mängdfunktioner under monotonicitet och subadditivitet, som kallas submodulära ordningsfunktioner och som är en underfamilj av submodulära funktioner. Informellt sett medger den submodulära ordningsfunktionen en mycket begränsad form av submodularitet som är definierad över en specifik permutation av grundmängden. Hans arbete pekade på det spännande sambandet mellan strömmande submodulär maximering och submodulär ordermaximering. Inspirerad av en strömningsalgoritm med 0.25-approximation för maximering av en monoton submodulär funktion som är föremål för en matroidbegränsning, gav Udwani en algoritm med 0.25-approximation för maximering av submodulära ordningsfunktioner som är föremål för en matroidbegränsning. Baserat på ovanstående resultat skulle vi vilja utforska ytterligare i vilka fall det är möjligt att generalisera från algoritmer för strömning av submodulära maximeringsfunktioner till algoritmer för maximering av submodulära orderfunktioner. Som en mer allmän begränsning än matroid är p-matchoid en samling av p matroider där varje matroid definieras på vissa delmängder av grundmängden. Relaterade arbeten gav en strömmingsalgoritm med 1/4p-tillnärmning för monoton submodulär funktionsmaximering under en p-matchoid-begränsning. Inspirerade av ovanstående algoritmer och det spännande sambandet använde vi vissa tekniker för att försöka generalisera flera strömningsalgoritmer för submodulära funktioner till offline-algoritmer för submodulära ordningsfunktioner, inklusive interleaved partitions och inkrementella värden. Under förutsättning att målfunktionen f är subadditiv och icke-negativ gav vi en algoritm för 1/4p-tillnärmning för monoton submodulär ordermaximering till ett p-matchoid-begränsningsvillkor. Dessutom sammanfattar vi misslyckanden i andra fall.