Browsing by Author "Diseth, Anastasia Chabounina"

Combinatorial optimization problems arise in many applications. Finding solutions that are as good as possible, ideally optimal, respect to given criteria is important. Additionally, many real-world combinatorial optimization problems are NP-hard. The so-called declarative approach to solving combinatorial optimization problems has proven to be successful in practice. In this work we focus on the the implicit hitting set-based (IHS) maximum satisfiability (MaxSAT) paradigm to solving combinatorial optimization problems declaratively. In the MaxSAT paradigm the problem at hand is formulated as a linear objective function to minimize subject to a set of constraints expressed in the language of propositional logic. In the IHS approach the problem is solved by alternating calls to two subroutines. An optimizer procedure computes optimal solutions over the variables in the objective function without the constraints available and a feasibility oracle verifies the solutions in terms of the constraints. In this work we study alternative divisions of constraints of a given problem formulation between the optimizer and the oracle. We allow the optimizer to compute solutions over any variables of the problem instance, thus extending the hitting set formulations of the IHS-based MaxSAT. We focus on two specific combinatorial optimization problems and existing MaxSAT encodings of these problems. The problems focus on are computing the treewidth of a graph and finding an optimal k-undercover Boolean matrix factorization. We have also extended a state-of-the-art IHS-based MaxSAT solver to support extended divisions of encodings and provide the implementation as open source.