000218889 001__ 218889
000218889 005__ 20190317000454.0
000218889 020__ $$a978-1-4503-4466-1
000218889 0247_ $$2doi$$a10.1145/2966986.2967040
000218889 02470 $$2ISI$$a000390297800004
000218889 037__ $$aCONF
000218889 245__ $$aFast generation of lexicographic satisfiable assignments: enabling canonicity in SAT-based applications
000218889 269__ $$a2016
000218889 260__ $$bAssoc Computing Machinery$$c2016$$aNew York
000218889 300__ $$a8
000218889 336__ $$aConference Papers
000218889 490__ $$aICCAD-IEEE ACM International Conference on Computer-Aided Design
000218889 520__ $$aLexicographic 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.
000218889 700__ $$0245677$$g196536$$aPetkovska, Ana
000218889 700__ $$aMishchenko, Alan
000218889 700__ $$0249604$$g263922$$aSoeken, Mathias
000218889 700__ $$0240269$$g167918$$aDe Micheli, Giovanni
000218889 700__ $$aBrayton, Robert K.
000218889 700__ $$g101954$$aIenne, Paolo$$0241619
000218889 7112_ $$dNovember 7-10, 2016$$cAustin, Texas, USA$$aInternational Conference on Computer Aided Design (ICCAD)
000218889 773__ $$tProceedings of the International Conference on Computer Aided Design (ICCAD)
000218889 8564_ $$uhttps://infoscience.epfl.ch/record/218889/files/2016_iccad_2.pdf$$zn/a$$s1054175$$yn/a
000218889 909C0 $$xU11140$$0252283$$pLSI1
000218889 909C0 $$0252192$$pLAP$$xU10418
000218889 909CO $$qGLOBAL_SET$$pconf$$pSTI$$pIC$$ooai:infoscience.tind.io:218889
000218889 917Z8 $$x112915
000218889 917Z8 $$x112915
000218889 937__ $$aEPFL-CONF-218889
000218889 973__ $$rREVIEWED$$sPUBLISHED$$aEPFL
000218889 980__ $$aCONF