Database migration is a ubiquitous need faced by enterprises that generate and use vast amounts of data. This is because of database software updates, or it is from changes to hardware, project standards, and other business factors. Migrating a large collection of databases is a way more challenging task than migrating a single database because of the presence of additional constraints. These constraints include capacities of shifts and sizes of databases. In this paper, we present a comprehensive framework that can be used to model database migration problems of different enterprises with customized constraints by appropriately instantiating the parameters of the framework. These parameters are the size of each database, the size of each shift, and the cost of testing each application. Each of these parameters can be either constant or arbitrary. Additionally, the cost of testing an application can be proportional to the number of databases that the application uses. We establish the computational complexities of a number of instantiations of this framework. We present fixed-parameter intractability results for various relevant parameters of the database migration problem. We also provide approximability and inapproximability results as well as lower bounds for the running time of any exact algorithm for the database migration problem. We show that the database migration problem is equivalent to a variation of the classical hypergraph partitioning problem. Our theoretical results also imply new theoretical results for the hypergraph partitioning problem that are interesting in their own right. Finally, we adapt heuristic algorithms devised for the hypergraph partitioning problem to the database migration problem, and we also give experimental results for the adapted heuristics. History: Accepted by Pascal Van Hentenryck, Area Editor for Computational Modeling: Methods & Analysis. Funding: B. Caskurlu and U. U. Acikalin are supported by The Scientific and Technological Research Council of Türkiye [Grant 122E599]. Supplemental Material: The software that supports the findings of this study is available within the paper and its Supplemental Information ( https://pubsonline.informs.org/doi/suppl/10.1287/ijoc.2023.0021 ) as well as from the IJOC GitHub software repository ( https://github.com/INFORMSJoC/2023.0021 ). The complete IJOC Software and Data Repository is available at https://informsjoc.github.io/ .

Abstract In this paper, we analyze two types of refutations for Unit Two Variable Per Inequality (UTVPI) constraints. A UTVPI constraint is a linear inequality of the form: $a_{i}\cdot x_{i}+a_{j} \cdot x_{j} \le b_{k}$ , where $a_{i},a_{j}\in \{0,1,-1\}$ and $b_{k} \in \mathbb{Z}$ . A conjunction of such constraints is called a UTVPI constraint system (UCS) and can be represented in matrix form as: ${\bf A \cdot x \le b}$ . UTVPI constraints are used in many domains including operations research and program verification. We focus on two variants of read-once refutation (ROR). An ROR is a refutation in which each constraint is used at most once. A literal-once refutation (LOR), a more restrictive form of ROR, is a refutation in which each literal ( $x_i$ or $-x_i$ ) is used at most once. First, we examine the constraint-required read-once refutation (CROR) problem and the constraint-required literal-once refutation (CLOR) problem. In both of these problems, we are given a set of constraints that must be used in the refutation. RORs and LORs are incomplete since not every system of linear constraints is guaranteed to have such a refutation. This is still true even when we restrict ourselves to UCSs. In this paper, we provide NC reductions between the CROR and CLOR problems in UCSs and the minimum weight perfect matching problem. The reductions used in this paper assume a CREW PRAM model of parallel computation. As a result, the reductions establish that, from the perspective of parallel algorithms, the CROR and CLOR problems in UCSs are equivalent to matching. In particular, if an NC algorithm exists for either of these problems, then there is an NC algorithm for matching.

This paper is concerned with a refutation system (proof system) for a class of linear constraint systems called difference constraint systems (DCS). In particular, we study the refutability of DCSs in the unit refutation (UR) system. Recall that a difference constraint is a linear relationship of the form: xi-xj ≤ bij and a DCS is a conjunction of such constraints. Associated with a refutation system are three important features, viz., (a) Soundness, (b) Completeness, and (c) Efficiency. The UR system is sound and efficient; however, it is incomplete, in that unsatisfiable DCSs may not have unit refutations. We establish that this refutation system is efficient in that there exists a tractable algorithm for determining if a DCS has a UR. Investigating weak (incomplete) refutation systems leads to a better understanding of the inference rules required for establishing contradictions in the given constraint system. Thus, this study is well-motivated. Despite the fact that unit refutations can be exponentially long in terms of the input system size, we provide a compact representation of these refutations. This compact representation is an important contribution of this paper.

Abstract In this paper, we discuss exact and parameterized algorithms for the problem of finding a read-once refutation (ROR) in an unsatisfiable Horn constraint system (HCS). Recall that a linear constraint system $\mathbf {A \cdot x \ge b}$ is said to be an HCS if each entry in $\textbf {A}$ belongs to the set $\{0,1,-1\}$ and at most one entry in each row of $\textbf {A}$ is positive. In this paper, we examine the importance of constraints in which more variables have negative coefficients than positive coefficients. In particular, we study the impact of the proportion of these ‘net-negative’ constraints has on the difficulty of finding RORs. There exist several algorithms for checking whether an HCS is feasible. To the best of our knowledge, these algorithms are not certifying, i.e. they do not provide a certificate of infeasibility. Our work is concerned with providing a specialized class of certificates called ‘read-once refutations’. In an ROR, each constraint defining the HCS may be used at most once in the derivation of a refutation. The problem of checking if an HCS has an ROR has been shown to be NP-hard. We analyse the HCS ROR problem from three different algorithmic perspectives, viz., parameterized algorithms, exact exponential algorithms and approximation algorithms. In particular, we show that the HCS ROR problem is fixed-parameter tractable (FPT) with respect to the number of constraints in the system that have more variables with negative coefficient than variables with positive coefficient. Additionally, we show that the HCS ROR problem becomes easy when this parameter is both small and large. We also derive an algorithm that runs in time $O(1.66^{m})$, where $m$ is the number of constraints in the HCS. On the lower-bound side, we derive a lower bound on the algorithmic resources needed for this problem using the Exponential Time Hypothesis. We also establish that the HCS ROR problem does not have a polynomial kernel when the number of constraints with three or more variables in a refutation is used as a parameter. Finally, we show that the problem of approximating the length of the shortest ROR in an HCS is NPO PB-complete1.

Abstract In this paper, we analyze Boolean formulas in conjunctive normal form (CNF) from the perspective of read-once resolution (ROR) refutation schemes. A read-once (resolution) refutation is one in which each clause is used at most once. Derived clauses can be used as many times as they are deduced. However, clauses in the original formula can only be used as part of one derivation. It is well known that ROR is not complete; that is, there exist unsatisfiable formulas for which no ROR exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called not-all-equal satisfiability (NAE-satisfiability). A CNF formula is NAE-satisfiable if it has a satisfying assignment in which at least one literal in each clause is set to false. It is well known that the problem of checking NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. The focus of this paper is on a variant of NAE-resolution called read-once NAE-resolution in which each clause (input or derived) can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for 2CNF formulas. Furthermore, we provide an algorithm to determine the smallest such NAE-resolution in polynomial time. This is in stark contrast to the corresponding problem concerning 2CNF formulas and ROR refutations. We also show that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

In this paper, we investigate properties of cutting plane based refutations for a class of integer programs called Horn constraint systems (HCS). Briefly, a system of linear inequalities A * x >= b is called a Horn constraint system, if each entry in A belongs to the set {0,1,-1} and furthermore there is at most one positive entry per row. Our focus is on deriving refutations i.e., proofs of unsatisfiability of such programs using cutting planes as a proof system. We also look at several properties of these refutations. Horn constraint systems can be considered as a more general form of propositional Horn formulas, i.e., CNF formulas with at most one positive literal per clause. Cutting plane calculus (CP) is a well-known calculus for deciding the unsatisfiability of propositional CNF formulas and integer programs. Usually, CP consists of a pair of inference rules. These are called the addition rule (ADD) and the division rule (DIV). In this paper, we show that cutting plane calculus is still complete for Horn constraints when every intermediate constraint is required to be Horn. We also investigate the lengths of cutting plane proofs for Horn constraint systems.

In this paper, we present two new problems and a theoretical framework that can be used to route information in heterogeneous communication networks. These problems are the cardinality-constrained and interval-constrained paths problems and they consist of finding paths in a network such that cardinality constraints on the number of nodes belonging to different sets of labels are satisfied. We propose a novel algorithm for finding said paths and demonstrate the effectiveness of our approach on networks of various sizes.