doi:10.1145/2966986.2967040
ISI:000390297800004
Petkovska, Ana
Mishchenko, Alan
Soeken, Mathias
De Micheli, Giovanni
Brayton, Robert K.
Ienne, Paolo
Fast generation of lexicographic satisfiable assignments: enabling canonicity in SAT-based applications
New York, Assoc Computing Machinery
http://infoscience.epfl.ch/record/218889/files/2016_iccad_2.pdf
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.
2016-06-21T13:02:46Z
http://infoscience.epfl.ch/record/218889
http://infoscience.epfl.ch/record/218889
Text