scholarly journals Lookahead-Based SMT Solving

10.29007/gzzf ◽  
2018 ◽  
Author(s):  
Antti Hyvärinen ◽  
Matteo Marescotti ◽  
Parvin Sadigova ◽  
Hana Chockler ◽  
Natasha Sharygina
Keyword(s):  
Upper Bound ◽  
Binary Tree ◽  
Search Space ◽  
Divide And Conquer ◽  
Constraint Solving ◽  
Prototype Implementation ◽  
Smt Solver ◽  
Smt Solving ◽  
Clause Learning

The lookahead approach for binary-tree-based search in constraint solving favors branching that provide the lowest upper bound for the remaining search space. The approach has recently been applied in instance partitioning in divide-and-conquer-based parallelization, but in general its connection to modern, clause-learning solvers is poorly understood. We show two ways of combining lookahead approach with a modern DPLL(T)-based SMT solver fully profiting from theory propagation, clause learning, and restarts. Our thoroughly tested prototype implementation is surprisingly efficient as an independent SMT solver on certain instances, in particular when applied to a non-convex theory, where the lookahead-based implementation solves 40% more unsatisfiable instances compared to the standard implementation.

Leveraging Control Flow Knowledge in SMT Solving of Program Verification

2021 ◽  
Vol 30 (4) ◽  
pp. 1-26
Author(s):  
Jianhui Chen ◽  
Fei He
Keyword(s):  
Program Verification ◽  
Search Space ◽  
General Purpose ◽  
Control Flow ◽  
Satisfiability Modulo Theories ◽  
Useful Knowledge ◽  
Smt Solver ◽  
Software Analysis ◽  
Smt Solving ◽  
Novel Approach

Satisfiability modulo theories (SMT) solvers have been widely applied as the reasoning engine for diverse software analysis and verification technologies. The efficiency of the SMT solver has significant effects on the performance of these technologies. However, current SMT solvers are designed for the general purpose of constraint solving. Lots of useful knowledge of programs cannot be utilized during SMT solving. As a result, the SMT solver may spend much effort to explore redundant search space. In this article, we propose a novel approach to utilizing control-flow knowledge in SMT solving. With this technique, the search space can be considerably reduced, and the efficiency of SMT solving is observably improved. We conducted extensive experiments on credible benchmarks. The results show significant improvements of our approach.

scholarly journals FOREST: An Interactive Multi-tree Synthesizer for Regular Expressions

2021 ◽  
pp. 152-169
Author(s):  
Margarida Ferreira ◽  
Miguel Terra-Neves ◽  
Miguel Ventura ◽  
Inês Lynce ◽  
Ruben Martins
Keyword(s):  
Real World ◽  
Regular Expression ◽  
User Interaction ◽  
Search Space ◽  
Satisfiability Modulo Theories ◽  
Experimental Results ◽  
Divide And Conquer ◽  
Regular Expressions ◽  
Smt Solver ◽  
Synthesis Procedure

AbstractForm validators based on regular expressions are often used on digital forms to prevent users from inserting data in the wrong format. However, writing these validators can pose a challenge to some users.We present Forest, a regular expression synthesizer for digital form validations. Forest produces a regular expression that matches the desired pattern for the input values and a set of conditions over capturing groups that ensure the validity of integer values in the input. Our synthesis procedure is based on enumerative search and uses a Satisfiability Modulo Theories (SMT) solver to explore and prune the search space. We propose a novel representation for regular expressions synthesis, multi-tree, which induces patterns in the examples and uses them to split the problem through a divide-and-conquer approach. We also present a new SMT encoding to synthesize capture conditions for a given regular expression. To increase confidence in the synthesized regular expression, we implement user interaction based on distinguishing inputs.We evaluated Forest on real-world form-validation instances using regular expressions. Experimental results show that Forest successfully returns the desired regular expression in 70% of the instances and outperforms Regel, a state-of-the-art regular expression synthesizer.

scholarly journals SMTS: Distributed, Visualized Constraint Solving

10.29007/fhgn ◽  
2018 ◽  
Author(s):  
Matteo Marescotti ◽  
Antti Hyvärinen ◽  
Natasha Sharygina
Keyword(s):  
Parallel Execution ◽  
Divide And Conquer ◽  
Constraint Solving ◽  
Web Interface ◽  
Smt Solver ◽  
Algorithm Portfolios ◽  
Sequential Constraint ◽  
Positive Experiences ◽  
Computing Environments ◽  
Development Resource

The inherent complexity of parallel computing makes development, resource monitor- ing, and debugging for parallel constraint-solving-based applications difficult. This paper presents SMTS, a framework for parallelizing sequential constraint solving algorithms and running them in distributed computing environments. The design (i) is based on a gen- eral parallelization technique that supports recursively combining algorithm portfolios and divide-and-conquer with the exchange of learned information, (ii) provides monitoring by visually inspecting the parallel execution steps, and (iii) supports interactive guidance of the algorithm through a web interface. We report positive experiences on instantiating the framework for one SMT solver and one IC3 solver, debugging parallel executions, and visualizing solving, structure, and learned clauses of SMT instances.

scholarly journals Lower and upper bounds for the continuous single facility location problem in the presence of a forbidden region and travel barrier

2020 ◽  
Author(s):  
Intesar Al-Mudahka ◽  
Marwa S. Al-Jeraiwi ◽  
Rym M’Hallah
Keyword(s):  
Objective Function ◽  
Upper Bound ◽  
Location Problem ◽  
Search Space ◽  
Upper Bounds ◽  
Divide And Conquer ◽  
Mixed Integer ◽  
Quadratic Constraints ◽  
Forbidden Region ◽  
Single Facility

In this paper, we investigate FRB, which is the single facility Euclidean location problem in the presence of a (non-)convex polygonal forbidden region where travel and location are not permitted. We search for a new facility’s location that minimizes the weighted Euclidean distances to existing ones. To overcome the non-convexity and non-differentiability of the problem’s objective function, we propose an equivalent reformulation (RFRB) whose objective is linear. Using RFRB, we limit the search space to regions of a set of non-overlapping candidate domains that may contain the optimum; thus we reduce RFRB to a finite series of tight mixed integer convex programming sub-problems. Each sub-problem has a linear objective function and both linear and quadratic constraints that are defined on a candidate domain. Based on these sub-problems, we propose an efficient bounding-based algorithm (BA) that converges to a (near-)optimum. Within BA, we use two lower and four upper bounds for the solution value of FRB. The two lower and two upper bounds are solution values of relaxations of the restricted problem. The third upper bound is the near-optimum of a nested partitioning heuristic. The fourth upper bound is the outcome of a divide and conquer technique that solves a smooth sub-problem for each sub-region. We reveal via our computational investigation that BA matches an existing upper bound and improves two more.

On Oriented Embedding of the Binary Tree into the Hypercube

1994 ◽  
Vol 3 (1) ◽  
pp. 27-38 ◽  
Author(s):  
Sergej L. Bezrukov
Keyword(s):  
Upper Bound ◽  
Binary Tree ◽  
New Approach

We consider the oriented binary tree and the oriented hypercube. The tree edges are oriented from the root to the leaves, while the orientation of the cube edges is induced by the direction from 0 to 1 in the coordinatewise form. The problem is to embed such a tree with l levels into the oriented n-cube as an oriented subgraph, for minimal possible n. A new approach to such problems is presented, which improves the known upper bound n/l ≤ 3/2 given by Havel [1] to n/l ≤ 4/3 + o(1) as l → ∞.

scholarly journals The ropelengths of knots are almost linear in terms of their crossing numbers

2019 ◽  
Vol 28 (14) ◽  
pp. 1950085
Author(s):  
Yuanan Diao ◽  
Claus Ernst ◽  
Attila Por ◽  
Uta Ziegler
Keyword(s):  
Upper Bound ◽  
Plane Graph ◽  
Crossing Number ◽  
Divide And Conquer ◽  
Plane Graphs ◽  
Cubic Lattice ◽  
Crossing Numbers ◽  
Total Length

For a knot or link [Formula: see text], let [Formula: see text] be the ropelength of [Formula: see text] and [Formula: see text] be the crossing number of [Formula: see text]. In this paper, we show that there exists a constant [Formula: see text] such that [Formula: see text] for any [Formula: see text], i.e. the upper bound of the ropelength of any knot is almost linear in terms of its minimum crossing number. This result is a significant improvement over the best known upper bound established previously, which is of the form [Formula: see text]. The proof is based on a divide-and-conquer approach on 4-regular plane graphs: a 4-regular plane graph of [Formula: see text] is first repeatedly subdivided into many small subgraphs and then reconstructed from these small subgraphs on the cubic lattice with its topology preserved with a total length of the order [Formula: see text]. The result then follows since a knot can be recovered from a graph that is topologically equivalent to a regular projection of it (which is a 4-regular plane graph).

scholarly journals Divide and Conquer: Towards Faster Pseudo-Boolean Solving

2018 ◽  
Author(s):  
Jan Elffers ◽  
Jakob Nordström
Keyword(s):  
Boolean Satisfiability ◽  
Conflict Analysis ◽  
Divide And Conquer ◽  
Theoretical Strength ◽  
Integer Coefficient ◽  
Sat Solvers ◽  
Wide Range ◽  
Clause Learning

The last 20 years have seen dramatic improvements in the performance of algorithms for Boolean satisfiability---so-called SAT solvers---and today conflict-driven clause learning (CDCL) solvers are routinely used in a wide range of application areas. One serious short-coming of CDCL, however, is that the underlying method of reasoning is quite weak. A tantalizing solution is to instead use stronger pseudo-Boolean (PB) reasoning, but so far the promise of exponential gains in performance has failed to materialize---the increased theoretical strength seems hard to harness algorithmically, and in many applications CDCL-based methods are still superior. We propose a modified approach to pseudo-Boolean solving based on division instead of the saturation rule used in [Chai and Kuehlmann '05] and other PB solvers. In addition to resulting in a stronger conflict analysis, this also improves performance by keeping integer coefficient sizes down, and yields a very competitive solver as shown by the results in the Pseudo-Boolean Competitions 2015 and 2016.

scholarly journals A New Upper Bound Based on Vertex Partitioning for the Maximum K-plex Problem

2021 ◽  
Author(s):  
Hua Jiang ◽  
Dongming Zhu ◽  
Zhichao Xie ◽  
Shaowen Yao ◽  
Zhang-Hua Fu
Keyword(s):  
Branch And Bound ◽  
Upper Bound ◽  
Undirected Graph ◽  
State Of The Art ◽  
Search Space ◽  
Exact Algorithms ◽  
Induced Subgraph ◽  
Massive Graphs ◽  
Vertex Set ◽  
Number Of Branches

Given an undirected graph, the Maximum k-plex Problem (MKP) is to find a largest induced subgraph in which each vertex has at most k−1 non-adjacent vertices. The problem arises in social network analysis and has found applications in many important areas employing graph-based data mining. Existing exact algorithms usually implement a branch-and-bound approach that requires a tight upper bound to reduce the search space. In this paper, we propose a new upper bound for MKP, which is a partitioning of the candidate vertex set with respect to the constructing solution. We implement a new branch-and-bound algorithm that employs the upper bound to reduce the number of branches. Experimental results show that the upper bound is very effective in reducing the search space. The new algorithm outperforms the state-of-the-art algorithms significantly on real-world massive graphs, DIMACS graphs and random graphs.

scholarly journals An Interval-Arithmetic-Based Approach to the Parametric Identification of the Single-Diode Model of Photovoltaic Generators

Energies ◽  
2020 ◽  
Vol 13 (4) ◽  
pp. 932 ◽  
Author(s):  
Martha Lucia Orozco-Gutierrez
Keyword(s):  
Experimental Data ◽  
Interval Arithmetic ◽  
Crystalline Silicon ◽  
Parametric Identification ◽  
Search Space ◽  
Operating Conditions ◽  
Divide And Conquer ◽  
Divide And Conquer Algorithm ◽  
Voltage Curve ◽  
Photovoltaic Generators

Parametric identification of the single diode model of a photovoltaic generator is a key element in simulation and diagnosis. Parameters’ values are often determined by using experimental data the modules manufacturers provide in the data sheets. In outdoor applications, the parametric identification is instead performed by starting from the current vs. voltage curve acquired in non-standard operating conditions. This paper refers to this latter case and introduces an approach based on the use of interval arithmetic. Photovoltaic generators based on crystalline silicon cells are considered: they are modeled by using the single diode model, and a divide-and-conquer algorithm is used to contract the initial search space up to a small hyper-rectangle including the identified set of parameters. The proposed approach is validated by using experimental data measured in outdoor conditions. The information provided by the approach, in terms of parametric sensitivity and of correlation between current variations and drifts of the parameters values, is discussed. The results are analyzed in view of the on-site application of the proposed approach for diagnostic purposes.

Formal basis for the refinement of rule based transition systems

1996 ◽  
Vol 6 (2) ◽  
pp. 329-354
Author(s):  
A. N Clark
Keyword(s):  
Software Development ◽  
Deterministic Model ◽  
Search Space ◽  
Transition Systems ◽  
Rule Based ◽  
Prototype Implementation ◽  
Development Path ◽  
Formal Basis

AbstractThis paper makes a contribution to the refinement of systems which involve search by proposing a simple non-deterministic model for rule based transition systems and using this to define a meaning for rule based refinement which allows each stage of the software development path to be verified with respect to the previous stage. The proposal allows a system which involves search to be specified in terms of all the possible outcomes. Each stage of refinement will introduce complexity to the rules and therefore develop the search space in ever more sophisticated ways. At each stage of the refinement it will be possible to be precise about which collections of outcomes have been deleted, thereby achieving a verified (prototype) implementation.

Sign in / Sign up

Export Citation Format

Share Document