Fast generation of lexicographic satisfiable assignments: enabling canonicity in SAT-based applications

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.


Publié dans:
Proceedings of the International Conference on Computer Aided Design (ICCAD)
Présenté à:
International Conference on Computer Aided Design (ICCAD), Austin, Texas, USA, November 7-10, 2016
Année
2016
Publisher:
New York, Assoc Computing Machinery
ISBN:
978-1-4503-4466-1
Laboratoires:




 Notice créée le 2016-06-21, modifiée le 2019-03-17

n/a:
Télécharger le document
PDF

Évaluer ce document:

Rate this document:
1
2
3
 
(Pas encore évalué)