9
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • 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, 2014 at 16:35

2 Answers 2

Reset to default
17
$\begingroup$

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).

Improve this answer
$\endgroup$
1
  • $\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, 2014 at 3:20
14
$\begingroup$

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

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

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