Problem solvers vary their approaches to solving problems depending on the context of the problem, the requirements of the solution, and the ways in which the problems and material to solve the problem are represented, or representations. Representations take many forms (i.e. tables, graphs, figures, images, formulas, visualizations, and other similar contexts) and are used to communicate information to a problem solver. Engagement with certain representations varies between problem solvers and can influence design and solution quality. A problem solver’s evaluation of representations and the reasons for using a representation can be considered factors in problem-solving heuristics. These factors describe unique problem-solving behaviors that can help understand problem solvers. These behaviors may lead to important relationships between a problem solver’s decisions and their ability to solve a problem and overall quality of the solution. Therefore, we pose the following research question: How do factors of problem-solving heuristics describe the unique behaviors of engineering students as they solve multiple problems? To answer this question, we interviewed 16 undergraduate engineering students studying civil engineering. The interviews consisted of a problem-solving portion that was followed immediately by a semi-structured retrospective interview with probing questions created based on the real time monitoring of themore »
G2SAT: Learning to Generate SAT Formulas
The Boolean Satisfiability (SAT) problem is the canonical NP-complete problem
and is fundamental to computer science, with a wide array of applications in planning,
verification, and theorem proving. Developing and evaluating practical SAT
solvers relies on extensive empirical testing on a set of real-world benchmark formulas.
However, the availability of such real-world SAT formulas is limited. While
these benchmark formulas can be augmented with synthetically generated ones,
existing approaches for doing so are heavily hand-crafted and fail to simultaneously
capture a wide range of characteristics exhibited by real-world SAT instances. In
this work, we present G2SAT, the first deep generative framework that learns to
generate SAT formulas from a given set of input formulas. Our key insight is
that SAT formulas can be transformed into latent bipartite graph representations
which we model using a specialized deep generative neural network. We show that
G2SAT can generate SAT formulas that closely resemble given real-world SAT
instances, as measured by both graph metrics and SAT solver behavior. Further,
we show that our synthetic SAT formulas could be used to improve SAT solver
performance on real-world benchmarks, which opens up new opportunities for
the continued development of SAT solvers and a deeper understanding of their
performance.
- Award ID(s):
- 1835598
- Publication Date:
- NSF-PAR ID:
- 10198846
- Journal Name:
- Advances in neural information processing systems
- ISSN:
- 1049-5258
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
The globalization of the IC supply chain has raised many security threats, especially when untrusted parties are involved. This has created a demand for a dependable logic obfuscation solution to combat these threats. Amongst a wide range of threats and countermeasures on logic obfuscation in the 2010s decade, the Boolean satisfiability (SAT) attack, or one of its derivatives, could break almost all state-of-the-art logic obfuscation countermeasures. However, in some cases, particularly when the logic locked circuits contain complex structures, such as big multipliers, large routing networks, or big tree structures, the logic locked circuit is hard-to-be-solved for the SAT attack. Usage of these structures for obfuscation may lead a strong defense, as many SAT solvers fail to handle such complexity. However, in this paper, we propose a neural-network-guided SAT attack (NNgSAT), in which we examine the capability and effectiveness of a message-passing neural network (MPNN) for solving these complex structures (SAT-hard instances). In NNgSAT, after being trained as a classifier to predict SAT/UNSAT on a SAT problem (NN serves as a SAT solver), the neural network is used to guide/help the actual SAT solver for finding the SAT assignment(s). By training NN on conjunctive normal forms (CNFs) corresponded to amore »
-
Quadratic Unconstrained Binary Optimization (QUBO) problem becomes an attractive and valuable optimization problem formulation in that it can easily transform into a variety of other combinatorial optimization problems such as Graph/number Partition, Max-Cut, SAT, Vertex Coloring, TSP, etc. Some of these problems are NP-hard and widely applied in industry and scientific research. Meanwhile, QUBO has been discovered to be compatible with two emerging computing paradigms, neuromorphic computing, and quantum computing, with tremendous potential to speed up future optimization solvers. In this paper, we propose a novel neuromorphic computing paradigm that employs multiple collaborative spiking neural networks to solve QUBO problems. Each SNN conducts a local stochastic gradient descent search and shares the global best solutions periodically to perform a meta-heuristic search for optima. We simulate our model and compare it to a single SNN solver and a mult-SNN solver without collaboration. Through tests on benchmark problems, the proposed method is demonstrated to be more efficient and effective in searching for QUBO optima. Specifically, it exhibits x10 and x15-20 speedup respectively on the multi-SNN solver without collaboration and the single-SNN solver.
-
The Multi-Agent Path Finding (MAPF) problem arises in many real-world applications, ranging from automated warehousing to multi-drone delivery. Solving the MAPF problem optimally is NP-hard, and existing optimal and bounded-suboptimal MAPF solvers thus usually do not scale to large MAPF instances. Greedy MAPF solvers scale to large MAPF instances, but their solution qualities are often bad. In this paper, we therefore propose a novel MAPF solver, Hierarchical Multi-Agent Path Planner (HMAPP), which creates a spatial hierarchy by partitioning the environment into multiple regions and decomposes a MAPF instance into smaller MAPF sub-instances for each region. For each sub-instance, it uses a bounded-suboptimal MAPF solver to solve it with good solution quality. Our experimental results show that HMAPP solves as large MAPF instances as greedy MAPF solvers while achieving better solution qualities on various maps.
-
Reusable symbolic evaluators are a key building block of solver-aided verification and synthesis tools. A reusable evaluator reduces the semantics of all paths in a program to logical constraints, and a client tool uses these constraints to formulate a satisfiability query that is discharged with SAT or SMT solvers. The correctness of the evaluator is critical to the soundness of the tool and the domain properties it aims to guarantee. Yet so far, the trust in these evaluators has been based on an ad-hoc foundation of testing and manual reasoning. This paper presents the first formal framework for reasoning about the behavior of reusable symbolic evaluators. We develop a new symbolic semantics for these evaluators that incorporates state merging. Symbolic evaluators use state merging to avoid path explosion and generate compact encodings. To accommodate a wide range of implementations, our semantics is parameterized by a symbolic factory, which abstracts away the details of merging and creation of symbolic values. The semantics targets a rich language that extends Core Scheme with assumptions and assertions, and thus supports branching, loops, and (first-class) procedures. The semantics is designed to support reusability, by guaranteeing two key properties: legality of the generated symbolic states, andmore »
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Publisher's Version of Record
- The DOI is not currently available
