Max SAT apx

MAX CNF-SAT §

Input: $CNF$ boolean formula (clause lenght not fixed) Goal: find assignment that maximises # of sat clauses

Random assignment algoritm for fixed k §

1. set $x_i=0,1$ with prob. $1/2$ $\forall i$ note: works best with long clauses $P(C_{i}isUNSAT))=1/2^k$ ($k$ number of literals)

2. divide and conquer, finds at leeast $1-1/2^k$ SAT clauses.

LP-relaxation + Randomized Rounding §

1. variabili:

$$\forall i{x}_i\in \{0,1\}\forall C{z}_c\in \{0,1\}$$

2. funzione obj:

$$\max \sum _C{w}_c{z}_C$$

where $w_C$ is a weight, (for max CNFSAT $w_c=1$ ), we get something for free. 3. creare i vincoli:

$$\forall C\sum _{i\in C^{+}}{x}_i+\sum _{i\in C^{-}}(1-x_i)\ge z_c$$

where $C^{+}$ and $C^{-}$ are the set of variables and negated variables of clause $C$ respectivly. 4. rilasso, passo al continuo

$$\forall i{x}_i^{\ast }\in [0,1]\forall C{z}_c^{\ast }\in [0,1]$$

We get a linear programming problem, solvable in P time. Since the serch space of the lineare problem is bigger, the solution is better than the discrete one:

$$LP\ge OPT$$

5. rounding. We do it probabilistically:

$$x_i=\{\begin{array}{l}1\text{ with prob }{x}_i^{\ast }\\ 0\text{ otherwise }\end{array}$$ $${\beta }_k:=(1-1/2^k)$$

expected number of SAT clauese:

$$E[X]=\sum _C{w}_{i}E[C_i]=\sum _C{w}_{c}E[C_i])\sum _C{w}_{c}P[C_i\text{ is SAT}]$$

where $C_i=1,0$ if is SAT or not. (we used linearity and expted of bernoullui random variable).

Pick a clause $C$ with $|C|=k$ literals.

$$P(C\text{ is SAT})\ge {\beta }_k{z}_c^{\ast }$$

in fact:

$$P(C\text{ is SAT})=1-{\Pi }_{i\in C}(1-x_i^{\ast })$$