A branch and bound algorithm for extracting smallest minimal unsatisfiable subformulas

Explaining the causes of infeasibility of Boolean formulas has practical applications in numerous fields, such as artificial intelligence (repairing inconsistent knowledge bases), formal verification (abstraction refinement and unbounded model checking), and electronic design (diagnosing and correcting infeasibility). Minimal unsatisfiable subformulas (MUSes) provide useful insights into the causes of infeasibility. An unsatisfiable formula often has many MUSes. Based on the application domain, however, MUSes with specific properties might be of interest. In this paper, we tackle the problem of finding a smallest-cardinality MUS (SMUS) of a given formula. An SMUS provides a succinct explanation of infeasibility and is valuable for applications that are heavily affected by the size of the explanation. We present (1) a baseline algorithm for finding an SMUS, founded on earlier work for finding all MUSes, and (2) a new branch-and-bound algorithm called Digger that computes a strong lower bound on the size of an SMUS and splits the problem into more tractable subformulas in a recursive search tree. Using two benchmark suites, we experimentally compare Digger to the baseline algorithm and to an existing incomplete genetic algorithm approach. Digger is shown to be faster in nearly all cases. It is also able to solve far more instances within a given runtime limit than either of the other approaches.     

Matching From the First Iteration: An Iterative Switching Algorithm for an Input Queued Switch

An iterative switching algorithm for an input queued switch consists of a number of iterations in every time step, where each iteration computes a disjoint matching. If input is matched to output in a given iteration, a packet (if any) is forwarded from to in the corresponding time step. Most of the iterative switching algorithms use a request grant accept (RGA) arbitration type (e.g. iSLIP). Unfortunately, due to this particular type of arbitration, the matching computed in one iteration is not necessarily maximal (more input and output ports can still be matched). This is exactly why multiple iterations are needed. However, multiple iterations make the time step larger and reduce the speed of the switch. We present a new iterative switching algorithm (based on the RGA arbitration) called with the underlying assumption that the number of iterations is possibly limited to one, hence reducing the time step and allowing the switch to run at a higher speed. We prove that achieves throughput and delay guarantees with a speedup of 2 and one iteration under a constant burst traffic model, which makes as good as any maximal matching algorithm in the theoretical sense. We also show by simulation that achieves relatively high throughput in practice under uniform and non-uniform traffic patterns with one iteration and no speedup.     

Eco-City Projects: Incorporating Sustainability Requirements during Pre-Project Planning

International standards exist for evaluating building or neighborhood sustainability. Nonetheless, they are still not available for large-scale developments. Of special interest to practitioners is how to ensure that sustainability requirements of large-scale projects are well integrated in a master plan. This paper provides design managers of new eco-cities with a framework to integrate sustainability in the pre-project planning phase. A case study of a planned eco-city is investigated to delineate its pre-project planning practices, compare them to the proposed framework, and infer lessons learned. The case study highlights the importance of regular interactions between business planners and master planners to incorporate sustainability requirements at early planning phases.     

Switching using parallel input-output queued switches with no speedup

We propose an efficient parallel switching architecture that requires no speedup and guarantees bounded delay. Our architecture consists of k input-output-queued switches with first-in-first-out queues, operating at the line speed in parallel under the control of a single scheduler, with k being independent of the number N of inputs and outputs. Arriving traffic is demultiplexed (spread) over the k identical switches, switched to the correct output, and multiplexed (combined) before departing from the parallel switch. We show that by using an appropriate demultiplexing strategy at the inputs and by applying the same matching at each of the k parallel switches during each cell slot, our scheme guarantees a way for cells of a flow to be read in order from the output queues of the switches, thus, eliminating the need for cell resequencing. Further, by allowing the scheduler to examine the state of only the first of the k parallel switches, our scheme also reduces considerably the amount of state information required by the scheduler. The switching algorithms that we develop are based on existing practical switching algorithms for input-queued switches, and have an additional communication complexity that is optimal up to a constant factor.     

On achieving throughput in an input-queued switch

We establish some lower bounds on the speedup required to achieve throughput for some classes of switching algorithms in a input-queued switch with virtual output queues (VOQs). We use a weak notion of throughput, which will only strengthen the results, since an algorithm that cannot achieve weak throughput cannot achieve stronger notions of throughput. We focus on priority switching algorithms, i.e., algorithms that assign priorities to VOQs and forward packets of high priority first. We show a lower bound on the speedup for two fairly general classes of priority switching algorithms: input priority switching algorithms and output priority switching algorithms. An input priority scheme prioritizes the VOQs based on the state of the input queues, while an output priority scheme prioritizes the VOQs based on their output ports. We first show that, for output priority switching algorithms, a speedup S/spl ges/2 is required to achieve weak throughput. From this, we deduce that both maximal and maximum size matching switching algorithms do not imply weak throughput unless S/spl ges/2. The bound of S/spl ges/2 is tight in all cases above, based on a result in Dai et al. Finally, we show that a speedup S/spl ges/3/2 is required for the class of input priority switching algorithms to achieve weak throughput.     

Principles of sequential-equivalence verification

Traditionally, designers use simulation to check the functional equivalence of specification and implementation models. Although simulation can eliminate some or most design errors, it can never completely certify design correctness. Formal equivalence verification (FEV) is a viable alternative that has gained wide industrial acceptance. FEV, which uses automata theory and mathematical logic to formally reason about the correctness of design transformations, is broadly divided into two categories: combinational and sequential. This article is a general survey of conceptual and algorithmic approaches to sequential equivalence checking. Although this fundamental problem is very complex, recent advances in satisfiability solvers and ATPG approaches are making good headway.