Aarhus Universitets segl

English

Du er her: AU » Om AU » Organisation » Phase Transitions for the Boolean Satisfaction Problem

Om AU

Phase Transitions for the Boolean Satisfaction Problem

Projekter: Projekt › Forskning

Se relationer på Aarhus Universitet

Beskrivelse

Kunstig intelligens (AI) beskæftiger sig med at gøre maskiner i stand til at foretage "intelligente valg". Indenfor AI-planlægning, der er den gren af kunstig intelligens der vedrører intelligente agenter, autonome robotter og ubemandede køretøjer, bygger de "intelligente valg" på at finde en strategi, der ud fra en beskrivelse af verden, de ønskede mål, og de mulige handlinger, opnår de givne mål. At finde disse strategier er et meget komplekst problem, og det bliver derfor ofte løst ved at transformere problemet til et boolean satisfaction (SAT) problem, som kan løses effektivt ved hjælp af moderne såkaldte SAT solvers. Ved første øjekast er det overraskede, at den overstående metode overhovedet er effektiv, da det forventes at være umuligt at løse SAT problemet i polynomiel tid (dette er den berømte P ≠ NP formodning). På trods af dette kan de SAT problemer der fremkommer i AI-planlægning løses særdeles effektivt; selv høj-dimensionale problemer med mere end 1.000.000 variable. Dette formodes at skyldes, at det kun er en meget lille klasse af SAT problemer, der er svære at løse (kræver eksponentiel tid), og at disse problemer ligger på grænsefladen hvor SAT problemet går fra at være underrestringeret til at være overrestringeret. Formålet med dette projekt er at lave et matematisk bevis for gyldigheden af denne berømte formodning, der er kendt som "the satisfiability conjecture".
StatusIgangværende
Effektiv start/slut dato01/11/2021 → 31/10/2025
Linkshttps://dff.dk/forskningsprojekter?SearchableText=Basse&period%3Alist=f0yb7m7qxl&instrument%3Alist=r7sp31l4c2&filed_method%3Alist=all#go-explore

Links

ID: 229109595