In this paper, we perform an experimental study of approximation algorithms for the unweighted tree augmentation problem (UTAP). Our goal is to establish a baseline performance for several existing approximation algorithms on actual instances rather than worst-case instances. In particular, we are interested in whether the algorithms' performance in practical instances is consistent with their worst-case guarantee rankings. We are also interested in whether preprocessing times, implementation difficulties, and running times justify the use of an algorithm in practice. We profile and analyze three approximation algorithms from the literature against a simple randomized algorithm. The performance of each algorithm was evaluated using metrics for space usage, running time, and solution quality. We found that the simple randomized algorithm is very competitive with the approximation algorithms and that the algorithms do not necessarily rank according to their theoretical guarantees. The randomized algorithm is easier to implement and understand, using less space than any of the more sophisticated approximation algorithms.

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 study two closely related problems on bipartite graphs, viz., the partial vertex cover problem and the budgeted maximum coverage problem. Both these problems arise in a number of different application domains, including, but not limited to, computer security and transportation logistics. It is well known that the vertex cover problem is solvable in polynomial time on bipartite graphs. However, the computational complexity of the partial vertex cover problem on bipartite graphs was open, thus far. In this paper, we establish that the partial vertex cover problem is \bf NP-hard, even on bipartite graphs. Our result also establishes that the closely related budgeted maximum coverage problem is \bf NP-hard on bipartite graphs. For the latter problem, we present an $\frac{8}{9}$-approximation algorithm. Our approximation guarantee matches and resolves the integrality gap of the natural linear programming relaxation for this problem and improves upon a recent $\frac{4}{5}$-approximation algorithm for the same problem.

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.

In this paper, we discuss certifying algorithms for zero-clairvoyant scheduling (ZCS) problems. ZCS problems are a class of real-time scheduling problems defined in the E-T-C scheduling framework [Subramani, K. (2005) A comprehensive framework for specifying clairvoyance, constraints and periodicity in real-time scheduling. Comput. J., 48, 259–272]. In ZCS, the dispatcher has no knowledge of the execution time of a given job, even after the job has finished executing. A polynomial-time algorithm for ZCS was proposed in previous work of the first author [Subramani, K. (2007) A polynomial time algorithm for zero-clairvoyant scheduling. J. Appl. Logic, 5, 667–680]. However, the algorithm proposed therein is not certifying. The algorithm that we propose in this paper is certifying, in that it provides a structure that certifies the ‘yes’-instances and another structure that certifies the ‘no’-instances of ZCS problems. These structures make the discovery of implementation errors straightforward and greatly simplify the software development cycle. Moreover, the certifying algorithm has the same running time (asymptotically) as its non-certifying counterpart. We also show that the proposed certifying technique can be used to certify a class of mathematical programs called E-Quantified Polyhedral programs (E-QPPs). However, for E-QPPs, the proposed certifying algorithm has a higher asymptotic running time than its non-certifying counterpart.

Abstract This paper is concerned with the design and analysis of improved algorithms for determining the optimal length resolution refutation (OLRR) of a system of difference constraints over an integral domain. The problem of finding short explanations for unsatisfiable Difference Constraint Systems (DCS) finds applications in a number of design domains including program verification, proof theory, real-time scheduling, and operations research. These explanations have also been called “certificates” and “refutations” in the literature. This problem was first studied in Subramani (J Autom Reason 43(2):121–137, 2009 ), wherein the first polynomial time algorithm was proposed. In this paper, we propose two new strongly polynomial algorithms which improve on the existing time bound. Our first algorithm, which we call the edge progression approach, runs in O ( n 2 · k + m · n · k ) time, while our second algorithm, which we call the edge relaxation approach, runs in O ( m · n · k ) time, where m is the number of constraints in the DCS, n is the number of program variables, and k denotes the length of the shortest refutation. We conducted an extensive empirical analysis of the three OLRR algorithms discussed in this paper. Our experiments indicate that in the case of sparse graphs, the new algorithms discussed in this paper are superior to the algorithm in Subramani (J Autom Reason 43(2):121–137, 2009 ). Likewise, in the case of dense graphs, the approach in Subramani (J Autom Reason 43(2):121–137, 2009 ) is superior to the algorithms described in this paper. One surprising observation is the superiority of the edge relaxation algorithm over the edge progression algorithm in all cases, although both algorithms have the same asymptotic time complexity.

This article is concerned with the design and analysis of polynomial time algorithms for determining whether a Planar Quantified Integer Program (PQIP) is feasible. A PQIP can be described briefly as an integer program involving two variables, in which each variable can be either universally or existentially quantified. There are four types of PQIPs, depending on how the variables are quantified (existentially or universally). In this article, we present two new, simple, and efficient algorithms for the ∀∃ case as well as a detailed account of the complexity of the other cases. Moreover, we discuss certification with respect to the provided algorithms.

In this article, we introduce a Prover–Verifier model for analysing the computational complexity of a class of constraint satisfaction problems (CSPs) termed boolean binary constraint satisfaction problems (BBCSPs). BBCSPs represent an extremely general class of CSPs and find applications in a wide variety of domains including constraint programming, puzzle solving and program testing. The constraints in a BBCSP permit the combination of multiple theories as opposed to traditional constraint systems in which all constraints belong to the same theory. We establish that each instance of a BBCSP admits a coin-flipping Turing machine that halts in time polynomial in the size of the input. Furthermore, the algorithm is oblivious in that it never sees more than one constraint at a time. The prover, P, in the Prover–Verifier model is endowed with very limited powers. In particular, it has no memory and it can only pose restricted queries to the verifier. The verifier, on the other hand, is both omniscient in that it is cognisant of all the problem details and insincere in that it does not have to decide a priori on the intended proof. However, the verifier must stay consistent in its responses, i.e. it cannot rule out a certain possibility in one response to a query from the prover and then rule in the same possibility in response to a subsequent query. We note that the combination of the resources required by the prover and the type of certificate demanded of the verifier, determine the resources required by an algorithm. Inasmuch as our provers will be memoryless and our verifiers will be asked for extremely simple certificates, our work establishes the existence of a simple, randomised algorithm for BBCSPs. Our model itself serves as a basis for the design of zero-knowledge machine learning algorithms in that the prover ends up learning the proof desired by the verifier. Likewise, our work finds applications in the domain of certifying algorithm design, wherein the goal is to provide a proof of correctness of the algorithm on the input instance by providing an easily checkable certificate.

Abstract In this paper, we analyze the problem of state minimization in a class of Finite State Automata called Two Start State Deterministic Finite State Automata (2-MDFAs). A 2-MDFA is similar to a deterministic finite state automaton (DFA), in that on a given input, each state has precisely one destination state; however, it differs from a DFA in that there are two start states. A string is accepted by a 2-MDFA if and only if there exists a transitional path from either start state to a finish state, on that string . Observe that 2-MDFAs provide a limited amount of non-determinism and hence investigating their properties from the perspective of state minimization is a worthwhile pursuit. In case of unbounded non-determinism, i.e., Non-deterministic finite state automata (NFAs), it is well-known that the state minimization problem is PSPACE-complete [Jiang and Ravikumar in Proceedings of the 18th International Colloquium on Automata, Languages and Programming, ICALP’91, Madrid, Spain, July 8–12, 1991] and further that such automata can be exponentially more succinct than DFAs [Meyer and Fischer in Proceedings of the 12th SWAT(Annual Symposium on switching and automata theory), pp 188-191, 1971]. Even in the case of 2-MDFAs, the minimization problem remains non-trivial; indeed, Malcher in Theor Comput Sci 327(3):375–390, 2004 shows that the corresponding decision problem is NP-complete. We focus on deriving approximability bounds for the state minimization problem in 2-MDFAs. Our main contribution in the current paper, is the design of an n -approximation algorithm for state minimization in 2-MDFAs, where n denotes the minimum number of states required to represent the input language as a 2-MDFA. We also present a proof that this bound is tight for our algorithm.

There are two principal modes in which real-time scheduling differs from scheduling in conventional models: (i) execution time variability and (ii) existence of complex timing constraints between jobs. There is a third issue that indirectly depends upon the non-constant nature of execution times, namely the degree of clairvoyance permitted by the application. Finally, there also exist the issues of periodicity and the presence of inter-period constraints; these issues need to be explicitly accounted for, in an analytic fashion. In traditional scheduling models, it is usual to assume fixed values for job execution times. This essentially means that a job will take exactly the same time to execute, in every instance of its invocation. From a real-time perspective, this assumption is both unrealistic and dangerous, in that it may lead to constraint violation at runtime. With a view towards enhancing the fault-tolerance of the system, the execution times of jobs are modeled through convex sets; doing so permits the capturing of situations that cannot be modeled otherwise. For instance, by monitoring the execution time of a job, over a number of independent runs, one can identify its safety interval with a high degree of confidence. The product of the safety intervals, over all the jobs in the system, forms a convex set. The second feature unique to real-time systems, is the presence of temporal relationships that constrain job execution. For instance, consider the pair of requirements: (i) job J1 should conclude 10 units before job J2 commences and (ii) job J2 commences within 12 units of job J1 concluding. These requirements cannot be modeled through precedence graphs, which by definition, are directed and acyclic. However, they can be easily modeled through simple, difference constraints. In hard real-time scheduling, it is important to guarantee the schedulability of the system a priori, since the violation of a constraint could lead to catastrophic consequences. However, in the presence of variable execution times and complex timing constraints, the definition of schedulablity is not obvious. In this context, it is necessary to mention the dispatchability problem; the dispatcher is concerned with strategies to assign jobs on the time line, once the scheduler has declared the job-set to be feasible. The nature of the schedulability query is determined by whether or not the dispatcher can use the execution times of jobs in the computation of the schedule. Observe that there are three possibilities, namely (i) the dispatcher never knows the execution time of a job, (ii) the dispatcher knows the execution time of a job after it has finished execution and (iii) the dispatcher knows the execution time of a job, even before it has commenced execution. Thus, depending upon the nature of the application involved, there are three different schedulability specifications, namely zero-clairvoyant (static), partially clairvoyant (parametric) and totally clairvoyant (co-static). Each specification affords a different level of flexibility and has different dispatching concerns. This paper presents the framework, called the E-T-C scheduling model, which explicitly accommodates execution time variability, complex timing constraints and different schedulability queries. This enables the specification of a wide range of real-time scheduling problems that occur in practical settings. This paper also discusses the relationships between flexibility and complexity in the proposed model. Each aspect of the model is motivated through examples from real-world design. The E-T-C model is itself a single period framework, in that all constraints are necessarily intra-period. This framework is extended to formulate the E-T-C-P scheduling framework, which explicitly accounts for inter-period constraints. The strengths of these two frameworks lie in their abilities to abstract the essentials of a number of real-time situations. In addition, decoupling the constraint system from the schedulability query greatly enhances the flexibility of the specification process. Although the primary purpose of this paper is to elaborate on scheduling problems only, it also discusses the problems of real-time dispatchability and optimization in clairvoyant scheduling.

In this paper we introduce a new mathematical modelling technique called Periodic Linear Programming; the periodic properties of Periodic Linear Programs (PLPs) permit the specification of inter-period constraints in embedded systems, in a straightforward and natural manner. We analyse PLPs in which the relationship between program variables is restricted to the class of difference constraints. Our analysis establishes that such PLPs can be reduced to simple linear programs, and hence decided in polynomial time. The class of difference constraints is extremely important from the perspective of embedded systems design, in that it permits the specification of complex timing constraints in real-time specification languages. A PLP can be thought of as a finite-description tool that represents infinite-state systems; although we use this tool purely for the purpose of modelling real-time scheduling problems, PLPs also find applications in other areas, such as concurrency design. In studying this programming paradigm, we develop novel techniques that, to the best of our knowledge, are not part of the literature. We build on the PLP structure to introduce a generalisation called Periodic Quantified Linear Programming; this programming paradigm permits the specification and analysis of uncertainty in the parameters of a PLP. Consequently, a Periodic Quantified Linear Program (PQLP) is the natural modelling tool to capture the requirements of periodic, embedded systems that are characterised by uncertainty in the execution times of processes, periodicity and relative timing constraints. In this paper, we use the PQLP structure to model and solve the periodic version of the zero-clairvoyant scheduling problem. Modelling uncertainty in the problem description is a typical technique used to incorporate a measure of fault-tolerance in the specification.

Summary form only given. Real-time systems are finding use in complex and dynamic environments such as cruise controllers, life support systems, nuclear reactors, etc., These systems have separate components that sense, control and stabilize the environment towards achieving the mission or target. These consociate components synchronize, compute and control themselves locally or have a centralized component to do the above. Distributed computing techniques improve the overall performance and reliability of large real-time systems with spread components. We propose and evaluate three distributed dispatching algorithms for partially clairvoyant schedules. For a job set of size n, the algorithms have dispatch times of O(1) per job. In the first algorithm, one processor executes all the jobs and other processors compute the dispatch functions. This scenario simplifies design and is better in situations where one processor controls all the devices. For the other algorithms, all the processors execute jobs assigned to them and compute the dispatch functions in a certain defined order; which is a plausible scenario in distributed controlling. We create various test-cases to test the algorithms due to the unavailability of benchmarks.

In this article, we exploit the graphical structure of 2SAT formulas to show that the shortest tree-like resolution refutation of an unsatisfiable 2SAT formula can be determined in polynomial time.