research-article

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

Authors:

Paolo IenneAuthors Info & Claims

2016 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Pages 1 - 8

https://doi.org/10.1145/2966986.2967040

Published: 07 November 2016 Publication History

Abstract

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.

8. References

[1]

The EPFL Combinational Benchmark Suite, “Multi-output PLA benchmarks”. http://1si.epf1.ch/benchmarks.

Google Scholar

[2]

Berkeley Logic Synthesis and Verification Group, Berkeley, Calif. ABC: A System for Sequential Synthesis and Verification. httD://www.eecs.berkelev.edu/Thlanmi/abc/.

Google Scholar

[3]

N. Een and N. Sorensson. An extensible SAT-solver. In Proceedings of the InternationalConference on Theory and Applications of Satisflability Testing, volume 2919, pages 502–18. Springer, May 2003.

Google Scholar

[4]

Z. Huang, L. Wang, Y. Nasikovskiy, and A. Mishchenko. Fast Boolean matching based on NPN classification. In Proceedings of the 2013 International Conference on Field Programmable Technology, pages 310–13, Kyoto, Dec. 2013.

Google Scholar

[5]

D. E. Knuth. Fascicle 6: Satisfiability, volume 19 of The Art of Computer Programming. Addison-Wesley Reading, Mass., Dec. 2015.

Google Scholar

[6]

J. Marques-Silva, J. Argelich, A. Graca, and I. Lynce. Boolean lexicographic optimization: algorithms & applications. Annals of Mathematics and Artificial Intelligence, 62 (3): 317–43, May 2011.

Digital Library

Google Scholar

[7]

A. Nadel. Generating diverse solutions in SAT. In Proceedings of the InternationalConference on Theory and Applications of Satisflability Testing, pages 287–301, Ann Arbor, Mich., June 2011.

Google Scholar

[8]

A. Nadel and V. Ryvchin. Bit-vector optimization. In Proceedings of the 22nd InternationalConference on Tools and Algorithms for the Construction and Analysis of Systems, pages 851–67, Eindhoven, The Netherlands, Apr. 2016.

Google Scholar

[9]

A. Petkovska, A. Mishchenko, D. Novo, M. Owaida, and P. Ienne. Progressive generation of canonical sum of products using a SAT solver. In Proceedings of the 25th International Workshop on Logic and Synthesis, Austin, Tex., June 2016.

Google Scholar

[10]

M. Soeken, D. Große, A. Chandrasekharan, and R. Drechsler. BDD minimization for approximate computing. In Proceedings of the 21st Asia and South Pacific Design Automation Conference, pages 474–79, Macao, Jan. 2016.

Google Scholar

[11]

M. Soeken, A. Mishchenko, A. Petkovska, B. Sterin, P. Ienne, R. Brayton, and G. De Micheli. Heuristic NPN classification for large functions using AIGs and LEXSAT. In Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, Bordeaux, France, July 2016.

Google Scholar

[12]

G. S. Tseitin. On the complexity of derivation in propositional calculus. In Automation of Reasoning 2: Classical Papers on Computational Logic 19671970, Symbolic Computation, pages 466–83.Springer Berlin, 1983.

Google Scholar

[13]

R. Venkatesan, A. Agarwal, K. Roy, and A. Raghunathan. MACACO: Modeling and analysis of circuits for approximate computing. In Proceedings of the InternationalConference on Computer Aided Design, pages 667–73, San Jose, Calif., Nov. 2011.

Google Scholar

[14]

J. Yuan, A. Aziz, C. Pixley, and K. Albin. Simplifying Boolean constraint solving for random simulation-vector generation. IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 23 (3): 412–20, Mar. 2004.

Google Scholar

Cited By

View all

Cohen ANadel ARyvchin V(2021)Local Search with a SAT Oracle for Combinatorial OptimizationTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72013-1_5(87-104)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72013-1_5
Vasicek Z(2019)Formal Methods for Exact Analysis of Approximate CircuitsIEEE Access10.1109/ACCESS.2019.29586057(177309-177331)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2958605
Mishchenko ABrayton RPetkovska ASoeken MAmarú LDomic A(2018)Canonical computation without canonical representationProceedings of the 55th Annual Design Automation Conference10.1145/3195970.3196006(1-6)Online publication date: 24-Jun-2018
https://dl.acm.org/doi/10.1145/3195970.3196006
Show More Cited By

Index Terms

Fast generation of lexicographic satisfiable assignments: Enabling canonicity in SAT-based applications
1. Computing methodologies
  1. Artificial intelligence
    1. Search methodologies
2. Theory of computation
  1. Design and analysis of algorithms

Index terms have been assigned to the content through auto-classification.

Recommendations

A modular CNF-based SAT solver
SBCCI '10: Proceedings of the 23rd symposium on Integrated circuits and system design

The state-of-the-art SAT solvers, such as Chaff [11], zChaff [18], BerkMin [5], and Minisat [2] usually share the same core techniques, for instance: the watched literals structures conflict clause recording and non-chronological backtracking. ...
Hidden gold in random generation of SAT satisfiable instances
IJCAI'97: Proceedings of the 15th international joint conference on Artifical intelligence - Volume 1

Evaluation of incomplete algorithms that solve SAT requires to generate hard satisfiable instances. For that purpose, the kSAT uniform random generation is not usable. The other generators of satisfiable instances generate instances that are not ...
Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

We first introduce Abstract DPLL, a rule-based formulation of the Davis--Putnam--Logemann--Loveland (DPLL) procedure for propositional satisfiability. This abstract framework allows one to cleanly express practical DPLL algorithms and to formally reason ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

2016 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Nov 2016

946 pages

Publisher

IEEE Press

Publication History

Published: 07 November 2016

Permissions

Request permissions for this article.

Request Permissions

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
200
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 01 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Cohen ANadel ARyvchin V(2021)Local Search with a SAT Oracle for Combinatorial OptimizationTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-72013-1_5(87-104)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-72013-1_5
Vasicek Z(2019)Formal Methods for Exact Analysis of Approximate CircuitsIEEE Access10.1109/ACCESS.2019.29586057(177309-177331)Online publication date: 2019
https://doi.org/10.1109/ACCESS.2019.2958605
Mishchenko ABrayton RPetkovska ASoeken MAmarú LDomic A(2018)Canonical computation without canonical representationProceedings of the 55th Annual Design Automation Conference10.1145/3195970.3196006(1-6)Online publication date: 24-Jun-2018
https://dl.acm.org/doi/10.1145/3195970.3196006
Chandrasekharan AGroße DDrechsler RChandrasekharan AGroße DDrechsler R(2018)PreliminariesDesign Automation Techniques for Approximation Circuits10.1007/978-3-319-98965-5_2(11-25)Online publication date: 10-Oct-2018
https://doi.org/10.1007/978-3-319-98965-5_2
Nadel A(2018)Solving MaxSAT with Bit-Vector OptimizationTheory and Applications of Satisfiability Testing – SAT 201810.1007/978-3-319-94144-8_4(54-72)Online publication date: 26-Jun-2018
https://doi.org/10.1007/978-3-319-94144-8_4
Petkovska AMishchenko ANovo DOwaida MIenne P(2017)Progressive Generation of Canonical Irredundant Sums of Products Using a SAT SolverAdvanced Logic Synthesis10.1007/978-3-319-67295-3_8(169-188)Online publication date: 16-Nov-2017
https://doi.org/10.1007/978-3-319-67295-3_8

Abstract

8. References

Cited By

Index Terms

Recommendations

A modular CNF-based SAT solver

Hidden gold in random generation of SAT satisfiable instances

Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T)

Comments

Information

Published In

Publisher

Publication History

Permissions

Qualifiers

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

View options

Figures

Other

Share

Share this Publication link

Share on social media

Affiliations