MAX 1 in 2 SAT Algorithm

The maximum satisfiability problem (Max-Sat) is the problem of finding the maximum number of clauses that can be satisified in a Boolean satisfiability instance. The exactly 1 in 2 Sat problem asks, given a set of clauses each with two literals, is there a set of literals such that each clause has exactly one literal from this set.

The Complexity of Making Unique Choices: Approximating 1-in-k SAT by Guruswami and Trevisan gives a method for approximating Max 1 in 2 Sat. They state monotone (no negated literals) Max 1 in 2 Sat "admits an e-approximation in polynomial time".

I would like to find an exact algorithm for the Max monotone 1 in 2 Sat problem.

-
Monotone 1-in-Ek admits an $e$-approximation, but this is interesting only for $k\geq 4$: for $k <4$ a random assignment does better. Monotone 1-in-E2 is MaxCut and admits a $1.138$-approximation given by the Goemans-Williamson algorithm. – Sasho Nikolov Aug 22 '14 at 16:35

A monotone 1-in-2 clause demands that the two variables have different values. Thus, you can model the problem as a graph problem, with one vertex per variable which is to be colored black or white, and an edge for a clause indicating the colors need to be different. Thus, the question is to make the graph bipartite by deleting a minimum number of edges. This is the MaxCut or Edge Bipartization problem. It is NP-hard.

For Edge Bipartization, there is an algorithm that runs fast when few edges need to be deleted. I wrote an implementation for a slightly more general problem described here (source code).

-
Thanks. There is a simple way to transform the monotone Exactly 1 in 3 SAT problem into a max weighted independent set problem. If an instance is solvable then the associated graph can be made bipartite by removing one edge from each clause. I am hoping certain properties of 1 in 3 SAT will make MaxCut easier on these types of graphs. For example, 1 in 3 SAT has powerful reduction rules. – Russell Easterly Aug 24 '14 at 3:20

An exact algorithm for the Max Monotone 1 in 2 Sat problem (i.e., MaxCut) running faster than $2^n$ (about $O(1.8^n)$ time) can be found in Chapter 6 of my PhD thesis, here: http://web.stanford.edu/~rrwill/thesis.pdf

I don't know of another exact algorithm for the problem that improves over exhaustive search on all instances. For sparse instances (with $O(n)$ clauses), Greg Sorkin and his coauthors have a number of algorithmic results. See here: https://sites.google.com/site/gregorysorkin/pubx

-
Thanks. Dimitris Achlioptas has proven the phase transition clause to variable ratio for 1 in 3 SAT is 1/3. Solvable 1 in 3 SAT instances will have associated graphs with low edge to vertices ratios. – Russell Easterly Aug 24 '14 at 4:27
@RussellEasterly Not really, this is only true for most solvable instances. – Sasho Nikolov Aug 24 '14 at 5:54