Learn more about our powerful automated reasoning technology »

System And Method for Configuration of an Ensemble Solver

Publication Source: Patent US9684865B1

In a system for enabling configuration of an ensemble of several solvers, such that the ensemble can efficiently solve a constraint problem, for each one of several candidate configurations, an array of scores is computed. The array corresponds to a statistical parameter related to a problem solution, and the computation is based on, at least in part, a set of features associated with the problem. One candidate configuration is assigned to a solver, and based on the array of scores associated with that candidate configuration the same or a different candidate configuration is assigned to a another solver. A system for dynamically reconfiguring an ensemble of solvers obtains runtime data from several solvers, and a new configuration is determined by applying a machine learning and/or heuristic analysis procedure to the runtime data. The configuration of a solver may be updated according to the new configuration while that solver is running.
Google Scholar    Article

Systems and Methods for Planning a Solution to a Dynamically Changing Problem

Publication Source: Patent US8892483B1

A plan representing a final solution to a problem is obtained efficiently, if the problem changes while being solved, by identifying the solution elements not affected by the change, and by reusing those solution elements.
Google Scholar    Article

Extreme SAT-based Constraint Solving with R-Solve

Publication Source: The IEEE Conference on High Performance Extreme Computing (HPEC), Waltham, MA, USA, IEEE, September, 2014

We present the architecture of R-Solve, a highperformance constraint solver that extends the gains made in SAT performance over the past fifteen years on static decision problems to problems that require on-the-fly adaptation, solution space exploration and optimization. R-Solve brings together a modern, open SAT solver, HPC ideas in ensemble and collaborative parallel solving and a novel set of extensions supporting, for the first time, an efficient system for unrestricted incremental solving.
Google Scholar    Article

Systems, Methods, and Apparatus for Distributed Decision Processing

Publication Source: Patent US8688619B1

Methods, apparatus, and computer software product for making a decision based on the semantics of formal logic are provided. In an exemplary embodiment, two custom computing apparatuses are used to resolve the satisfiability of a logical formula and provide an example. In this embodiment, the two custom computing apparatuses operate in concert to explore the space of possible satisfying examples. This Abstract is provided for the sole purpose of complying with the Abstract requirement rules. This Abstract is submitted with the explicit understanding that it will not be used to interpret or to limit the scope or the meaning of the claims.
Google Scholar    Article

Poster Reception-Alef Parallel SAT Solver for HPC Hardware

Publication Source: The ACM/IEEE SC Conference on High Performance Networking and Computing, Tampa, FL, USA, 2006

Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications, including formal verification of both hardware and software, mathematics, and planning. However, solver performance, measured in terms of speed and maximum problem size, is a limiting factor to the application of SAT to real-world problems. We are developing a parallel SAT solver, Alef, to take advantage of HPC hardware.The Alef parallel SAT solver utilizes algorithms and heuristics that improve its performance over existing approaches. We are developing the solver to run well on commercially available HPC hardware. Our analysis shows that our algorithms combined with the low message latency of supercomputers are likely to produce a significant performance improvement over existing solvers in terms of speed and maximum problem size. Our poster will describe the algorithms we are using, illustrate our approach to problem partitioning, and present our performance analysis to date.
Google Scholar    Article

1 2