• Articles • Previous Articles    

Some Hard Examples for the Resolution Method

Yu Xiangdong;   

  1. Huazhong University of Science and Technology Wuhan;
  • Online:1990-05-10 Published:1990-05-10

Given n propositional variables,let K_n(i,j),0≤i≤j≤n,be the set (or disjunction )of all conjunctions of i literals of which exactly j literais are negative.Dunham and Wang conjectured that it may require exponential time to decide that every disjunction K_n (i,j)is not valid by the resolution method.This paper gives a proof of the conjecture and then exhibits a new counterexample to the feasibility of the resolution or con- sensus method.

Key words: computer graphics; point-sampled surface; segmentation; parameterization; $k$-means clustering; multidimensional scaling; 3D manipulation; solid modeling; virtual environment; constraint;

[1] Brartford Dunham and Hao Wang, Towards feasible solution of the tautology problem, Ann. Math. Logic, 10 (1976), 117-154.
[1] William Croft, Jörg-Rüdiger Sack, and Wei Shi. Differential Privacy via a Truncated and Normalized Laplace Mechanism [J]. Journal of Computer Science and Technology, 2022, 37(2): 369-388.
[2] Wen-Jun Yang, Bei-Ji Zou, Kai-Wen Li, Shu Liu. A Character Flow Framework for Multi-Oriented Scene Text Detection [J]. Journal of Computer Science and Technology, 2021, 36(3): 465-477.
[3] Yang-Jie Cao, Shuang Wu, Chang Liu, Nan Lin, Yuan Wang, Cong Yang, Jie Li. Seg-CapNet: A Capsule-Based Neural Network for the Segmentation of Left Ventricle from Cardiac Magnetic Resonance Imaging [J]. Journal of Computer Science and Technology, 2021, 36(2): 323-333.
[4] Jun Gao, Paul Liu, Guang-Di Liu, Le Zhang. Robust Needle Localization and Enhancement Algorithm for Ultrasound by Deep Learning and Beam Steering Methods [J]. Journal of Computer Science and Technology, 2021, 36(2): 334-346.
[5] Nuo Qun, Hang Yan, Xi-Peng Qiu, Xuan-Jing Huang. Chinese Word Segmentation via BiLSTM+Semi-CRF with Relay Node [J]. Journal of Computer Science and Technology, 2020, 35(5): 1115-1126.
[6] Hui-Si Wu, Meng-Shu Liu, Lu-Lu Yin, Ping Li, Zhen-Kun Wen, Hon-Cheng Wong. Automatic Video Segmentation Based on Information Centroid and Optimized SaliencyCut [J]. Journal of Computer Science and Technology, 2020, 35(3): 564-575.
[7] Xiao-Lin Li, Li Ma, Xiang-Dong He, Hui Xiong. You Are How You Behave-Spatiotemporal Representation Learning for College Student Academic Achievement [J]. Journal of Computer Science and Technology, 2020, 35(2): 353-367.
[8] Hong-Cheu Liu, Jixue Liu. On the Expressive Power of Logics on Constraint Databases with Complex Objects [J]. Journal of Computer Science and Technology, 2019, 34(4): 795-817.
[9] Ming-Zhe Zhang, Yun-Zhan Gong, Ya-Wen Wang, Da-Hai Jin. Unit Test Data Generation for C Using Rule-Directed Symbolic Execution [J]. Journal of Computer Science and Technology, 2019, 34(3): 670-689.
[10] Han Liu, Hang Du, Dan Zeng, Qi Tian. Cloud Detection Using Super Pixel Classification and Semantic Segmentation [J]. Journal of Computer Science and Technology, 2019, 34(3): 622-633.
[11] Bo Ren, Xu-Yun Yang, Ming C. Lin, Nils Thuerey, Matthias Teschner, Chenfeng Li. Visual Simulation of Multiple Fluids in Computer Graphics: A State-of-the-Art Report [J]. , 2018, 33(3): 431-451.
[12] Xu-Zhou Zhang, Yun-Zhan Gong, Ya-Wen Wang, Ying Xing, Ming-Zhe Zhang. Automated String Constraints Solving for Programs Containing String Manipulation Functions [J]. , 2017, 32(6): 1125-1135.
[13] Zai-Liang Chen, Peng Peng, Bei-Ji Zou, Hai-Lan Shen, Hao Wei, Rong-Chang Zhao. Automatic Anterior Lamina Cribrosa Surface Depth Measurement Based on Active Contour and Energy Constraint [J]. , 2017, 32(6): 1214-1221.
[14] Cui-Cui Zhang, Zhi-Lei Liu. Prior-Free Dependent Motion Segmentation Using Helmholtz-Hodge Decomposition Based Object-Motion Oriented Map [J]. , 2017, 32(3): 520-535.
[15] Ming-Ming Cheng, Qi-Bin Hou, Song-Hai Zhang, Paul L. Rosin. Intelligent Visual Media Processing: When Graphics Meets Vision [J]. , 2017, 32(1): 110-121.
Full text



[1] Chittabrata Ghosh, Bin Xie, and Dharma P. Agrawal. ROPAS: Cross-Layer Cognitive Architecture for Mobile UWB Networks[J]. , 2008, 23(3): 413 -425 .
[2] Rafael Messias Martins, Gabriel Faria Andery, Henry Heberle, Fernando Vieira Paulovich, Alneu de Andrade Lopes, Helio Pedrini, Member, IEEE, and Rosane Minghim, Member, IEEE. Multidimensional Projections for Visual Analysis of Social Networks[J]. , 2012, 27(4): 791 -810 .
[3] Li Chen, Jing-Zheng Wu, Yin-Run Lv, Yong-Ji Wang. An Efficient Approach for Solving Optimization over Linear Arithmetic Constraints[J]. , 2016, 31(5): 987 -1011 .
[4] En Wang, Yong-Jian Yang, Jie Wu, Fellow, IEEE, Wen-Bin Liu. A Buffer Scheduling Method Based on Message Priority in Delay Tolerant Networks[J]. , 2016, 31(6): 1228 -1245 .
[5] Fei-Fei Kou, Jun-Ping Du, Cong-Xian Yang, Yan-Song Shi, Wan-Qiu Cui, Mei-Yu Liang, Yue Geng. Hashtag Recommendation Based on Multi-Features of Microblogs[J]. , 2018, 33(4): 711 -726 .
[6] Xin Yang, Dawei Wang, Wenbo Hu, Li-Jing Zhao, Bao-Cai Yin, Qiang Zhang, Xiao-Peng Wei, Hongbo Fu. DEMC: A Deep Dual-Encoder Network for Denoising Monte Carlo Rendering[J]. Journal of Computer Science and Technology, 2019, 34(5): 1123 -1135 .

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