Texas A&M Physics Team Logs First-Place Finish in 2016 SAT Competition

As the saying goes in Aggieland, if you do something once at Texas A&M University, it’s a tradition.

Consider another one added to the list, now that a trio of Texas A&M physicists has taken first place in the incomplete unweighted Max-SAT random track solvers category of the 2016 Satisfiability (SAT) Competition, notching the victory with their first-ever entry into the vaunted annual international contest.

The 2016 SAT Competition is a competitive event for solvers of the Boolean Satisfiability (SAT) problem in computer science where one attempts to determine whether or not a Boolean formula — a set of binary variables linked together with Boolean operators, such as AND, NOT and OR — can be satisfied. Texas A&M’s team — composed of physics postdoctoral researcher Zheng Zhu, physics graduate student Chao Fang and physics professor Helmut G. Katzgraber, with input and advice from Texas A&M High Performance Research Computing’s Marinus Pennings — came up with the optimal solution with the best central processing unit (CPU) run time among all Max-SAT entries. Their work, which is funded in part by the U.S. Office of the Director of National Intelligence’s Intelligence Advanced Research Projects Activity (IARPA), is detailed in a recent paper posted to arXiv.

“Every year, the SAT association hosts a competition for the fastest SAT solver,” Katzgraber said. “These are hard computations problems, known as constraint satisfaction problems, that are relevant all across science and industry. Basically, if you can solve such a problem efficiently, you can solve a whole class of problems that can be found all over the place.”

This year’s SAT Competition was organized as a satellite event to the 19th International Conference on Theory and Applications of Satisfiability Testing, held July 5-8 in Bordeaux, France, and featuring a variety of tracks, including the Max-SAT solver one won by the Texas A&M physics team with its inaugural submission in the history of the overall competition. The objective is to gauge current state-of-the-art in the field of SAT solvers, a method of complex problem-solving that combines high-performance computing with high-end algorithmic developments, and to make such benchmark solutions publically available.

“We entered our solver in one track of the competition for the first time and won,” Katzgraber said. “This is huge, because industry, in particular, is very interested in these algorithms.”

Katzgraber said he and his teammates discovered this past spring that the algorithms they commonly use to study complex physics problems might be efficient in solving SAT problems. After testing and fine tuning, they arrived at their eventual top-ranked solution.

“Instead of using traditional local search algorithms that work in little corners of solution space, we used an algorithm designed to wander around the solution space efficiently,” Katzgraber said. “This, in turn, allowed us to find the solutions within record times.”

Organized since 2002, the SAT Competition is widely regarded as the driving force behind the development of SAT solvers, which are key in many industrial applications, including hardware and software verification. The SAT 2016 website notes that many hard combinatorial problems can be tackled using SAT-based techniques, including problems that arise in formal verification, artificial intelligence, operations research, computational biology, cryptology, data mining, machine learning and mathematics. The theoretical and practical advances in SAT research during the past 20 years have contributed to making SAT solving technology an indispensable tool in a variety of domains.

Katzgraber says his team plans to submit to more categories for future annual events, which he notes are as much about continuing to push the technological envelope as motivating grassroots innovation through friendly competition and the opportunity to compare and contrast ideas and approaches.

“Basically, if we can solve these hard combinatorial problems efficiently, we could, for example, create efficient probabilistic membership filters that are of keen interest to the U.S. government,” Katzgraber said.

For additional information on the 2016 SAT Competition and complete results, visit http://baldur.iti.kit.edu/sat-competition-2016/.

# # # # # # # # # #

About Research at Texas A&M University: As one of the world’s leading research institutions, Texas A&M is at the forefront in making significant contributions to scholarship and discovery, including that of science and technology. Research conducted at Texas A&M represented annual expenditures of more than $866.6 million in fiscal year 2015. Texas A&M ranked in the top 20 of the National Science Foundation’s Higher Education Research and Development survey (2014), based on expenditures of more than $854 million in fiscal year 2014. Texas A&M’s research creates new knowledge that provides basic, fundamental and applied contributions resulting in many cases in economic benefits to the state, nation and world. To learn more, visit http://research.tamu.edu.

-aTm-

Contact: Shana K. Hutchins, (979) 862-1237 or shutchins@science.tamu.edu or Dr. Helmut G. Katzgraber, (979) 845-2590 or hgk@tamu.edu