Show The Graduate Center Menu
 
 

PicatSAT

PicatSAT system developed by Neng-Fa Zhou took the first place in both the CSP and COP categories of the main track in the 2019 XCSP competition. Detailed results are available here:
XCSP3 Competition 2019 Results.

SAT solvers' performance has drastically improved during the past 20 years, thanks to the inventions of techniques from conflict-driven clause learning, backjumping, variable and value selection heuristics, to random restarts. SAT has become the backbone of many software systems that require combinatorial search, including formal methods, planning, software and hardware verification, and cyber security. Recently SAT has found its way into machine learning and data mining applications.

PicatSAT, which is available as a module in the Picat language, translates domain variables and constraints into SAT. PicatSAT employs a hybrid of log and direct encodings for domain variables, and performs numerous optimizations.

PicatSAT adopts optimizations from CP systems (preprocessing constraints to narrow the domains of variables), language compilers (decomposing constraints into basic ones and eliminating common subexpressions), and hardware design systems (using a logic optimizer to optimize codes for small constraints). Furthermore, PicatSAT reasons about equivalences in arithmetic constraints, and exploits them to eliminate variables and clauses. With these optimizations, PicatSAT is able to generate compact and fast code. PicatSAT is written in Picat with about 10,000 lines of code. Picat's features, such as attributed variables, arrays and maps, unification, pattern-matching rules, loops, and list comprehensions, are all put into good use in the implementation. There are hundreds of optimization rules, and they can be easily described as pattern-matching rules in Picat. Without Picat it would be impossible for our small team to implement such an optimizing compiler.

Details about PicatSAT can be found in the tutorial given by Neng-Fa Zhou at CP’19:
Building a Fast CSP Solver Based on SAT.