Dynamic SAT with Decision Change Costs: Formalization and Solutions
Daisuke Hatano and Katsutoshi Hirayama
We address a dynamic decision problem, in which decision makers must pay some costs when they change their decisions along the way. We formalize this problem as dynamic SAT (DynSAT) with decision change costs, whose goal is to find a sequence of models that would minimize the aggregation of the costs for changing variables. Then, we provide two solutions for solving the specific case of this problem. The first solution is to use a Weighted Partial MaxSAT solver after we encode the entire problem as the Weighted Partial MaxSAT problem. The second solution, which we believe is novel, is to use the Lagrangian decomposition technique. This technique divides the entire problem into sub-problems, each of which can be solved by an exact Weighted Partial MaxSAT solver separately, and produces both lower and upper bounds on the optimal in an anytime manner. To compare the performance of these solvers, we made experiments on the random problem and the target tracking problem. The experimental results show that a solver based on Lagrangian decomposition performs better for the random problem and competitively for the target tracking problem.