Problem med maximal tillfredsställelse

I beräkningskomplexitetsteorin är problemet med maximal tillfredsställelse ( MAX-SAT ) problemet med att bestämma det maximala antalet satser, av en given boolesk formel i konjunktiv normal form , som kan göras sant genom en tilldelning av sanningsvärden till variablerna för formeln. Det är en generalisering av det booleska tillfredsställbarhetsproblemet , som frågar om det finns en sanningstilldelning som gör alla satser sanna.

Exempel

Formeln för konjunktiv normalform

är inte tillfredsställande: oavsett vilka sanningsvärden som tilldelas dess två variabler, kommer åtminstone en av dess fyra satser att vara falsk. Det är dock möjligt att tilldela sanningsvärden på ett sådant sätt att tre av fyra satser blir sanna; verkligen, varje sanningsuppdrag kommer att göra detta. Därför, om denna formel ges som en instans av MAX-SAT-problemet, är lösningen på problemet siffran tre.

Hårdhet

MAX-SAT-problemet är NP-hårt , eftersom dess lösning lätt leder till lösningen av det booleska tillfredsställbarhetsproblemet, som är NP-komplett .

Det är också svårt att hitta en ungefärlig lösning på problemet, som uppfyller ett antal klausuler inom ett garanterat approximationsförhållande för den optimala lösningen. Mer exakt är problemet APX -komplett och tillåter således inte ett polynom-tidsapproximationsschema om inte P = NP.

Viktad MAX-SAT

Mer generellt kan man definiera en viktad version av MAX-SAT enligt följande: givet en konjunktiv normalformsformel med icke-negativa vikter tilldelade varje sats, hitta sanningsvärden för dess variabler som maximerar den kombinerade vikten av de nöjda satserna. MAX-SAT-problemet är en instans av viktad MAX-SAT där alla vikter är 1.

Approximationsalgoritmer

1/2-ungefär

Att slumpmässigt tilldela varje variabel att vara sann med sannolikhet 1/2 ger en förväntad 2-approximation . Mer exakt, om varje sats har minst k variabler, ger detta en (1 − 2 k )-approximation. Denna algoritm kan avrandomiseras med metoden för villkorade sannolikheter .

(1-1/ e )-approximation

MAX-SAT kan också uttryckas med ett linjärt heltalsprogram (ILP). Fixa en konjunktiv normalformformel F med variabler x 1 , x 2 , ..., x n , och låt C beteckna satserna i F . Låt S + c och S c för varje sats c i C beteckna de mängder av variabler som inte är negerade i c , respektive de som är negerade i c . Variablerna y x i ILP kommer att motsvara variablerna i formeln F , medan variablerna z c kommer att motsvara satserna. ILP är följande:

maximera (maximera vikten av de uppfyllda klausulerna)
föremål för för alla (satsen är sann om den har en sann, icke-negerad variabel eller en falsk, negerad)
för alla . (varje klausul är antingen uppfylld eller inte)
för alla . (varje variabel är antingen sann eller falsk)

Ovanstående program kan avslappnas till följande linjära program L :

maximera (maximera vikten av de uppfyllda klausulerna)
föremål för för alla (satsen är sann om den har en sann, icke-negerad variabel eller en falsk, negerad)
för alla .
för alla .

Följande algoritm som använder den avslappningen är en förväntad (1-1/ e )-approximation:

  1. Lös det linjära programmet L och få en lösning O
  2. Ställ in variabel x att vara sann med sannolikheten y x där y x är värdet som ges i O .

Denna algoritm kan också avrandomiseras med metoden för villkorade sannolikheter.

3/4-uppskattning

Algoritmen för 1/2-approximation fungerar bättre när satser är stora medan (1-1/ e )-approximation fungerar bättre när satser är små. De kan kombineras enligt följande:

  1. Kör den (avrandomiserade) 1/2-approximationsalgoritmen för att få en sanningsuppgift X .
  2. Kör (avrandomiserad) (1-1/e)-approximation för att få en sanningsuppgift Y .
  3. Utdata beroende på vilket av X eller Y som maximerar vikten av de uppfyllda klausulerna.

Detta är en deterministisk faktor (3/4)-approximation.

Exempel

På formeln

där , kommer (1-1/ e )-approximationen att sätta varje variabel till True med sannolikhet 1/2, och kommer därför att bete sig identiskt med 1/2-approximationen. Om man antar att tilldelningen av x väljs först under avrandomiseringen, kommer de avrandomiserade algoritmerna att välja en lösning med totalvikten medan den optimala lösningen har vikten .

Lösare

Många exakta lösare för MAX-SAT har utvecklats under de senaste åren, och många av dem presenterades i den välkända konferensen om det booleska tillfredsställbarhetsproblemet och relaterade problem, SAT-konferensen. 2006 var SAT-konferensen värd för den första MAX-SAT-utvärderingen som jämförde prestandan för praktiska lösare för MAX-SAT, som den har gjort tidigare för problemet med pseudo-boolesk tillfredsställelse och det kvantifierade booleska formelproblemet . På grund av dess NP-hårdhet kan stora MAX-SAT-instanser i allmänhet inte lösas exakt, och man måste ofta tillgripa approximationsalgoritmer och heuristik

Det finns flera lösare som skickats till de senaste Max-SAT-utvärderingarna:

  • Branch and Bound baserat: Clone, MaxSatz (baserat på Satz ), IncMaxSatz, IUT_MaxSatz, WBO, GIDSHSat.
  • Tillfredsställelsebaserad: SAT4J, QMaxSat.
  • Otillfredsställelsebaserad: msuncore, WPM1, PM2.

Speciella fall

MAX-SAT är en av optimeringsutvidgningarna av det booleska tillfredsställbarhetsproblemet , vilket är problemet med att avgöra om variablerna för en given boolesk formel kan tilldelas på ett sådant sätt att formeln utvärderas till TRUE. Om satserna är begränsade till att ha högst 2 literaler, som i 2-satisfiability , får vi MAX-2SAT- problemet. Om de är begränsade till högst 3 literaler per sats, som i 3-satisfiability , får vi MAX-3SAT- problemet.

Relaterade problem

Det finns många problem relaterade till tillfredsställelsen av konjunktiva booleska formler i normalform.

  • Beslutsproblem :
  • Optimeringsproblem, där målet är att maximera antalet uppfyllda klausuler:
    • MAX-SAT, och motsvarande viktade version Weighted MAX-SAT
    • MAX -k SAT, där varje sats har exakt k variabler:
    • Problemet med partiell maximal tillfredsställelse (PMAX-SAT) frågar efter det maximala antalet satser som kan uppfyllas av vilken som helst tilldelning av en given delmängd av satser. Resten av klausulerna måste vara uppfyllda.
    • Problemet med mjuk tillfredsställelse (soft-SAT), givet en uppsättning SAT-problem, frågar efter det maximala antalet av dessa problem som kan tillgodoses av vilken som helst tilldelning.
    • Minsta tillfredsställelseproblem.
  • MAX-SAT-problemet kan utvidgas till det fall där variablerna för begränsningstillfredsställelseproblemet tillhör uppsättningen av reella. Problemet är att hitta den minsta q så att den q - avslappnade skärningspunkten mellan begränsningarna inte är tom.

Se även

externa länkar

  1. ^ Markera Krentel. Optimeringsproblemens komplexitet . Proc. av STOC '86. 1986.
  2. ^ Christos Papadimitriou. Beräkningskomplexitet. Addison-Wesley, 1994.
  3. ^ Cohen, Cooper, Jeavons. En fullständig karaktärisering av komplexitet för problem med boolesk begränsningsoptimering . CP 2004.
  4. ^ Vazirani 2001 , sid. 131.
  5. ^    Borchers, Brian; Furman, Judith (1998-12-01). "En tvåfasig exakt algoritm för MAX-SAT- och viktade MAX-SAT-problem". Journal of Combinatorial Optimization . 2 (4): 299-306. doi : 10.1023/A:1009725216438 . ISSN 1382-6905 . S2CID 6736614 .
  6. ^   Du, Dingzhu; Gu, Jun; Pardalos, Panos M. (1997-01-01). Tillfredsställelseproblem: Teori och tillämpningar: DIMACS Workshop, 11-13 mars 1996 . American Mathematical Soc. sid. 393. ISBN 9780821870808 .
  7. ^ Vazirani 2001 , Lemma 16.2.
  8. ^ Vazirani 2001 , avsnitt 16.2.
  9. ^ Vazirani , sid. 136.
  10. ^ Vazirani 2001 , sats 16.9.
  11. ^ Vazirani 2001 , Exempel 16.11.
  12. ^ R. Battiti och M. Protasi. Approximate Algorithms and Heuristics for MAX-SAT Handbook of Combinatorial Optimization, Vol 1, 1998, 77-148, Kluwer Academic Publishers.
  13. ^ Josep Argelich och Felip Manyà. Exakta Max-SAT-lösare för alltför begränsade problem . I Journal of Heuristics 12(4) s. 375-392. Springer, 2006.
  14. ^ Jaulin, L.; Walter, E. (2002). "Garanterat robust olinjär minimaxuppskattning" (PDF) . IEEE-transaktioner på automatisk kontroll . 47 (11): 1857–1864. doi : 10.1109/TAC.2002.804479 .