optimeringslogik

Optimeringslogik är ett forskningsområde inom matematikens logik och datorvetenskap som studerar hur optimeringsproblem kan beskrivas och hanteras inom formella språk. Målsättningen är att skriva specifikationer där målfunktionen, begränsningar och preferenser uttrycks tillsammans med logiska villkor om problemets objekt, så att automatiserade metoder kan söka efter bästa lösning under givna villkor.

Formaliseringarna är varierande och inkluderar: utökning av första ordningens logik med optimeringsoperatorer; semiringbaserade mjuka begränsningsramar; optimering under teorier (Optimization Modulo Theories, OMT); samt ansatser inom logikprogrammering och answer-set programming (ASP) med optimeringsuttryck. Dessa ramverk syftar till att kombinera både hårda krav och mjuka kriterier i en enhetlig beskrivning.

Teoretiska frågor inom optimeringslogik rör uttrycksmöjlighet, avgörbarhet och kompleksitet hos språken som används för att beskriva problem, liksom existens och struktur hos optimala modeller. Flera problem studeras också med multiobjektiv optimering, där Pareto-effektivitet eller lexikografisk ordning ger flera alternativa bästa lösningar.

Metoder och verktyg innefattar reducering till SAT/SMT och deras optimeringsvarianter, branch-and-bound-tekniker, samt klassiska metoder från linjär och heltalsprogrammering. Det finns även specialiserade OMT-sökare för att hantera kombinationen av logik och matematiska krav.

Användningar förekommer inom planering, schemaläggning, resursfördelning, konfigurationsproblem, programvaruverifikation och systemsyntes. Optimeringslogik fungerar ofta som en bro mellan teoretisk logik och praktiska beslut.