Upper Bounds for MaxSat: Further Improved

摘要: Given a boolean CNF formula F of length |F| (sum the number variables in each clause) with m clauses on n variables, we prove following results. --The MAXSAT problem, which asks for an assignment satisfying maximum F, can be solved O(1:341294m|F|) time. --The parameterized version that is determining whether there exists at least k (for some integer k), O(k21:380278k + |F|) time. --MAXSAT O(1:105729|F||F|) time. These bounds improve recent respectively O(1:3972m|F|), O(k21:3995k and O(1:1279|F||F|) due to Niedermeier Rossmanith [11] these problems. Our last bound comes quite close O(1:07578|F||F|) Hirsch[6] Satisfiability problem (not MAXSAT).