Professors Vijay Ganesh and Krzysztof Czarnecki, along with their PhD student Jimmy Liang won a best paper award at the top-tier SPLC 2015 conference held in Nashville, TN, USA from July 20-24, 2015. The paper titled "SAT-based Analysis of Large Real-world Feature Models is Easy" explains why very large and complex feature models, encoded as Boolean satisfiability instances, are easy for SAT solvers to solve. This is indeed a puzzling phenomenon because modern SAT solvers are able to solve such large complex instances very efficiently, even though the Boolean SAT problem is known to be NP-complete (believed to be intractable in general). The authors performed very careful experiments to tease out the important structural aspects of such instances, and showed how modern solvers are able to exploit such structure. They also characterized the efficacy of modern solvers on such instances theoretically using ideas from parameterized complexity theory.
Thursday, August 6, 2015