Under Construction

(2-SAT) MINIMUM TWO SATISFIABILITY
Instance: A CNF formula with 2 variables per clause.
          Each variable x has weight W(x)>=0;
Solution: A satisfying set of variables, i.e., A set X of variables
          such that when assigning true to the variables in X and 
          false to the other variables the CNF formula is satisfied.
Measure : W(X) (i.e. Sum {W(x): x in X})

+------------------------------------------------------------------+
|   The "Local-Ratio Theorem" (oriented for 2-SAT)                 |
+------------------------------------------------------------------+
|   If   X is 2-approximation 2SAT w.r.t the weight function W1    |
|   and  X is 2-approximation 2SAT w.r.t the weight function W2    |
|   then X is 2-approximation 2SAT w.r.t the weight function W1+W2 |
+------------------------------------------------------------------+

The main idea is as follows: let x be any variable.
TRUE (x) the set of all variables forced to be true when x= true.
FALSE(x) the set of all variables forced to be true when x= false.
Define W1 s.t. W1<=W and W1(TRUE(x))=W1(FALSE(x))>0.
and W1(y)=0 for all variables nor in TRUE(x) neither in FALSE(x).

Q1: All 2SAT sets are 2-approximations w.r.t W1. Why?

+-----------------------------------------------------------------+
|Before starting verify that the CNF is satisfiable [EvenItaiShamir76].
|Now as long as not all variables got assigned:
|   select non assigned variable x;
|   case:
|      x=true  leads to a contradiction: assign x=false;
|      x=false leads to a contradiction: assign x=true;
|      W(TRUE(x))=0                    : assign x=true;
|      W(FALSE(x))=0                   : assign x=false;
|      Otherwise (the Local-Ratio Step):
|        Find any W1 s.t. W1<=W and W1(TRUE(x))=W1(FALSE(x))>0.
|        W=W-W1;
+-----------------------------------------------------------------+

The above simplifies the "Gusfield and Pitt" algorithm by omitting
the "transitive closure phase". Furthermore,
we (Rawitz and myself) generalized this approach efficiently
to the "Two variable Integer Program" (see 2VIP).