发表机构
Faculty of Engineering Science, College of Engineering, University of Tehran; Department of Engineering Science, College of Engineering, University of Tehran（德黑兰大学工程学院; 德黑兰大学工程学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文研究连续t-模下的双极模糊最小权可满足性问题，提出子句见证分支定界方法，其打包界可减少约45%的已探索节点数，验证了求解器的有效性。
AI 中文摘要
最小权可满足性要求找到满足布尔赋值且代价最小，而许多模糊决策与知识系统采用分级正、负关系而非清晰文字。本文提出双极模糊最小权可满足性问题，其中正、负子句-变量关系、目标子句水平及变量状态均用单位区间表示。子句要求由任意连续t-模定义的双极模糊关系等式表达，经典最小权CNF可满足性作为清晰特例可恢复，且无论所选t-模为何，即便所提公式采用连续变量，该特例仍存在最优布尔解。针对分级问题，子句满足性由容许变量域与有效子句见证集表征，该结构催生了带预处理、传播、下闭包及不相交见证打包界的精确子句见证分支定界方法。计算实验针对显式见证枚举、混合整数基线及外部SATLIB公式验证了求解器；在聚焦的分级消融集上，打包界相比单行见证界将已探索节点的中位数减少约45%。
英文摘要
Minimum-weight satisfiability asks for a satisfying Boolean assignment of minimum cost, while many fuzzy decision and knowledge systems operate with graded positive and negative relations rather than crisp literals. This paper introduces a bipolar fuzzy minimum-weight satisfiability problem in which positive and negative clause--variable relations, target clause levels, and variable states are represented in the unit interval. The clause requirements are expressed by bipolar fuzzy relational equalities defined with an arbitrary continuous t-norm. Classical minimum-weight CNF satisfiability is recovered as a crisp special case, independently of the selected t-norm, and an optimal Boolean solution is shown to exist in that specialization even though the proposed formulation uses continuous variables. For the graded problem, clause satisfaction is characterized through admissible variable domains and effective clause-witness sets. This structure leads to an exact clause-witness branch-and-bound method with preprocessing, propagation, lower-point closure, and a disjoint-witness packing bound. Computational experiments verify the solver against explicit witness enumeration, mixed-integer baselines, and external SATLIB formulas; on a focused graded ablation set, the packing bound reduces the median number of explored nodes by about 45 percent relative to the single-row witness bound.
