Chapter 9. Preprocessing in SAT Solving

Preprocessing has become a key component of the Boolean satisfiability (SAT) solving workflow. In practice, preprocessing is situated between the encoding phase and the solving phase, with the aim of decreasing the total solving time by applying efficient simplification techniques on SAT instances to speed up the search subsequently performed by a SAT solver. In this chapter, we overview key preprocessing techniques proposed in the literature. While the main focus is on techniques applicable to formulas in conjunctive normal form (CNF), we also selectively cover main ideas for preprocessing structural and higher-level SAT instance representations.

Equational Theorem Proving Modulo

Unlike other methods for theorem proving modulo with constrained clauses [12, 13], equational theorem proving modulo with constrained clauses along with its simplification techniques has not been well studied. We introduce a basic paramodulation calculus modulo equational theories E satisfying certain properties of E and present a new framework for equational theorem proving modulo E with constrained clauses. We propose an inference rule called Generalized E-Parallel for constrained clauses, which makes our inference system completely basic, meaning that we do not need to allow any paramodulation in the constraint part of a constrained clause for refutational completeness. We present a saturation procedure for constrained clauses based on relative reducibility and show that our inference system including our contraction rules is refutationally complete.

Home Economics, “Handicapped Homemakers,” and Postwar America

In the two decades following World War II, a loose network of home economists at colleges and universities across the United States turned their attention to homemaking methods for women with physical disabilities. Often in consultation with physically disabled homemakers, these home economists researched and designed assistive devices, adaptive equipment, and work simplification techniques for use in the home. Their efforts signaled a new field of study, “homemaker rehabilitation,” which helped to enlarge the broader vocational rehabilitation system beyond its historic focus on male veterans and wage earners while also expanding the boundaries of home economics itself. Home economists’ work with disabled homemakers both bolstered and challenged postwar domesticity, middle-class gender roles, and able-bodied normalcy. Calling attention to these contradictions reveals much about how home economists engaged with and understood disability and how their work intersected with burgeoning movements for disability rights.

Modelling and Analysis of Semantically Enriched Simplified Trajectories Using Graph Databases

<p><strong>Abstract.</strong> Geospatial databases are utilized in modelling the huge volume of spatial-temporal data generated by tracking moving objects equipped with positioning devices. This data can be used in performing trajectory analysis such as optimum path finding or identification of collision risk. At the same time, this massive data becomes difficult to handle using traditional databases as raw trajectories contain a lot of unnecessary data points. Thus, trajectory simplification techniques are applied to reduce the number of vertices representing a trajectory. However, elimination of intermediate points by simplification process leads to a loss of semantics associated with the trajectories. These semantics are dependent on the application domain. For example, a trajectory of a moving vessel can convey information about time, distances travelled, bearing, or velocity. This research proposes a graph data model that enriches the simplified geometry of trajectories with the semantics lost in the simplification process. Raw trajectories, initially modelled and stored in a PostgreSQL/PostGIS database, are simplified according to both their spatial and temporal characteristics using the Synchronized Euclidean Distance (SED), while the Semantically Enriched Line simpliFication (SELF) data structure is adopted to preserve the semantics of the vertices eliminated in the simplification process. Then, enriched simplified trajectories are transferred to a Neo4j database and modelled in terms of nodes and edges using graphs. Trajectories can then be further processed using Cypher query language and Neo4j spatial procedures. A visualization tool has been developed on top of Neo4j graph database to support the semantic retrieval and visualization of trajectories.</p>

Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing

The theory of arrays has a central place in software verification due to its ability to model memory or data structures. Yet, this theory is known to be hard to solve in both theory and practice, especially in the case of very long formulas coming from unrolling-based verification methods. Standard simplification techniques à la read-over-write suffer from two main drawbacks: they do not scale on very long sequences of stores and they miss many simplification opportunities because of a crude syntactic (dis-)equality reasoning. We propose a new approach to array formula simplification based on a new dedicated data structure together with original simplifications and low-cost reasoning. The technique is efficient, scalable and it yields significant simplification. The impact on formula resolution is always positive, and it can be dramatic on some specific classes of problems of interest, e.g. very long formula or binary-level symbolic execution. While currently implemented as a preprocessing, the approach would benefit from a deeper integration in an array solver.