satisfiability_weighted_ddnnf_negation (1017B)
1 # Satisfiability weighted ddnnf negation 2 3 The [computational_problem] of deciding whether a [dDNNF] has a [falsifying_assigment] of at least a given weight 4 - weight is given as a weight on each literal 5 - up to renormalization, up to negation 6 - 0 has weight 0 7 - 1 has positive weight 8 9 In the absence of weight this is [satisfiability_dnnnf_negation] which can be done thanks to [counting] 10 11 It is tractable when weights are written in [unary], by [dynamic programming]: we know how many assignments there are of each weight, and how many satisfying assignments there are on each weight 12 13 We can do [satisfiability_weighted_ddnnf] of deciding whether there is an assignment of at least this weight, by storing the maximum weight 14 - of course exact weight is [NP_hard] by reduction from [subset_sum] 15 16 Already challenging for [orthogonal_DNF], cf [satisfiability_weighted_orthogonal_DNF_negation] 17 18 Related to [ddnnf_complementation] 19 20 Up: [satisfiability_weighted_knowledge_compilation], [ddnnf], [ddnnf_complementation]