In Weighted Model Counting(WMC),we assign weights to literals and compute the sum of the weights of the models of a given propositional formula where the weight of an assignment is the product of the weights of its li...In Weighted Model Counting(WMC),we assign weights to literals and compute the sum of the weights of the models of a given propositional formula where the weight of an assignment is the product of the weights of its literals.The current WMC solvers work on Conjunctive Normal Form(CNF)formulas.However,CNF is not a natural representation for human-being in many applications.Motivated by the stronger expressive power of Pseudo-Boolean(PB)formulas than CNF,we propose to perform WMC on PB formulas.Based on a recent dynamic programming algorithm framework called ADDMC for WMC,we implement a weighted PB counting tool PBCounter.We compare PBCounter with the state-of-the-art weighted model counters SharpSAT-TD,ExactMC,D4,and ADDMC,where the latter tools work on CNF with encoding methods that convert PB constraints into a CNF formula.The experiments on three domains of benchmarks show that PBCounter is superior to the model counters on CNF formulas.展开更多
Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a ma...Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many reaHife problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis- Putnam-Logemann-Loveland （DPLL） procedure and Branch and Bound （B^B） algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007~2011 Max-SAT evaluations, emphasizing on the most promising research directions.展开更多
基金supported by NSFC(Grant Nos.61976050,61972384)the Jilin Province Science and Technology Department project(Nos.20240101378JC,20240602005RC,YDZJ202201ZYTS415)Jilin Education Department Project(No.JJKH20231319KJ)。
文摘In Weighted Model Counting(WMC),we assign weights to literals and compute the sum of the weights of the models of a given propositional formula where the weight of an assignment is the product of the weights of its literals.The current WMC solvers work on Conjunctive Normal Form(CNF)formulas.However,CNF is not a natural representation for human-being in many applications.Motivated by the stronger expressive power of Pseudo-Boolean(PB)formulas than CNF,we propose to perform WMC on PB formulas.Based on a recent dynamic programming algorithm framework called ADDMC for WMC,we implement a weighted PB counting tool PBCounter.We compare PBCounter with the state-of-the-art weighted model counters SharpSAT-TD,ExactMC,D4,and ADDMC,where the latter tools work on CNF with encoding methods that convert PB constraints into a CNF formula.The experiments on three domains of benchmarks show that PBCounter is superior to the model counters on CNF formulas.
基金supported by the Research Center of College of Computer and Information Sciences at King Saud University, Saudi Arabia
文摘Partial Maximum Boolean Satisfiability （Partial Max-SAT or PMSAT） is an optimization variant of Boolean satisfiability （SAT） problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many reaHife problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis- Putnam-Logemann-Loveland （DPLL） procedure and Branch and Bound （B^B） algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007~2011 Max-SAT evaluations, emphasizing on the most promising research directions.
