Computer Science

Computer Science ›› 2024, Vol. 51 ›› Issue (11A): 240300161-5.doi: 10.11896/jsjkx.240300161

• Intelligent Computing • Previous Articles     Next Articles

Model Counting Method for Pseudo-Boolean Constraints

ZHENG Suhao1, NIU Qinzhou1, TAO Xiaomei2   

  1. 1 College of Information Science and Engineering,Guilin University of Technology,Guilin,Guangxi 541006,China
    2 School of Computer Science and Engineering & School of Software,Guangxi Normal University,Guilin,Guangxi 541006,China
  • Online:2024-11-16 Published:2024-11-13
  • About author:ZHENG Suhao,born in 1999,postgra-duate.His main research interests include SAT problem algorithms and theo-ry,and so on.
    NIU Qinzhou,born in 1956,Ph.D,professor.His main research interests include SAT problem algorithms,and computer network.
  • Supported by:
    National Natural Science Foundation of China(61906051).

PDF (PC)

155

Abstract: Pseudo-Boolean constraints problem is a kind of combinatorial optimization problem similar to the Boolean constraints problem.The core of solving such problems lies in encoding Pseudo-Boolean constraints in different mathematical forms,such as linear programming,integer programming,and other forms of combinatorial optimization.The current popular solution is to convert the problem into Boolean formulas,and then use the conflict-oriented clause learning(CDCL) class SAT solver to solve these Boolean formulas.This paper proposes a new method to solve the model counting problem in the Pseudo-Boolean constraints problem.Firstly,the related concepts of knowledge compilation and extension rules are introduced,and then how to transform Pseudo-Boolean constraints problem into binary decision diagram(BDD) by knowledge compilation is discussed in detail,and the characteristics of BDD structure are discussed emphatically.Finally,the model counting method based on extension rules isadoptedto deal with the model counting problem in Pseudo-Boolean constraints problem.Experimental results show that the proposed method has better performance when dealing with clauses with higher complementarity factors.

Key words: Pseudo-Boolean constraints, SAT problem, Model counting, Knowledge compilation, Clause

CLC Number: 

  • TP301
[1]EÉN N,SÖRENSSON N.Translating pseudo-boolean con-straints into SAT[J].Journal on Satisfiability,Boolean Mode-ling and Computation,2006,2(1/2/3/4):1-26.
[2]ABÍO I,NIEUWENHUIS R,OLIVERAS A,et al.A new look at BDDs for pseudo-Boolean constraints[J].Journal of Artificial Intelligence Research,2012,45:443-480.
[3]BOFILL M,COLL J,NIGHTINGALE P,et al.SAT encodings for Pseudo-Boolean constraints together with at-most-one constraints[J].Artificial Intelligence,2022,302:103604.
[4]DING Z Y.Research and Implementation of Applying LinearAlgebra to Solve Satisfiability Problem[D].Guangzhou:Sun Yat-sen University,2014.
[5]FANG C,LIU J.A linear algebra formulation for boolean satis-fiability testing[J].arXiv:1701.02401,2017.
[6]HAI L,JIGUI S,YIMIN Z.Theorem proving based on the extension rule[J].Journal of Automated Reasoning,2003,31:11-21.
[7]YIN M H,LIN H,SUN J G.Solving #SAT using extensionrules[J].Journal of Software,2009,20(7):1714-1725.
[8]JHA A,SUCIU D.Knowledge compilation meets database theory:compiling queries to decision diagrams[C]//Proceedings of the 14th International Conference on Database Theory.2011:162-173.
[9]INOUE K.Evaluating abductive hypotheses using an EM algorithm on BDDs[C]//Proc.IJCAI-09.2009:810-815.
[10]DARWICHE A.Decomposable negation normal form[J].Journal of the ACM(JACM),2001,48(4):608-647.
[11]GU W X.Knowledge Compilation Survey[J].Computer Scien-ce,2010,37(7):7.
[12]ZHAO X W.Research of the Knowledge compilation and Contingent Flexible Planning[D].Changchun:Northeast Normal University,2010.
[13]LYU S,ZHANG T,WANG Q,et al.Two Novel AlgorithmsBased on Extension Rule for Solving# SAT Problem[J].Journal of Northeastern University(Natural Science),2019,40(5):630.
[14]LATOUR A L D,SEN A,MEEL K S.Solving the identifying code set problem with grouped independent support[J].arXiv:2306.15693,2023.
[15]AUSIELLO G,CRESCENZI P,GAMBOSI G,et al.Complexity and approximation:Combinatorial optimization problems and their approximability properties[M].Springer Science & Business Media,2012.
[16]ROUGHGARDEN T.Algorithmic game theory[J].Communications of the ACM,2010,53(7):78-86.
[17]DUDEK J M,PHAN V H N,VARDI M Y.DPMC:weightedmodel counting by dynamic programming on projectjoin trees[C]//International Conference on Principles and Practice of Constraint Programming.Cham:Springer International Publi-shing,2020:211-230.
[18]SUZUKI R,HASHIMOTO K,SAKAI M.Improvement of Projected Model-Counting Solver with Component Decomposition Using SAT Solving in Components:JSAI Technical Report:SIG-FPAI[R].2017:31-36.
[19]PHILIPP T,STEINKE P.Pblib-a library for encoding pseudo-boolean constraints into cnf[C]//International Conference on Theory and Applications of Satisfiability Testing.Cham:SpringerInternational Publishing,2015:9-16.
[1] WANG Chenglong, HE Xingxing, ZANG Hui, LI Yingfang, WANG Danchen, LI Tianrui. Literal Chunk Contradiction and Clause Regular Contradiction in Propositional Logic [J]. Computer Science, 2024, 51(7): 272-277.
[2] LIU Lingrong, CHEN Shuwei, JIANG Shipan. L-type Redundancy Property in Propositional Logic [J]. Computer Science, 2023, 50(6A): 220600013-5.
[3] LI Jie, ZHONG Xiao-mei. Redundant Literals of Ternary Clause Sets in Propositional Logic [J]. Computer Science, 2022, 49(6A): 109-112.
[4] HE Bin, XU Dao-yun. Community Structure of Regular (3,4)-CNF Formula [J]. Computer Science, 2021, 48(4): 26-30.
[5] WANG Yi-jie, XU Yang, WU Guan-feng. Branching Heuristic Strategy Based on Learnt Clauses Deletion Strategy for SAT Solver [J]. Computer Science, 2021, 48(11): 294-299.
[6] SHEN Xue, CHEN Shu-wei, AI Sen-yang. Reward Mechanism Based Branching Strategy for SAT Solver [J]. Computer Science, 2020, 47(7): 42-46.
[7] ZHU Kai, WU Guo-qing, YUAN Meng-ting. On Hardness of Approximation for Optimized Problem of Synchronizing Partially Specified Deterministic Finite Automata [J]. Computer Science, 2020, 47(5): 14-21.
[8] SONG Bo-sheng, CHENG Yu. Uniform Solution to QAST Problem by Communication P Systems with MembraneDivision and Promoters [J]. Computer Science, 2020, 47(5): 38-42.
[9] CAO Feng,XU Yang,ZHONG Jian,NING Xin-ran. First-order Logic Clause Set Preprocessing Method Based on Goal Deduction Distance [J]. Computer Science, 2020, 47(3): 217-221.
[10] LIU Ting, XU Yang, CHEN Xiu-lan. Unit Clauses and Their Complementary Literals and Redundant Clauses in Propositional Logic [J]. Computer Science, 2019, 46(8): 255-259.
[11] WEN Xi-ming,FANG Liang-da,YU Quan,CHANG Liang,WANG Ju. Knowledge Forgetting in Multi-agent Modal Logic System KD45n [J]. Computer Science, 2019, 46(7): 195-205.
[12] CHEN Qing-shan, XU Yang, WU Guan-feng. Learnt Clause Evaluation Algorithm of SAT Problem Based on Trend Strength [J]. Computer Science, 2018, 45(12): 137-141.
[13] SHE Guang-wei, XU Dao-yun. Modified Warning Propagation Algorithm for Solving Regular (3,4)-SAT Instance Sets [J]. Computer Science, 2018, 45(11): 312-317.
[14] ZHANG Ming-ming and XU Dao-yun. Phase Transition Phenomenon of Regular 3-SAT Problem [J]. Computer Science, 2016, 43(4): 33-36.
[15] CHEN De-hua, FENG Jie-ying, LE Jia-jin and PAN Piao. Research on Structured Method for Chinese Pathological Text [J]. Computer Science, 2016, 43(10): 272-276.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.