More Web Proxy on the site http://driver.im/

research-article

Open access

Implementing Efficient All Solutions SAT Solvers

Authors:

Takehide SohAuthors Info & Claims

Journal of Experimental Algorithmics (JEA), Volume 21

Article No.: 1.12, Pages 1 - 44

https://doi.org/10.1145/2975585

Published: 04 November 2016 Publication History

Abstract

All solutions SAT (AllSAT for short) is a variant of the propositional satisfiability problem. AllSAT has been relatively unexplored compared to other variants despite its significance. We thus survey and discuss major techniques of AllSAT solvers. We accurately implemented them and conducted comprehensive experiments using a large number of instances and various types of solvers including a few publicly available software. The experiments revealed the solvers’ characteristics. We made our implemented solvers publicly available so that other researchers can easily develop their solvers by modifying our code and comparing it with existing methods.

References

[1]

Rakesh Agrawal, Tomasz Imieliński, and Arun Swami. 1993. Mining association rules between sets of items in large databases. SIGMOD Rec. 22, 2 (June 1993), 207--216.

Digital Library

[2]

Rakesh Agrawal and Ramakrishnan Srikant. 1994. Fast algorithms for mining association rules in large databases. In Proceedings of the 20th International Conference on Very Large Data Bases (VLDB’94). Morgan Kaufmann Publishers Inc., San Francisco, CA, 487--499. http://dl.acm.org/citation.cfm?id=645920.672836

Digital Library

[3]

Sheldon B. Akers. 1978. Binary decision diagrams. IEEE Trans. Comput. 27, 6 (June 1978), 509--516.

Digital Library

[4]

Fadi A. Aloul, Igor L. Markov, and Karem A. Sakallah. 2004. MINCE: A static global variable-ordering heuristic for SAT search and BDD manipulation. J. UCS 10, 12 (2004), 1562--1596.

[5]

Henrik Reif Andersen, Tarik Hadzic, John N. Hooker, and Peter Tiedemann. 2007. A constraint store based on multivalued decision diagrams. In Principles and Practice of Constraint Programming--CP 2007. Springer, Berlin, 118--132.

Digital Library

[6]

Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. 2003. Algorithms and complexity results for #SAT and Bayesian inference. In Proceedings of the 44th IEEE Annual Symposium on Foundations of Computer Science. IEEE Computer Society, Washington, DC, 340--351.

Digital Library

[7]

Roberto J. Bayardo, Jr. and Robert C. Schrag. 1997. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence and 9th Conference on Innovative Applications of Artificial Intelligence (AAAI’97/IAAI’97). AAAI Press, Providence, RI, 203--208. http://dl.acm.org/citation.cfm?id=1867406.1867438

Digital Library

[8]

Paul Beame, Russell Impagliazzo, Toniann Pitassi, and Nathan Segerlind. 2010. Formula caching in DPLL. ACM Trans. Comput. Theory 1, 3, Article 9 (March 2010), 33 pages.

Digital Library

[9]

Anton Belov, Daniel Diepold, Marijn J. H. Heule, and Matti Järvisalo (Eds.). 2014. Proceedings of SAT Competition 2014; Solver and Benchmark Descriptions. Department of Computer Science Series of Publications B, Vol. B-2014-2. University of Helsinki, Helsinki. http://hdl.handle.net/10138/135571

[10]

David Bergman, Andre A. Cire, Willem-Jan van Hoeve, and John N. Hooker. 2016. Discrete optimization with decision diagrams. INFORMS J. Comput. 28, 1 (2016), 47--66.

[11]

Armin Biere. 2008. PicoSAT essentials. JSAT 4, 2--4 (2008), 75--97. http://jsat.ewi.tudelft.nl/content/volume4/JSAT4_5_Biere.pdf.

[12]

Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. 1999. Symbolic model checking without BDDs. In Proceedings of the 5th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS’99). Springer-Verlag, London, UK, 193--207. http://dl.acm.org/citation.cfm?id=646483.691738

Digital Library

[13]

Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh. 2009. Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. IOS Press, Amsterdam, The Netherlands, The Netherlands.

Digital Library

[14]

Jörg Brauer, Andy King, and Jael Kriener. 2011. In Proceedings of the 23rd International Conference on Computer Aided Verification (CAV 2011). Springer, Berlin, 191--207.

[15]

Randal E. Bryant. 1986. Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C-35, 8 (Aug. 1986), 677--691.

Digital Library

[16]

Huan Chen and Joao Marques-Silva. 2009. TG-PRO: A new model for SAT-based ATPG. In Proceedings of the IEEE International High Level Design Validation and Test Workshop (HLDVT 2009). 76--81.

[17]

Xinguang Chen and Peter van Beek. 2001. Conflict-directed backjumping revisited. J. Artif. Int. Res. 14, 1 (March 2001), 53--81. http://dl.acm.org/citation.cfm?id=1622394.1622397

Digital Library

[18]

Edmund Clarke, Daniel Kroening, Natasha Sharygina, and Karen Yorav. 2004. Predicate abstraction of ANSI-C programs using SAT. Formal Meth. Syst. Des. 25, 2--3 (2004), 105--127.

Digital Library

[19]

Yves Crama and Peter L. Hammer. 2011. Boolean Functions—Theory, Algorithms, and Applications. Encyclopedia of mathematics and its applications, Vol. 142. Cambridge University Press, Cambridge. http://www.cambridge.org/gb/knowledge/isbn/item6222210/?site_locale=en_GB.

[20]

Adnan Darwiche. 2001. Decomposable negation normal form. J. ACM 48, 4 (2001), 608--647.

Digital Library

[21]

Adnan Darwiche. 2004. New advances in compiling CNF into decomposable negation normal form. In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI’2004), Including Prestigious Applicants of Intelligent Systems (PAIS 2004), Ramon López de Mántaras and Lorenza Saitta (Eds.). IOS Press, Valencia, Spain, 328--332.

Digital Library

[22]

Rina Dechter and Daniel Frost. 2002. Backjump-based backtracking for constraint satisfaction problems. Artif. Intell. 136, 2 (2002), 147--188.

Digital Library

[23]

Niklas Eén and Niklas Sörensson. 2003. An extensible SAT-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing, (SAT 2003), Selected Revised Papers, Lecture Notes in Computer Science, Vol. 2919, Enrico Giunchiglia and Armando Tacchella (Eds.). Springer, Berlin, 502--518.

[24]

Thomas Eiter, Kazuhisa Makino, and Georg Gottlob. 2008. Computational aspects of monotone dualization: A brief survey. Discrete Appl. Math. 156, 11 (2008), 2035--2049. In Memory of Leonid Khachiyan (1952--2005).

Digital Library

[25]

Andrew Gainer-Dewar and Paola Vera-Licona. 2016. The minimal hitting set generation problem: Algorithms and computation. CoRR abs/1601.02939 (2016). http://arxiv.org/abs/1601.02939

[26]

Malay Kumar Ganai, Aarti Gupta, and Pranav Ashar. 2004. Efficient SAT-based unbounded symbolic model checking using circuit cofactoring. In Proceedings of the IEEE/ACM International Conference on Computer Aided Design (ICCAD’04). IEEE Computer Society, Washington, DC, 510--517.

Digital Library

[27]

Martin Gebser, Benjamin Kaufmann, André Neumann, and Torsten Schaub. 2007. In Proceedings of the 9th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2007). Springer, Berlin, 260--265.

Digital Library

[28]

Martin Gebser, Benjamin Kaufmann, and Torsten Schaub. 2009. Solution enumeration for projected boolean search problems. In Proceedings of the 6th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR’09). Springer-Verlag, Berlin, 71--86.

Digital Library

[29]

Orna Grumberg, Assaf Schuster, and Avi Yadgar. 2004. In Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2004). Springer, Berlin, 275--289.

[30]

Tias Guns, Siegfried Nijssen, and Luc De Raedt. 2011. Itemset mining: A constraint programming perspective. Artif. Intell. 175, 1213 (2011), 1951--1983.

Digital Library

[31]

Aarti Gupta, Zijiang Yang, Pranav Ashar, and Anubhav Gupta. 2000. Formal Methods in Computer-Aided Design: Third International Conference, FMCAD 2000 Austin, TX, USA, November 1--3, 2000 Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, Chapter SAT-Based Image Computation with Application in Reachability Analysis, 391--408.

Digital Library

[32]

Jiawei Han, Hong Cheng, Dong Xin, and Xifeng Yan. 2007. Frequent pattern mining: Current status and future directions. Data Mining Knowl. Disc. 15, 1 (2007), 55--86.

Digital Library

[33]

Hoos H. Holger and T. Stützle. 2000. SATLIB: An online resource for research on SAT. In Proceedings of the 4th International Conference on Theory and Applications of Satisfiability Testing (SAT 2000), Ian Gent, Hans van Maaren, and Toby Walsh (Eds.), Vol. 63. IOS Press, 283--292.

[34]

John N. Hooker. 2013. In Proceedings of the 10th International Conference on Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems (CPAIOR 2013). Springer, Berlin, 94--110.

[35]

Jinbo Huang and Adnan Darwiche. 2005. In Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Revised Selected Papers. Springer, Berlin, 157--172.

Digital Library

[36]

Jinbo Huang and Adnan Darwiche. 2007. The language of search. J. Artif. Intell. Res. (JAIR) 29 (2007), 191--219.

Digital Library

[37]

Takeru Inoue, Keiji Takano, Takayuki Watanabe, Jun Kawahara, Ryo Yoshinaka, Akihiro Kishimoto, Koji Tsuda, Shin-ichi Minato, and Yasuhiro Hayashi. 2014. Distribution loss minimization with guaranteed error bound. IEEE Trans. Smart Grid 5, 1 (Jan. 2014), 102--111.

[38]

Takeru Inoue, Norihito Yasuda, Shunsuke Kawano, Yuji Takenobu, Shin-ichi Minato, and Yasuhiro Hayashi. 2015. Distribution network verification for secure restoration by enumerating all critical failures. IEEE Trans. Smart Grid 6, 2 (March 2015), 843--852.

[39]

Saïd Jabbour, Jerry Lonlac, Lakhdar Sais, and Yakoub Salhi. 2014a. Extending modern SAT solvers for models enumeration. In Proceedings of the 15th IEEE International Conference on Information Reuse and Integration (IRI 2014). IEEE Computer Society, Washington, DC, 803--810.

[40]

Saïd Jabbour, Joao Marques-Silva, Lakhdar Sais, and Yakoub Salhi. 2014b. In Proceedings of the 14th European Conference on Logics in Artificial Intelligence (JELIA 2014). Springer International Publishing, Cham, 152--165.

[41]

Saïd Jabbour, Lakhdar Sais, and Yakoub Salhi. 2013. Boolean satisfiability for sequence mining. In Proceedings of the 22nd ACM International Conference on Conference on Information; Knowledge Management (CIKM’13). ACM, New York, NY, 649--658.

Digital Library

[42]

Karthick Jayaraman, Nikolaj Bjørner, Geoff Outhred, and Charlie Kaufman. 2014. Automated Analysis and Debugging of Network Connectivity Policies. Technical Report MSR-TR-2014-102. Microsoft Research. http://research.microsoft.com/apps/pubs/default.aspx?id=225826.

[43]

HoonSang Jin, HyoJung Han, and Fabio Somenzi. 2005. In Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2005). Springer, Berlin, 287--300.

[44]

HoonSang Jin and Fabio Somenzi. 2005. Prime clauses for fast enumeration of satisfying assignments to boolean circuits. In Proceedings of the 42nd Annual Design Automation Conference (DAC’05). ACM, New York, NY, 750--753.

Digital Library

[45]

David J. Johnson and Michael A. Trick (Eds.). 1996. Cliques, Coloring, and Satisfiability: Second DIMACS Implementation Challenge, 1993. American Mathematical Society, Boston, MA.

[46]

Roberto J. Bayardo, Jr. and Joseph Daniel Pehoushek. 2000. Counting models using connected components. In Proceedings of the 17th National Conference on Artificial Intelligence and 12th Conference on on Innovative Applications of Artificial Intelligence, 2000, Henry A. Kautz and Bruce W. Porter (Eds.). AAAI Press/The MIT Press, Austin, Texas, 157--162. http://www.aaai.org/Library/AAAI/2000/aaai00-024.php.

Digital Library

[47]

Hyeong-Ju Kang and In-Cheol Park. 2005. SAT-based unbounded symbolic model checking. IEEE Trans. Comput.-Aided Design Integr. Circ. Syst. 24, 2 (Feb. 2005), 129--140.

Digital Library

[48]

Donald E. Knuth. 2011. The Art of Computer Programming: Combinatorial Algorithms, Part 1 (1st ed.). Addison-Wesley Professional, Upper Saddle River, NJ.

Digital Library

[49]

Jean-Marie Lagniez and Pierre Marquis. 2016. On preprocessing techniques and their impact on propositional model counting. J. Automat. Reason. (2016), 1--69.

[50]

Shuvendu K. Lahiri, Randal E. Bryant, and Byron Cook. 2003. A Symbolic Approach to Predicate Abstraction. Springer, Berlin, 141--153.

[51]

Shuvendu K. Lahiri, Robert Nieuwenhuis, and Albert Oliveras. 2006. SMT Techniques for Fast Predicate Abstraction. Springer, Berlin, 424--437.

Digital Library

[52]

C. Y. Lee. 1959. Representation of switching circuits by binary-decision programs. Bell Syst. Tech. J. 38, 4 (1959), 985--999.

[53]

Bin Li, Michael S. Hsiao, and Shuo Sheng. 2004. A novel SAT all-solutions solver for efficient preimage computation. In Proceedings of the 2004 Design, Automation and Test in Europe Conference and Exposition (DATE 2004). IEEE Computer Society, Washington, DC, 272--279.

Digital Library

[54]

Nuno Lopes, Nikolaj Bjørner, Patrice Godefroid, and George Varghese. 2013. Network Verification in the Light of Program Verification. Technical Report. Microsoft Research. http://research.microsoft.com/apps/pubs/default.aspx?id=201589.

[55]

Nuno P. Lopes, Nikolaj Bjørner, Patrice Godefroid, Karthick Jayaraman, and George Varghese. 2015. Checking beliefs in dynamic networks. In Proceedings of the 12th USENIX Conference on Networked Systems Design and Implementation (NSDI’15). USENIX Association, Berkeley, CA, 499--512. http://dl.acm.org/citation.cfm?id=2789770.2789805

Digital Library

[56]

Stephen M. Majercik and Michael L. Littman. 1998. Using caching to solve larger probabilistic planning problems. In Proceedings of the 15th National Conference on Artificial Intelligence and 10th Innovative Applications of Artificial Intelligence Conference (AAAI’98), Jack Mostow and Chuck Rich (Eds.). AAAI Press/The MIT Press, Madison, Wisconsin, 954--959. http://www.aaai.org/Library/AAAI/1998/aaai98-135.php.

Digital Library

[57]

Sharad Malik and Lintao Zhang. 2009. Boolean satisfiability from theoretical hardness to practical success. Commun. ACM 52, 8 (Aug. 2009), 76--82.

Digital Library

[58]

Joao Marques-Silva and Karem A. Sakallah. 1999. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 5 (May 1999), 506--521.

Digital Library

[59]

Ken L. McMillan. 2002. In Proceedings of the 14th International Conference on Computer Aided Verification (CAV 2002). Springer, Berlin, 250--264.

[60]

Shin-ichi Minato. 2013. Techniques of BDD/ZDD: Brief history and recent activity. IEICE Transactions on Information and Systems 96-D, 7 (2013), 1419--1429. http://search.ieice.org/bin/summary.php?id=e96-d_7_1419.

[61]

António Morgado and Joao Marques-Silva. 2005. Good learning and implicit model enumeration. In Proceedings of the 17th IEEE International Conference on Tools with Artificial Intelligence (ICTAI’05). IEEE Computer Society, Washington, DC, 131--136.

Digital Library

[62]

DoRon B. Motter and Igor L. Markov. 2002. In Proceedings of the 4th International Workshop on Algorithm Engineering and Experiments. Revised Papers. Springer, Berlin, 29--42.

[63]

Keisuke Murakami and Takeaki Uno. 2014. Efficient algorithms for dualizing large-scale hypergraphs. Discrete Appl. Math. 170 (2014), 83--94.

Digital Library

[64]

Knot Pipatsrisawat and Adnan Darwiche. 2007. A lightweight component caching scheme for satisfiability solvers. In Proceedings of the 10th International Conference on Theory and Applications of Satisfiability Testing (SAT 2007), Lecture Notes in Computer Science, Vol. 4501, João Marques-Silva and Karem A. Sakallah (Eds.). Springer, Berlin, 294--299.

Digital Library

[65]

Patrick Prosser. 1993. Hybrid algorithms for the constraint satisfaction problem. Comput. Intell. 9 (1993), 268--299.

[66]

Junaid Qadir and Osman Hasan. 2015. Applying formal methods to networking: Theory, techniques, and applications. IEEE Commun. Surv. Tutorials. 17, 1 (First quarter 2015), 256--291.

[67]

Kavita Ravi and Fabio Somenzi. 2004. In Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004), held as part of the Joint European Conferences on Theory and Practice of Software (ETAPS 2004). Springer, Berlin, 31--45.

[68]

Kyoko Sekine. 1997. Algorithm for Computing the Tutte Polynomial and Its Applications. Ph.D. dissertation. Department of Information Science, University of Tokyo.

[69]

Kyoko Sekine and Hiroshi Imai. 1995. A Unified Approach via BDD to the Network Reliability and Path Numbers. Technical Report. Department of Information Science, University of Tokyo.

[70]

Kyoko Sekine, Hiroshi Imai, and Seiichiro Tani. 1995. In Proceedings of the 6th International Symposium on Algorithms and Computations (ISAAC’95). Springer Berlin, 224--233.

Digital Library

[71]

Shuo Sheng and Michael Hsiao. 2003. Efficient preimage computation using a novel success-driven ATPG. In Proceedings of the Conference on Design, Automation and Test in Europe (2003). IEEE Computer Society, Washington, DC, 822--827.

Digital Library

[72]

Carsten Sinz. 2005. Towards an optimal CNF encoding of boolean cardinality constraints. In Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming (CP 2005), Peter van Beek (Ed.). Springer, Berlin, 827--831.

Digital Library

[73]

Marc Thurley. 2006. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT 2006). Springer, Berlin, 424--429.

Digital Library

[74]

Takahisa Toda. 2013. In Proceedings of the 12th International Symposium on Experimental Algorithms (SEA 2013). Springer, Berlin, 91--102.

[75]

Takahisa Toda. 2016. Dualization of boolean functions using ternary decision diagrams. Ann. Math. Artif. Intell. (2016), 1--16.

[76]

Takahisa Toda and Koji Tsuda. 2015. BDD construction for all solutions SAT and efficient caching mechanism. In Proceedings of the 30th Annual ACM Symposium on Applied Computing (SAC’15). ACM, New York, NY, 1880--1886.

Digital Library

[77]

Takeaki Uno, Masashi Kiyomi, and Hiroki Arimura. 2004. LCM ver. 2: Efficient mining algorithms for frequent/closed/maximal itemsets. In Proceedings of the IEEE ICDM Workshop on Frequent Itemset Mining Implementations (FIMI’04) (CEUR Workshop Proceedings), Roberto J. Bayardo, Jr., Bart Goethals, and Mohammed Javeed Zaki (Eds.), Vol. 126. CEUR-WS.org. http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-126/uno.pdf.

[78]

Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter. 2007. Handbook of Knowledge Representation. Elsevier Science, San Diego.

Digital Library

[79]

Yinlei Yu, Pramod Subramanyan, Nestan Tsiskaridze, and Sharad Malik. 2014. All-SAT using minimal blocking clauses. In Proceedings of the 27th International Conference on VLSI Design and 13th International Conference on Embedded Systems. IEEE Computer Society, Washington, DC, 86--91.

Digital Library

[80]

Shuyuan Zhang, Sharad Malik, and Rick McGeer. 2012. In Proceedings of the 10th International Symposium on Automated Technology for Verification and Analysis. Springer, Berlin, 1--16.

Cited By

Boege TBolt JStudený M(2025)Self-adhesivity in lattices of abstract conditional independence modelsDiscrete Applied Mathematics10.1016/j.dam.2024.10.006361:C(196-225)Online publication date: 30-Jan-2025
https://dl.acm.org/doi/10.1016/j.dam.2024.10.006
Lagniez JLonca EMarquis POrtiz MPagnucco M(2024)Leveraging decision-DNNF compilation for enumerating disjoint partial modelsProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning10.24963/kr.2024/48(509-519)Online publication date: 2-Nov-2024
https://dl.acm.org/doi/10.24963/kr.2024/48
Spallitta GSebastiani RBiere AWooldridge MDy JNatarajan S(2024)Disjoint partial enumeration without blocking clausesProceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v38i8.28652(8126-8135)Online publication date: 20-Feb-2024
https://dl.acm.org/doi/10.1609/aaai.v38i8.28652
Show More Cited By

Index Terms

Implementing Efficient All Solutions SAT Solvers

Recommendations

CDCL(Crypto) SAT solvers for cryptanalysis
CASCON '19: Proceedings of the 29th Annual International Conference on Computer Science and Software Engineering

Over the last two decades we have seen a dramatic improvement in the efficiency of conflict-driven clause-learning Boolean satisfiability (CDCL SAT) solvers on industrial problems from a variety of domains. The availability of such a powerful general-...
Enhancing Clause Learning by Symmetry in SAT Solvers
ICTAI '10: Proceedings of the 2010 22nd IEEE International Conference on Tools with Artificial Intelligence - Volume 01

The satisfiability problem (SAT) is shown to be the first decision NP-complete problem. It is central in complexity theory. A CNF formula usually contains an interesting number of symmetries. That is, the formula remains invariant under some variable ...
Clause vivification by unit propagation in CDCL SAT solvers
Abstract
Original and learnt clauses in Conflict-Driven Clause Learning (CDCL) SAT solvers often contain redundant literals. This may have a negative impact on solver performance, because redundant literals may deteriorate both the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Journal of Experimental Algorithmics

ACM Journal of Experimental Algorithmics Volume 21, Issue

Special Issue SEA 2014, Regular Papers and Special Issue ALENEX 2013

2016

404 pages

ISSN:1084-6654

EISSN:1084-6654

DOI:10.1145/2888418

Issue’s Table of Contents

Copyright © 2016 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 November 2016

Accepted: 01 July 2016

Revised: 01 May 2016

Received: 01 September 2015

Published in JEA Volume 21

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

JSPS KAKENHI

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

44
Total Citations
View Citations
2,985
Total Downloads

Downloads (Last 12 months)325
Downloads (Last 6 weeks)49

Reflects downloads up to 02 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Boege TBolt JStudený M(2025)Self-adhesivity in lattices of abstract conditional independence modelsDiscrete Applied Mathematics10.1016/j.dam.2024.10.006361:C(196-225)Online publication date: 30-Jan-2025
https://dl.acm.org/doi/10.1016/j.dam.2024.10.006
Lagniez JLonca EMarquis POrtiz MPagnucco M(2024)Leveraging decision-DNNF compilation for enumerating disjoint partial modelsProceedings of the 21st International Conference on Principles of Knowledge Representation and Reasoning10.24963/kr.2024/48(509-519)Online publication date: 2-Nov-2024
https://dl.acm.org/doi/10.24963/kr.2024/48
Spallitta GSebastiani RBiere AWooldridge MDy JNatarajan S(2024)Disjoint partial enumeration without blocking clausesProceedings of the Thirty-Eighth AAAI Conference on Artificial Intelligence and Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence and Fourteenth Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v38i8.28652(8126-8135)Online publication date: 20-Feb-2024
https://dl.acm.org/doi/10.1609/aaai.v38i8.28652
Datta RZhao GJain DShamsi K(2024)On Hardware Trojan Detection using Oracle-Guided Circuit LearningProceedings of the Great Lakes Symposium on VLSI 202410.1145/3649476.3658705(198-203)Online publication date: 12-Jun-2024
https://dl.acm.org/doi/10.1145/3649476.3658705
Shi JYang ZKang HXu BHe JLo DRoychoudhury PPaiva AAbreu RStorey MSharif BXia X(2024)Greening Large Language Models of CodeProceedings of the 46th International Conference on Software Engineering: Software Engineering in Society10.1145/3639475.3640097(142-153)Online publication date: 14-Apr-2024
https://dl.acm.org/doi/10.1145/3639475.3640097
Oparin GBogdanova VPashinin A(2024)Dynamics of Bipartite Logical Networks2024 47th MIPRO ICT and Electronics Convention (MIPRO)10.1109/MIPRO60963.2024.10569248(13-18)Online publication date: 20-May-2024
https://doi.org/10.1109/MIPRO60963.2024.10569248
Bombarda AGargantini A(2024)Design, implementation, and validation of a benchmark generator for combinatorial interaction testing toolsJournal of Systems and Software10.1016/j.jss.2023.111920209(111920)Online publication date: Mar-2024
https://doi.org/10.1016/j.jss.2023.111920
Tang ZLi CYou HLiu XWang YDai YBai GLin X(2023)Logical Resolving-Based Methodology for Efficient Reliability AnalysisMicromachines10.3390/mi1501008515:1(85)Online publication date: 30-Dec-2023
https://doi.org/10.3390/mi15010085
Miller HWilliams BChen YNeville J(2023)Counting knot mosaics with ALLSAT (student abstract)Proceedings of the Thirty-Seventh AAAI Conference on Artificial Intelligence and Thirty-Fifth Conference on Innovative Applications of Artificial Intelligence and Thirteenth Symposium on Educational Advances in Artificial Intelligence10.1609/aaai.v37i13.27002(16284-16285)Online publication date: 7-Feb-2023
https://dl.acm.org/doi/10.1609/aaai.v37i13.27002
Xue YJin DHerlihy M(2023)Invited Paper: Fault-tolerant and Expressive Cross-Chain SwapsProceedings of the 24th International Conference on Distributed Computing and Networking10.1145/3571306.3571388(28-37)Online publication date: 4-Jan-2023
https://dl.acm.org/doi/10.1145/3571306.3571388
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Figures

Tables

Media

View Issue’s Table of Contents