This article examines dynamic energy consumption caused by data during software execution on deeply embedded microprocessors, which can be significant on some devices. In worst-case energy consumption analysis, energy models are used to find the most costly execution path. Taking each instruction’s worst-case energy produces a safe but overly pessimistic upper bound. Algorithms for safe and tight bounds would be desirable. We show that finding exact worst-case energy is NP-hard, and that tight bounds cannot be approximated with guaranteed safety. We conclude that any energy model targeting tightness must either sacrifice safety or accept overapproximation proportional to data-dependent energy.
Formally, following the presentation of @cite_9 , define @math to be a set of literals, and @math a set of disjunctive form clauses: where each @math is a Boolean variable. A truth assignment defines each @math or its negation to be true. A clause is deemed to be satisfied if at least one literal in the clause is assigned true. A MAXSAT problem is a set of literals and set of clauses @math , such that the solution is the truth assignment that causes the maximal number of clauses to be satisfied.
@cite_9
2040924621
Abstract In this paper, we present improved exact and parameterized algorithms for the maximum satisfiability problem. In particular, we give an algorithm that computes a truth assignment for a boolean formula F satisfying the maximum number of clauses in time O(1.3247 m | F |), where m is the number of clauses in F , and | F | is the sum of the number of literals appearing in each clause in F . Moreover, given a parameter k , we give an O(1.3695 k +| F |) parameterized algorithm that decides whether a truth assignment for F satisfying at least k clauses exists. Both algorithms improve the previous best algorithms by Bansal and Raman for the problem.