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.

  • 1
    $\begingroup$ 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. $\endgroup$ – 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).

  • $\begingroup$ 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. $\endgroup$ – 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

  • $\begingroup$ 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. $\endgroup$ – Russell Easterly Aug 24 '14 at 4:27
  • $\begingroup$ @RussellEasterly Not really, this is only true for most solvable instances. $\endgroup$ – Sasho Nikolov Aug 24 '14 at 5:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.