TY - CPAPER
DO - 10.1145/2966986.2967040
AB - Lexicographic Boolean satisfiability (LEXSAT) is a variation of the Boolean satisfiability problem (SAT). Given a variable order, LEXSAT finds a satisfying assignment whose integer value under the given variable order is minimum (maximum) among all satisfiable assignments. If the formula has no satisfying assignments, LEXSAT proves it unsatisfiable, as does the traditional SAT. The paper proposes an efficient algorithm for LEXSAT by combining incremental SAT solving with binary search. It also proposes methods that use the lexicographic properties of the assignments to further improve the runtime when generating consecutive satisfying assignments in lexicographic order. The proposed algorithm outperforms the state-of-the-art LEXSAT algorithmâ€”on average, it is 2.4 times faster when generating a single LEXSAT assignment, and it is 6.3 times faster when generating multiple consecutive assignments.
T1 - Fast generation of lexicographic satisfiable assignments: enabling canonicity in SAT-based applications
DA - 2016
AU - Petkovska, Ana
AU - Mishchenko, Alan
AU - Soeken, Mathias
AU - De Micheli, Giovanni
AU - Brayton, Robert K.
AU - Ienne, Paolo
JF - Proceedings of the International Conference on Computer Aided Design (ICCAD)
PB - Assoc Computing Machinery
PP - New York
ID - 218889
SN - 978-1-4503-4466-1
UR - http://infoscience.epfl.ch/record/218889/files/2016_iccad_2.pdf
ER -