Publication

Guiding Real-world SAT Solving with Dynamic Hypergraph Separator Decomposition

AbstractThe general solution of satisfiability problems is NPComplete. Although state-of-the-art SAT solvers can efficiently obtain the solutions of many real-world instances, there are still a large number of real-world SAT families which cannot be solved in reasonable time. Much effort has been spent to take advantage of the internal structure of SAT instances. Existing decomposition techniques are based on preprocessing the static structure of the original problem. We present a dynamic decomposition method based on hypergraph separators. Integrating the separator decomposition into the variable ordering of a modern SAT solver leads to speedups on large real-world satisfiability problems. Compared with a static decomposition based variable ordering, such as Dtree (Huang and Darwiche, 2003), our approach does not need time to construct the full tree decomposition, which sometimes needs more time than the solving process itself. Our primary focus is to achieve speedups on large real-world satisfiability problems. Our results show that the new solver often outperforms both regular zChaff and zChaff integrated with Dtree decomposition. The dynamic separator decomposition shows promise in that it significantly decreases the number of decisions forsome real-world problems.

Download publication

Related Resources

See what’s new.

Publication

2013

Design Tools for the Rest of Us: Maker Hardware Requires Maker Software

In our own work, we are developing and applying a system which…

Publication

2012

Confirmation and Cognitive Bias in Design Cognition

The desire to better understand design cognition has led to the…

Publication

2013

Development of Discrete Event System Specification (DEVS) Building Performance Models for Building Energy Design

The discrete event system specification (DEVS) is a formalism for…

Publication

2009

Equivariant gluing constructions of contact-stationary Legendrian submanifolds in the (2n+1)-sphere

A contact-stationary Legendrian submanifold of the (2n+1)-sphere is a…

Get in touch

Something pique your interest? Get in touch if you’d like to learn more about Autodesk Research, our projects, people, and potential collaboration opportunities.

Contact us