This paper describes SimX, a recently developed library for developing parallel, discrete-event simulations in Python. Written in C++ and Python, SimX enables rapid development and prototyping of a parallel simulation entirely in Python by providing the simulation modeler with core functionality such as processes, event queuing, time advancement, domain partitioning, synchronization and message passing. Designed for both ease-of-use and scalability, applications built using SimX can be executed on multi-core workstations or high performance clusters and can also be easily integrated with other Python tools for scientific computing. In this paper, we briefly discuss the motivation for developing SimX, provide a brief but illustrative example on using SimX to develop an application, a short description of its architecture and some of our initial experiences using SimX in a diverse array of domains. SimX is free software and is publicly available at http://github.com/sim-x under the GNU LGPL license.

We present the SimCore parallel simulation library, an object-oriented framework for developing parallel distributed discrete-event simulation applications, implemented in C++ with a Python front-end. SimCore is designed to scale to thousands of processors but is simple enough to use for application programmers, an outcome of its fast C++ core and message passing routines integrated with the full expressive power of Python. We discuss the design philosophy of SimCore including the software architecture and the C++/Python interface implementation that allows applications to be written in pure Python or a hybrid of Python and C++ or even pure C++. We also provide real world examples of the scalability and briefly describe a few diverse applications that have been deployed using SimCore.

As traditional hardware scaling laws have started to break down, Co-Design of hardware and software has become the most promising avenue towards exa-scale computing. We present a bottom-up approach as part of a larger project that develops an optimization framework for computational codesign for molecular dynamics applications. Our approach finds optimum circuit designs for arithmetic functions, such as square root or multiplication, which are the basic building blocks of the domain-specific arithmetic calculations in molecular dynamics simulations. Our design approach employs the Boolean satisfiability problem (SAT) as a vehicle for circuit design, using state-of-the-art SAT solvers that show their algorithmic power on mid-range performance computing platforms to rein in the inevitable combinatorial explosion of possible circuit designs as we increase the bit-length of our operations. While the main emphasis is on the modeling methodology, we show initial results of automated designs for a 4-bit square root circuit and a mini-calculator.

feedback received during a workshop of experts organized by the U.S. Department of Energy’s Office of Energy Policy and Systems Analysis. Our analysis demonstrates that achieving deep decarbonization by 2050 will require substantial decarbonization of the electric power sector resulting in an increase in the deployment of zero-carbon and low-carbon technologies such as renewables and carbon capture utilization and storage. The present results also show that the degree to which the electric power sector will need to decarbonize and low-carbon technologies will need to deploy depends on the nature of technological advances in the energy sector, the ability of end-use sectors to electrify and level of electricity demand.

This paper presents a detailed empirical study of local search for Boolean satisfiability (SAT), highlighting several interesting properties, some of which were previously unknown or had only anecdotal evidence. Specifically, we study hard random 3-CNF formulas and provide surprisingly simple analytical fits for the optimal (static) noise level and the runtime at optimal noise, as a function of the clause-to-variable ratio. We also demonstrate, for the first time for local search, a power-law decay in the tail of the runtime distribution in the low noise regime. Finally, we discuss a Markov Chain model capturing this intriguing feature.

This work proposes new approximate (and exact) inference methods for reasoning about an important and hard-to-compute property of the solution space of combinatorial problems, namely clusters of solutions. Given a constraint satisfaction problem (CSP), we can think of two solutions as being "connected" if they differ in the value of only one variable. Clusters of solutions can thus be defined in a natural manner: two solutions s 1 and s 2 are in the same cluster if and only if there is a path of connected solutions from s 1 to s 2 . The main question we seek to address is, given a CSP, how many solution clusters does it have?.

We present SessionSim, a tool for generating realistic communication sessions such as phone calls, http and email data traffic. Realistic data traffic is a crucial requirement to gauge the realism of any larger communication network simulation study. SessionSim is part of a large-scale communication network simulation environment (MIITS: Multi-scale Integrated Information and Telecommunications System), where detailed information about the individuals in a synthetic population is available, including activities (e.g., sleep, work, lunch) and locations. The key aspect of the SessionSim modeling philosophy is the insight that communication behavior heavily depends on the type of activity people are engaged in; key model parameters in addition to the nature of this dependence are inter-session times, source-destination pairs, and the actual data content that determines session size or duration. We present a mix of empirical data, earlier models and intuition for determining session parameters for phone calls, http and email and briefly discuss validation studies showing that our generated communication sessions adequately mimic real-world data. We also discuss our implementation of SessionSim in the scalable OO-simulation framework called SimCore.

Systematic search and local search paradigms for combinatorial problems are generally believed to have complementary strengths. Nevertheless, attempts to combine the power of the two paradigms have had limited success, due in part to the expensive information communication overhead involved. We propose a hybrid strategy based on shared memory, ideally suited for multi-core processor architectures. This method enables continuous information exchange between two solvers without slowing down either of the two. Such a hybrid search strategy is surprisingly effective, leading to substantially better quality solutions to many challenging Maximum Satisfiability (MaxSAT) instances than what the current best exact or heuristic methods yield, and it often achieves this within seconds. This hybrid approach is naturally best suited to MaxSAT instances for which proving unsatisfiability is already hard; otherwise the method falls back to pure local search.

We propose a new incomplete algorithm for the Maximum Satisfiability (MaxSAT) problem on unweighted Boolean formulas, focused specifically on instances for which proving unsatisfiability is already computationally difficult. For such instances, our approach is often able to identify a small number of what we call "bottleneck" constraints, in time comparable to the time it, takes to prove unsatisfiability. These bottleneck constraints can have useful semantic content. Our algorithm uses a relaxation of the standard backtrack search for satisfiability testing (SAT) as a guiding heuristic, followed by a low-noise local search when needed. This allows us to heuristically exploit the power of unit propagation and clause learning. On a test suite consisting of all unsatisfiable industrial instances from SAT Race 2008, our Solver, RelaxedMinisat, is the Only (MaxSAT) solver capable of identifying a single bottleneck constraint in all but one instance.

Constraint satisfaction problems (CSPs) are at the core of many tasks with direct practical relevance, such as hardware and software verification, planning, and scheduling to name a few. The two main solution paradigms for solving such problems are based on backtrack-style search and local search. However, recently, a new powerful technique, called survey propagation (SP), was introduced. SP can solve certain classes of problem instances with millions of variables and constraints. This discovery raised a question of whether the traditional techniques are the best one can do when tackling large and important constraint satisfaction problems. This dissertation discusses non-traditional approaches to solving CSPs. The techniques we use include probabilistic inference, statistical tools and a combination of systematic and local search. We provide a new derivation of SP based on purely combinatorial insights. Our method also enables us to derive SP-style procedures for a diverse range of constraint satisfaction problems, and provides insights into structure of solution spaces. The second part of the dissertation describes approaches to counting number of solutions of a CSP with the help of Belief Propagation and statistics. We also provide a novel hybrid algorithm for minimizing the number of violated constraints, which employs both systematic and local search, harnessing their complementary strengths. These methods are the most scalable algorithms for certain hard to solve classes of Boolean satisfiability (SAT), model counting (#SAT), and maximum satisfiability (MaxSAT) problems.

Decimation is a simple process for solving constraint satisfaction problems, by repeatedly fixing variable values and simplifying without reconsidering earlier decisions. We investigate different decimation strategies, contrasting those based on local, syntactic information from those based on message passing, such as statistical physics based Survey Propagation (SP) and the related and more well-known Belief Propagation (BP). Our results reveal that once we resolve convergence issues, BP itself can solve fairly hard random k-SAT formulas through decimation; the gap between BP and SP narrows down quickly as k increases. We also investigate observable differences between BP/SP and other common CSP heuristics as decimation proceeds, exploring the hardness of the decimated formulas and identifying a somewhat unexpected feature of message passing heuristics, namely, unlike other heuristics for satisfiability, they avoid unit propagation as variables are fixed.

We show that an important and computationally challenging solution space feature of the graph coloring problem (COL), namely the number of clusters of solutions, can be accurately estimated by a technique very similar to one for counting the number of solutions. This cluster counting approach can be naturally written in terms of a new factor graph derived from the factor graph representing the COL instance. Using a variant of the Belief Propagation inference framework, we can efficiently approximate cluster counts in random COL problems over a large range of graph densities. We illustrate the algorithm on instances with up to 100, 000 vertices. Moreover, we supply a methodology for computing the number of clusters exactly using advanced techniques from the knowledge compilation literature. This methodology scales up to several hundred variables.

We describe a novel approach to statistical learning from particles tracked while moving in a random environment. The problem consists in inferring properties of the environment from recorded snapshots. We consider here the case of a fluid seeded with identical passive particles that diffuse and are advected by a flow. Our approach rests on efficient algorithms to estimate the weighted number of possible matchings among particles in two consecutive snapshots, the partition function of the underlying graphical model. The partition function is then maximized over the model parameters, namely diffusivity and velocity gradient. A Belief Propagation (BP) scheme is the backbone of our algorithm, providing accurate results for the flow parameters we want to learn. The BP estimate is additionally improved by incorporating Loop Series (LS) contributions. For the weighted matching problem, LS is compactly expressed as a Cauchy integral, accurately estimated by a saddle point approximation. Numerical experiments show that the quality of our improved BP algorithm is comparable to the one of a fully polynomial randomized approximation scheme, based on the Markov Chain Monte Carlo (MCMC) method, while the BP-based scheme is substantially faster than the MCMC scheme.

We consider the problem of estimating the model count (number of solutions) of Boolean formulas, and present two techniques that compute estimates of these counts, as well as either lower or upper bounds with different trade-offs between efficiency, bound quality, and correctness guarantee. For lower bounds, we use a recent framework for probabilistic correctness guarantees, and exploit message passing techniques for marginal probability estimation, namely, variations of Belief Propagation (BP). Our results suggest that BP provides useful information even on structured loopy formulas. For upper bounds, we perform multiple runs of the MiniSat SAT solver with a minor modification, and obtain statistical bounds on the model count based on the observation that the distribution of a certain quantity of interest is often very close to the normal distribution. Our experiments demonstrate that our model counters based on these two ideas, BPCount and MiniCount, can provide very good bounds in time significantly less than alternative approaches.

Loop Calculus, introduced by Chertkov and Chernyak, is a new technique to incrementally improve approximations computed by Loopy Belief Propagation (LBP), with the ability to eventually make them exact. In this extended abstract, we give a brief overview of this technique, and show its relevance to the AI community. We consider the problem of Boolean Satisfiability (SAT) and use LBP with Loop Calculus corrections to perform probabilistic inference about the problem. In this preliminary work, we focus on identifying the main issues encountered when applying Loop Calculus, and include initial empirical results in the SAT domain.

Survey propagation (SP) is an exciting new technique that has been remarkably successful at solving very large hard combinatorial problems, such as determining the satisfiability of Boolean formulas. In a promising attempt at understanding the success of SP, it was recently shown that SP can be viewed as a form of belief propagation, computing marginal probabilities over certain objects called covers of a formula. This explanation was, however, shortly dismissed by experiments suggesting that non-trivial covers simply do not exist for large formulas. In this paper, we show that these experiments were misleading: not only do covers exist for large hard random formulas, SP is surprisingly accurate at computing marginals over these covers despite the existence of many cycles in the formulas. This re-opens a potentially simpler line of reasoning for understanding SP, in contrast to some alternative lines of explanation that have been proposed assuming covers do not exist.

Performing realistic simulations of Internet packet traffic on a national or global level is a daunting task from both the modeling and the computational perspective. We present the MIITS (Multi-scale Integrated Information and Telecommunications System) tool that implements a novel approach to network simulation and report first scaling results from a realistic Internet scenario. MIITS' end-to-end approach to network simulation relies on modules for (i) accurate network topology and capacity representation, (ii) realistic communication session generation based on the activities of an agent population that is statistically equivalent to the population in a large metropolitan area, (iii) the actual scalable packet-level network simulation that is based on distributed event?driven technology, and (iv) analysis of large amounts of simulation output data. We present a sample simulation of a Los Angeles network as an intermediate step toward the vision of national-level simulation.

Motivated by realistic sensor network scenarios that have mis-informed nodes and variable network topologies, we propose an approach to routing that combines the best features of limited-flooding and information-sensitive path-finding protocols into a reliable, low-power method that can make delivery guarantees independent of parameter values or information noise levels. We introduce Parametric Probabilistic Sensor Network Routing Protocols, a family of light-weight and robust multi-path routing protocols for sensor networks in which an intermediate sensor decides to forward a message with a probability that depends on various parameters, such as the distance of the sensor to the destination, the distance of the source sensor to the destination, or the number of hops a packet has already traveled. We propose two protocol variants of this family and compare the new methods to other probabilistic and deterministic protocols, namely constant-probability gossiping, uncontrolled flooding, random wandering, shortest path routing (and a variation), and a load-spreading shortest-path protocol inspired by (Servetto and Barrenechea, 2002). We consider sensor networks where a sensor's knowledge of the local or global information is uncertain (parametrically noised) due to sensor mobility, and investigate the trade-off between robustness of the protocol as measured by quality of service (in particular, successful delivery rate and delivery lag) and use of resources (total network load). Our results for networks with randomly placed nodes and realistic urban networks with varying density show that the multi-path protocols are less sensitive to misinformation, and suggest that in the presence of noisy data, a limited flooding strategy will actually perform better and use fewer resources than an attempted single-path routing strategy, with the Parametric Probabilistic Sensor Network Routing Protocols outperforming other protocols. Our results also suggest that protocols using network information perform better than protocols that do not, even in the presence of strong noise.

We propose a hybrid model to alleviate the notorious problem of premature battery depletion in sensor networks: in a first stage, simple sensors are deployed over an area of interest using any traditional method, in a second phase, more powerful relays are put in positions that allow them to off-load as much of the forwarding burden imposed on the simple sensors as possible. We introduce this model in detail, give a few theoretical results with respect to the optimal placement of the powerful sensors, propose various heuristic approaches for their placement, and present comparative simulation results for these heuristics.