CAMA: A Multi-Valued Satisfiability Solver

Cong Liu, Andreas Kuehlmann1, and Matthew W. Moskewicz
(Professor Alberto L. Sangiovanni-Vincentelli)
GSRC

Boolean satisfiabilty (SAT) has many applications in the area of electronic design automation. In this project, a genuine multi-valued (MV) SAT solver, CAMA, is developed. Unlike encoding approaches, it directly deals with MV variables. We extended the major speed-up techniques used in state-of-the-art binary SAT solvers, such as two literal watch-based Boolean constraint propagation (BCP), conflict-based learning with identifying unique interception point (UIP), non-chronological back-tracking, and so on. An efficient conflict analysis algorithm-based MV SAT is developed. It makes the learned clauses as compact as possible, which has a dramatic impact on the overall performance. Finally, the performance of CAMA is compared to that of Chaff [1], one of the best binary SAT solvers known so far, using a one hot encoding scheme. Our experimental results show that for hard MV SAT problems, CAMA outperforms Chaff. And our analysis also reveals some fundamental reasons why a MV SAT solver has inherent advantages over a binary SAT solver.

[1]
M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, "Chaff: Engineering an Efficient SAT Solver," Proc. Design Automation Conf., Las Vegas, NV, June 2001.
1Adjunct Professor

More information (http://www-cad.eecs.berkeley.edu/~congliu/) or

Send mail to the author : (congliu@eecs.berkeley.edu)


Edit this abstract