›› 2012, Vol. 27 ›› Issue (4): 668-677.doi: 10.1007/s11390-012-1253-9

• Special Section on Theoretical Computer Science • Previous Articles     Next Articles

Satisfiability with Index Dependency

Hong-Yu Liang (梁宏宇) and Jing He (何晶)   

  1. Institute for Interdisciplinary Information Sciences, Tsinghua University, Beijing 100084, China
  • Received:2011-03-07 Revised:2012-03-18 Online:2012-07-05 Published:2012-07-05
  • Supported by:

    This work was supported in part by the National Basic Research 973 Program of China under Grant Nos. 2011CBA00300, 2011CBA00301, and the National Natural Science Foundation of China under Grant Nos. 61033001, 61061130540, 61073174.

We study the Boolean satisfiability problem (SAT) restricted on input formulas for which there are linear arithmetic constraints imposed on the indices of variables occurring in the same clause. This can be seen as a structural counterpart of Schaefer’s dichotomy theorem which studies the SAT problem with additional constraints on the assigned values of variables in the same clause. More precisely, let k-SAT(m,A) denote the SAT problem restricted on instances of k-CNF formulas, in every clause of which the indices of the last k−m variables are totally decided by the first m ones through some linear equations chosen from A. For example, if A contains i3=i1+2i2 and i4=i2−i1+1, then a clause of the input to 4-SAT(2,A) has the form yi1yi2yi1+2i2yi2-i1+1, with yi being xi or xi. We obtain the following results: 1) If m ≥ 2, then for any set A of linear constraints, the restricted problem k-SAT(m,A) is either in P or NP-complete assuming P ≠ NP. Moreover, the corresponding #SAT problem is always #P-complete, and the Max-SAT problem does not allow a polynomial time approximation scheme assuming P ≠ NP. 2) m=1, that is, in every clause only one index can be chosen freely. In this case, we develop a general framework together with some techniques for designing polynomial-time algorithms for the restricted SAT problems. Using these, we prove that for any A, #2-SAT(1,A) and Max-2-SAT(1,A) are both polynomial-time solvable, which is in sharp contrast with the hardness results of general #2-SAT and Max-2-SAT. For fixed k ≥ 3, we obtain a large class of non-trivial constraints A, under which the problems k-SAT(1,A), #k-SAT(1,A) and Max-k-SAT(1,A) can all be solved in polynomial time or quasi-polynomial time.

[1] Cook S A. The complexity of theorem proving procedures. InProc. ACM STOC, May 1971, pp.151-158.

[2] Aspvall B, Plass M F, Tarjan R E. A linear-time algorithmfor testing the truth of certain quantified boolean formulas.Inf. Process. Lett., 1979, 8(3): 121-123.

[3] Valiant L G. The complexity of computing the permanent.Theoret. Comput. Sci., 1979, 8(2): 189-201.

[4] Valiant L G. The complexity of enumeration and reliabilityproblems. SIAM J. Comput., 1979, 8(3): 410-421.

[5] Arora S, Lund C, Motwani R, Sudan M, Szegedy M. Proofverification and the hardness of approximation problems. J.ACM, 1998, 45(3): 501-555.

[6] Hastad J. Some optimal inapproximability results. J. ACM,2001, 48(4): 798-859.

[7] Henschen L, Wos L. Unit refutations and Horn sets. J. ACM,1974, 21(4): 590-605.

[8] Yamasaki S, Doshita S. The satisfiability problem for the classconsisting of Horn sentences and some non-Horn sentences inpropositional logic. Infor. Control, 1983, 59(1-3): 1-12.

[9] Schaefer T J. The complexity of satisfiability problems. InProc. ACM STOC, May 1978, pp.216-226.

[10] Allender E, Bauland M, Immerman N, Schnoor H, Vollmer H.The complexity of satisfiability problems: Refining Schaefer’stheorem. J. Comput. System Sci., 2009, 75(4): 245-254.

[11] Tovey C A. A simplified NP-complete satisfiability problem.Discrete Appl. Math., 1984, 8(1): 85-89.

[12] Kratochvìl J, Savick′y P, Tuza Z. One more occurrence of variablesmakes satisfiability jump from trivial to NP-complete.SIAM J. Comput., 1993, 22(1): 203-210.

[13] Gebauer H, Szab′o T, Tardos G. The local lemma is tight forSAT. In Proc. the 22nd ACM-SIAM Symposium on DiscreteAlgorithms (SODA), Jan. 2011, pp.664-674.

[14] Lichtenstein D. Planar formulae and their uses. SIAM J.Comput., 1982, 11(2): 329-343.

[15] Monien B, Sudborough I H. Bandwidth constrained NPcompleteproblems. In Proc. ACM STOC, May 1981, pp.207-217.

[16] Georgiou K, Papakonstantinou P A. Complexity and algorithmsfor well-structured k-SAT instances. In Proc. the 11thInternational Conference on Theory and Applications of SatisfiabilityTesting (SAT), May 2008, pp.105-118.

[17] Rosen K H. Elementary Number Theory and its Applications(5th Edition), Addison Wesley, 2004.

[18] Borosh I, Flahive M, Rubin D, Treybig B. A sharp boundfor solutions of linear diophantine equations. P. Am. Math.Soc., 1989, 105(4): 844-846.

[19] Borosh I, Flahive M, Treybig B. Small solution of linear Diophantineequations. Discrete Math., 1986, 58(3): 215-220.

[20] Bradley G H. Algorithms for Hermite and Smith normal matricesand linear diophantine equations. Math. Comput.,1971, 25(116): 897-907.
No related articles found!
Full text



[1] Zhang Zhongyun; Li Guojie;. Optimal Partitioning and Granularity of Uniform Task Graphs[J]. , 1991, 6(2): 185 -194 .
[2] Zong Chengqing; Chen Zhaoxiong; Huang Heyan;. Parsing with Dynamic Rule Selection[J]. , 1997, 12(1): 90 -96 .
[3] Ian Foster. Globus Toolkit Version 4: Software for Service-Oriented Systems[J]. , 2006, 21(4): 513 -520 .
[4] Jun Zhang, Zhao-Hui Peng, Shan Wang, and Hui-Jing Nie. CLASCN: Candidate Network Selection for Efficient Top-k Keyword Queries over Databases[J]. , 2007, 22(2): 197 -207 .
[5] Kai Dong, Tao Gu, Xian-Ping Tao, Jian Lv. Complete Bipartite Anonymity for Location Privacy[J]. , 2014, 29(6): 1094 -1110 .
[6] Wen-Qian Deng, Xue-Mei Li, Xifeng Gao, Cai-Ming Zhang. A Modified Fuzzy C-Means Algorithm for Brain MR Image Segmentation and Bias Field Correction[J]. , 2016, 31(3): 501 -511 .
[7] Chuang-Ye Zhang, Yan Niu, Tie-Ru Wu, Xi-Ming Li. Color Image Super-Resolution and Enhancement with Inter-Channel Details at Trivial Cost[J]. Journal of Computer Science and Technology, 2020, 35(4): 889 -899 .
[8] Lie-Huang Zhu, Bao-Kun Zheng, Meng Shen, Feng Gao, Hong-Yu Li, Ke-Xin Shi. Data Security and Privacy in Bitcoin System: A Survey[J]. Journal of Computer Science and Technology, 2020, 35(4): 843 -862 .
[9] Xiang-Jun Lu, Chi Zhang, Da-Wu Gu, Jun-Rong Liu, Qian Peng, Hai-Feng Zhang. Evaluating and Improving Linear Regression Based Profiling: On the Selection of Its Regularization[J]. Journal of Computer Science and Technology, 2020, 35(5): 1175 -1197 .

ISSN 1000-9000(Print)

CN 11-2296/TP

Editorial Board
Author Guidelines
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
E-mail: jcst@ict.ac.cn
  Copyright ©2015 JCST, All Rights Reserved