{"id":498,"date":"2023-02-06T20:10:53","date_gmt":"2023-02-06T20:10:53","guid":{"rendered":"https:\/\/solinfo.ro\/blog\/?p=498"},"modified":"2024-05-17T20:31:18","modified_gmt":"2024-05-17T20:31:18","slug":"grafuri-orientate-problema-2sat-problema-satisfiabilitatii","status":"publish","type":"post","link":"https:\/\/solinfo.ro\/blog\/grafuri-orientate-problema-2sat-problema-satisfiabilitatii\/","title":{"rendered":"Grafuri orientate – problema 2SAT (problema satisfiabilit\u0103\u0163ii)"},"content":{"rendered":"\n

Problema satisfiabilit\u0103\u021bii, prescurtat\u0103 cu SAT (satisfiability), presupune existen\u021ba unei atribuiri satisfiabile pentru o expresie boolean\u0103. O atribuire de valori booleene pentru o expresie se nume\u0219te „atribuire satisfiabil\u0103” dac\u0103 rezultatul expresiei, dup\u0103 atribuirea valorilor, este „adev\u0103rat”. De exemplu, expresia (x1<\/em> -> x2<\/em>) \u2227<\/strong> (~x3<\/em> -> x4<\/em>)<\/strong> este satisfiabil\u0103, pentru x1<\/em> =1, x2<\/em> = 1, x3<\/em> = 0, x4 <\/em>= 1. <\/p>\n\n\n\n

Folosind urm\u0103toarele echivalen\u021be logice<\/a>, o expresie poate fi simplificat\u0103 pentru a ob\u021bine forma normal conjunctiv\u0103<\/a>, adic\u0103 o conjunc\u021bie („\u2227” = AND gate) de propozi\u021bii <\/em>\u00een care fiecare propozi\u021bie este o disjunc\u021bie („\u2228” = OR gate) de literali. Deci, expresia de mai sus poate fi transformat\u0103 \u00een: (~x1<\/em> \u2228 x2<\/em>) \u2227 (x3<\/em> \u2228<\/strong> x4<\/em>).<\/strong><\/p>\n\n\n\n

A\u0219adar, este suficient s\u0103 studiem doar forma normal conjunctiv\u0103. \u00cen continuare, vom rezolva problema clasic\u0103 de pe infoarena<\/a>.<\/p>\n\n\n\n

<\/p>\n\n\n\n

Vom pleca de la urm\u0103toarea informa\u021bie: x \u2228 y = (~x -> y) \u2227<\/strong> (~y -> x)<\/strong><\/em> \u0219i de la tabelul pentru implica\u021bie, care arat\u0103 \u00een felul urm\u0103tor:<\/p>\n\n\n\n

\"\"<\/figure>\n\n\n\n

Deoarece forma normal conjunctiv\u0103, pe care noi o analiz\u0103m, este format\u0103 din conjuc\u021bii de propozi\u021bii \u0219i dorim ca rezultatul expresiei s\u0103 fie „adev\u0103rat”, fiecare dintre aceste propozi\u021bii (disjunc\u021bii de literari) trebuie s\u0103 fie la r\u00e2ndul ei adev\u0103rat\u0103. Pentru ca o propozi\u021bie de forma x \u2228 y<\/em><\/strong> s\u0103 fie adev\u0103rat\u0103, trebuie ca (~x -> y) \u2227<\/strong> (~y -> x)<\/strong> <\/em>(forma echivalent\u0103 de mai sus) s\u0103 fie adev\u0103rat\u0103. Vom trata implica\u021bia ca fiind o muchie \u00eentr-un graf orientat de la ~x<\/em> la y<\/em>, respectiv de la ~y <\/em>la x<\/em>. Scopul este s\u0103 ar\u0103t\u0103m c\u0103 ~x<\/em> NU<\/strong> este accesibil din x<\/em>, deci s\u0103 NU<\/strong> existe drum de la x<\/em> la ~x<\/em>, adic\u0103 x<\/em> \u0219i ~x<\/em> s\u0103 NU<\/strong> fac\u0103 parte din aceea\u0219i component\u0103 tare conex\u0103<\/em>. Dorim s\u0103 demonstr\u0103m acest lucru datorit\u0103 tabelului de implica\u021bie. Dac\u0103 ~x<\/em> ar fi accesibil din x<\/em>, ar \u00eensemna c\u0103 x<\/em> implic\u0103 ~x,<\/em> iar pentru x<\/em> = 1, acest lucru se traduce prin „1 implic\u0103 (->) 0”, lucru fals.<\/strong><\/p>\n\n\n\n

<\/p>\n\n\n\n

\"\"
Exemplu de graf ob\u021binut (surs\u0103: https:\/\/infoarena.ro\/2-sat)<\/figcaption><\/figure>\n\n\n\n

<\/p>\n\n\n\n

Conven\u021bie: pentru un nod x<\/em> (1 \u2264 x<\/em> \u2264 n), ~x<\/em> va fi echivalat cu x + n <\/em>(n + 1 \u2264 ~x<\/em> \u2264 2 * n). Prin urmare, c\u00e2nd vom citi datele de intrare, nodurile cu „-” \u00een fa\u021b\u0103 le vom transforma \u00een -x + n<\/em>. De exemplu, dac\u0103 x = –5<\/em>, acesta \u00eenseamn\u0103 ~5<\/em>, care, conform conven\u021biei, devine -(-5) + n = 5 + n<\/em>. <\/p>\n\n\n\n

Ca s\u0103 determin\u0103m dac\u0103 doua noduri fac parte din aceea\u0219i component\u0103 tare conex\u0103<\/em>, vom p\u0103stra \u00eentr-un vector comp[x] = componenta tare conex\u0103 din care face parte nodul x<\/span><\/em> \u0219i folosim algoritmul lui Sharir-Kosaraju. <\/p>\n\n\n\n

const int NMAX = 2e5;\n\nvector <int> g[NMAX + 1], rg[NMAX + 1], topsort; \/\/ \"g\" = graful original, \"rg\" = graful transpus\nint comp[NMAX + 1], n, ctc;\nbitset <NMAX + 1> viz;\n\nint val_asoc(int x){\n\n    \/\/ deoarece -x corespunde lui ~x, iar noi neg\u0103m un x (<= n) cu x + n, x (< 0) devine echivalent cu -x + n\n\n    if(x < 0)\n        return -x + n;\n\n    return x;\n}   \n\nint neg(int x){\n\n    \/\/ neg\u0103m x in func\u021bie de valorea sa fa\u021b\u0103 de n\n\n    if(x <= n)\n        return x + n;\n    \n    \/\/ ex: dac\u0103 x = -5 \u00eenseamn\u0103 ~5. El se va transforma din cauza nega\u021biei \u00een -(-5) + n = 5 + n, iar ~(~5) = 5, deci\n    \/\/ vom sc\u0103dea n pentru a ob\u021bine rezultatul 5 \n    return x - n;\n}\n\nvoid dfs(int x){\n\n    viz[x] = 1;\n\n    for(auto &y : g[x])\n        if(!viz[y])\n            dfs(y);\n\n    topsort.push_back(x);\n}\n\nvoid dfs2(int x){\n\n    comp[x] = ctc;\n\n    for(auto &y : rg[x])\n        if(!comp[y])\n            dfs2(y);\n\n}\n\nint main(){\n\n    int m = 0;\n    cin >> n >> m;\n\n    for(int i = 0; i < m; i++){\n\n        int x = 0, y = 0;\n        cin >> x >> y;\n\n        x = val_asoc(x);\n        y = val_asoc(y);\n        \n\n        g[neg(x)].push_back(y);\n        g[neg(y)].push_back(x);\n        \n        rg[y].push_back(neg(x));\n        rg[x].push_back(neg(y));\n\n    }\n\n    for(int i = 1; i <= 2 * n; i++)\n        if(!viz[i])\n            dfs(i);\n    \n    reverse(topsort.begin(), topsort.end());\n\n    for(auto &y : topsort){\n\n        if(comp[y])\n            continue;\n\n        ctc++;\n        dfs2(y);\n\n    }<\/pre>\n\n\n\n
Observa\u021bii importante: <\/p>\n\n\n\n
    \n
  1. Dac\u0103 doi literali fac parte din aceea\u0219i component\u0103 tare conex\u0103<\/em>, atunci ei vor avea aceea\u0219i valoare;<\/li>\n\n\n\n
  2. Dac\u0103 exist\u0103 drum de la un nod x<\/em> la un nod y<\/em>, atunci comp[x] \u2264<\/em> comp[y]<\/em>;<\/li>\n<\/ol>\n\n\n\n
    Odat\u0103 construit vectorul comp[]<\/em>, vom verifica daca nodul x<\/em> face parte din aceea\u0219i component\u0103 tare conex\u0103 <\/em>cu ~x<\/em>, caz \u00een care expresia nu este 2SAT.<\/p>\n\n\n\n
        bool _2sat = 1;\n    for(int i = 1; i <= n; i++)\n        if(comp[i] == comp[i + n]) \/\/ i + n = ~i\n            _2sat = 0;\n\n    if(_2sat == 0){\n\n        cout << \"-1\";\n        return 0;\n\n    }<\/pre>\n\n\n\n
    Ce ne mai r\u0103m\u00e2ne de f\u0103cut este s\u0103 atribuim valori literalilor. Pentru orice nod x<\/em>, dac\u0103 comp[x] > comp[~x], <\/em>atunci \u00eel vom seta pe x<\/em> = 1 \u0219i ~x<\/em> = 0, sau, dac\u0103 comp[x] < comp[~x]<\/em>, set\u0103m x<\/em> = 0 \u0219i ~x<\/em> = 1. (!) <\/p>\n\n\n\n
    De ce func\u021bioneaz\u0103? <\/p>\n\n\n\n
    Vom demonstra c\u0103 nu exist\u0103 2 noduri x<\/em> \u0219i y<\/em> astfel \u00eenc\u00e2t x<\/em> = 1, y<\/em> = 0 \u0219i y s\u0103 fie accesibil din x<\/em> (de cazul \u00een care x <\/em>= 1 \u0219i s\u0103 existe un drum de la x<\/em> la ~x<\/em> ne-am ocupat deja, verific\u00e2nd dac\u0103 acestea fac sau nu fac parte din aceea\u0219i component\u0103 tare conex\u0103<\/em>). Presupunem c\u0103 exist\u0103 o pereche (x<\/em>, y<\/em>) de astfel de noduri.<\/p>\n\n\n\n
      \n
    1. (!) => dac\u0103 x<\/em> = 1 => comp[x] > comp[~x];<\/em><\/li>\n\n\n\n
    2. (!) => dac\u0103 y<\/em> = 0 => comp[y] < comp[~y];<\/em><\/li>\n<\/ol>\n\n\n\n
      Dac\u0103 y este accesibil din x, atunci comp[x] \u2264<\/em> comp[y] => comp[~x]  < comp[x] \u2264 comp[y] < comp[~y]<\/em> (din toate cele 3 inegalit\u0103\u021bi). Din moment ce exist\u0103 un drum de la x<\/em> la y<\/em>, atunci exist\u0103 \u0219i un drum de la ~y<\/em> la ~x<\/em> (dac\u0103 x -> y <=> ~y -> ~x), deci comp[~y] \u2264 comp[~x]<\/em> (rela\u021bie datorat\u0103 sort\u0103rii topologice realizate de algoritmul lui Sharir-Kosaraju) – contrar cu ce am scris mai sus. Prin urmare, nu exist\u0103 2 noduri x<\/em> \u0219i y<\/em> astfel \u00eenc\u00e2t x<\/em> = 1, y<\/em> = 0 \u0219i y<\/em> s\u0103 fie accesibil din x<\/em>.<\/p>\n\n\n\n
      <\/p>\n\n\n\n
      for(int i = 1; i <= n; i++)\n    if(comp[i] > comp[i + n])\n         cout << 1 << \" \";\n    else \n         cout << 0 << \" \";<\/pre>\n\n\n\n
      <\/p>\n\n\n\n
      Autor: Pirnog Theodor Ioan<\/p>\n\n\n\n
      Colegiul Na\u021bional „B. P. Hasdeu”, Buz\u0103u<\/p>\n","protected":false},"excerpt":{"rendered":"
      Problema satisfiabilit\u0103\u021bii, prescurtat\u0103 cu SAT (satisfiability), presupune existen\u021ba unei atribuiri satisfiabile pentru o expresie boolean\u0103. O atribuire de valori booleene … <\/p>\n","protected":false},"author":3,"featured_media":506,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[],"class_list":["post-498","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-uncategorized"],"_links":{"self":[{"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/posts\/498","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/users\/3"}],"replies":[{"embeddable":true,"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/comments?post=498"}],"version-history":[{"count":15,"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/posts\/498\/revisions"}],"predecessor-version":[{"id":532,"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/posts\/498\/revisions\/532"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/media\/506"}],"wp:attachment":[{"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/media?parent=498"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/categories?post=498"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/solinfo.ro\/blog\/wp-json\/wp\/v2\/tags?post=498"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}