Salt ^® & Shaker^® Translation System

SAT solvers are a powerful class of constraint solver but require real-world problems to be translated into their Byzantine CNF input format. Salt is a constraint logic language and translation tool that significantly simplifies the process of applying a SAT solver to complex constraint problems such as those arising from hardware and software verification, optimization, and planning.

The Salt language provides a higher-level representation of propositional logic than CNF. Syntactically similar to a machine assembly language, the Salt language provides built-in operators for expressing propositional, fixed-point arithmetic, pseudo-Boolean, and set theoretic constraints. The Salt language is rigorously specified and has intrinsic support for tracking, propagating, and manipulating arithmetic overflow constraints. The application- and solver-independent syntax is designed to be both easy to write and easy to generate from a script or application program.

The Salt translation tool generates the DIMACS format CNF accepted by most modern SAT solvers. Salt contains a powerful but efficient optimization system that generates CNF that has been shown to reduce solution times by more than 30% on certain classes of known-hard arithmetic problems over standard translation algorithms. Because Salt starts from a higher semantic level than raw CNF, it can perform optimizations that are intractable for simple preprocessing tools to replicate. Salt has been demonstrated to scale to problems requiring millions of CNF variables to represent.

Salt comes bundled with the Shaker companion tool that translates the output from a SAT solver back into a form that can be interpreted by a human or application software. Shaker completely eliminates the need to parse the individual variable assignments returned by a SAT solver. Taken together, Salt and Shaker act as a complete level of abstraction between the SAT solver and the application. With Salt and Shaker, no knowledge of CNF or conversion routines is necessary.

Salt ^® & Shaker^® Key Benefits

• Productive: Salt can in integrated with existing tool flows. Time to translate problems into SAT and to interpret the results from SAT reduced from hours to minutes
• Powerful: Produces CNF that reduces the search time of modern SAT solvers by more than 5x over standard encoding algorithms for many clases of hard problems significantly beyond what simple preprocessing tools can achieve
• Expressive: Over 100 built in logic, set, and arithmetic operators
• Tunable: Salt language and tool parameters provide the control necessary to fine tune the translation for any choice of solver
• Complete: Salt and Shaker provide everything necessary to completely abstract any application from the underlying SAT solver
• Flexible: Syntax provides mechanism, not policy; built-in operators can be combined to produce any choice of problem encoding
• Scalable: Scales to any problem size a SAT solver can handle, including problems with over a million variables
• Sound: Salt language has a rigorous formal specification
• Easy to Use: Complete documentation and introductory examples are provided
• Compatible: Produces the DIMACS specified CNF format accepted by most modern SAT solvers

Request a White Paper

Version 1.5 now available. For more information about Salt & Shaker, including performance results and licensing terms, please contact us.