Search

In this paper, we propose a simple randomized algorithm for the NAE2SAT problem. The analysis of the algorithm uses the theory of symmetric, absorbing random walks. Inasmuch as the NAE2SAT problem is in the complexity class L (Deterministic Logarithmic Space) and L ⊆ P ⊆ RP, the existence of such an algorithm is not surprising. However, the simplicity of our approach and the insights revealed by its analysis make the current study worthwhile. Not-all-equal SAT (NAESAT) is the variant of the satisfiability problem (SAT), in which we are interested in an assignment that satisfies all the clauses, but falsifies at least one literal in each clause. NAESAT is an interesting SAT variant in its own right and has been studied by SAT theoreticians, on account of its connections to the graph colouring problem. It is well-known that the variant of NAESAT with exactly three literals per clause (NAE3SAT) is NP-complete [M.R. Garey and D.S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W. H. Freeman Company, San Francisco, 1979]. Likewise, there seem to be a number of polynomial time algorithms for NAE2SAT as part of algorithm design folklore [D.S. Johnson, Personal Communication]. Here we show that the NAE2SAT problem admits an extremely simple, literal-flipping algorithm, in precisely the same way that 2SAT does. On a satisfiable instance involving n variables, the probability that our algorithm does not find a satisfying assignment is at most 1/24. The randomized algorithm takes O(1) extra space, in the presence of a verifier and provides an interesting insight into checking whether a graph is bipartite. It must be noted that space-parsimonious randomized algorithms for a problem, such as the one proposed in this paper, invariably lead to error-bounded, online algorithms for the same. As part of our analysis, we argue that a restricted variant of NAE2SAT is L-complete. We note that the bounds derived in this paper are sharper than the ones in Papadimitriou [C.H. Papadimitriou, On selecting a satisfying truth assignment, in Proceedings of the 32nd Annual Symposium on Foundations of Computer Science, San Juan, Puerto Rico, 1-4 October 1991, IEEE, ed., IEEE, Washington, DC, 1991, pp. 163-169]. [ABSTRACT FROM AUTHOR]

We contrast the performance of three algorithms for the problem of deciding whether a Partially Clairvoyant real-time system with relative timing constraints, as specified in the E-T-C scheduling framework, has a feasible schedule. In the E-T-C scheduling model, real-time scheduling problems are specified through a specialized class of constraint logic programs (CLPs) called Quantified Linear Programs (QLPs) [Subramani, K., 2003, An analysis of quantified linear programs. In: C.S. Calude (Ed.) Proceedings of the 4th International Conference on Discrete Mathematics and Theoretical Computer Science (DMTCS), volume 2731 of Lecture Notes in Computer Science, July (Springer-Verlag), pp. 265- 277]; thus algorithms for determining the schedulability of instances are procedures to determine the satisfiability of CLPs. Two of these algorithms, viz., the primal algorithm and the dual algorithm have already been discussed in the literature, while a third algorithm called the randomized dual algorithm has been recently proposed [Subramani, K. and Desovski, D. 2005, A new verification procedure for partially Clairvoyant scheduling. Proceedings of the 3rd International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS), October; Subramani, K. and Desovski, D., 2005, Out of order quantifier elimination for standard quantified linear programs, Journal of Symbolic Computation, 40, 1383-1396]. Our experiments demonstrate that the dual-based algorithms (i.e. the dual and the randomized dual) are more effective from an implementational perspective; this is surprising since all three algorithms have the same worst case asymptotic complexity. [ABSTRACT FROM AUTHOR]