Click to open the HelpDesk interface
AECE - Front page banner

Menu:


FACTS & FIGURES

JCR Impact Factor: 0.459
JCR 5-Year IF: 0.442
Issues per year: 4
Current issue: Nov 2016
Next issue: Feb 2017
Avg review time: 78 days


PUBLISHER

Stefan cel Mare
University of Suceava
Faculty of Electrical Engineering and
Computer Science
13, Universitatii Street
Suceava - 720229
ROMANIA

Print ISSN: 1582-7445
Online ISSN: 1844-7600
WorldCat: 643243560
doi: 10.4316/AECE


TRAFFIC STATS

1,529,665 unique visits
477,921 downloads
Since November 1, 2009



No robots online now


SJR SCImago RANK

SCImago Journal & Country Rank


SEARCH ENGINES

aece.ro - Google Pagerank




TEXT LINKS

Anycast DNS Hosting
MOST RECENT ISSUES

 Volume 16 (2016)
 
     »   Issue 4 / 2016
 
     »   Issue 3 / 2016
 
     »   Issue 2 / 2016
 
     »   Issue 1 / 2016
 
 
 Volume 15 (2015)
 
     »   Issue 4 / 2015
 
     »   Issue 3 / 2015
 
     »   Issue 2 / 2015
 
     »   Issue 1 / 2015
 
 
 Volume 14 (2014)
 
     »   Issue 4 / 2014
 
     »   Issue 3 / 2014
 
     »   Issue 2 / 2014
 
     »   Issue 1 / 2014
 
 
 Volume 13 (2013)
 
     »   Issue 4 / 2013
 
     »   Issue 3 / 2013
 
     »   Issue 2 / 2013
 
     »   Issue 1 / 2013
 
 
  View all issues  


FEATURED ARTICLE

ABC Algorithm based Fuzzy Modeling of Optical Glucose Detection, SARACOGLU, O. G., BAGIS, A., KONAR, M., TABARU, T. E.
Issue 3/2016

AbstractPlus


SAMPLE ARTICLES

FEM Analysis of Brushless DC Servomotor with Fractional Number of Slots per Pole, BALUTA, G., GRAUR, A., PENTIUC, R., DIACONESCU, C., POPA, C.
Issue 1/2014

AbstractPlus

Controller Architecture Design for MMC-HVDC, ZHANG, B., ZHAO, C., GUO, C., XIAO, X., ZHOU, L.
Issue 2/2014

AbstractPlus

Post-error Correction in Automatic Speech Recognition Using Discourse Information, KANG, S., KIM, J.-H., SEO, J.
Issue 2/2014

AbstractPlus

Pipelined Error-detecting Codes in FPGA Testing, BREKHOV, O., RATNIKOV, M.
Issue 2/2014

AbstractPlus

An Ink-Jet Printed Capacitive Sensor for Angular Position/Velocity Measurements, KRKLJES, D. B., STOJANOVIC, G. M.
Issue 4/2016

AbstractPlus

A Novel Approach to Fault Detection in Complex Electric Power Systems, ZHANG, Y., WANG, Z.
Issue 3/2014

AbstractPlus




LATEST NEWS

2017-Feb-16
With new technologies, such as mobile communications, internet of things, and wide applications of social media, organizations generate a huge volume of data, much faster than several years ago. Big data, characterized by high volume, diversity and velocity, increasingly drives decision making and is changing the landscape of business intelligence, from governments to private organizations, from communities to individuals. Big data analytics that discover insights from evidences has a high demand for computing efficiency, knowledge discovery, problem solving, and event prediction. We dedicate a special section of Issue 4/2017 to Big Data. Prospective authors are asked to make the submissions for this section no later than the 31st of May 2017, placing "Big Data - " before the paper title in OpenConf.

2017-Jan-30
We have the confirmation Advances in Electrical and Computer Engineering will be included in the Gale database.

2016-Dec-17
IoT is a new emerging technology domain which will be used to connect all objects through the Internet for remote sensing and control. IoT uses a combination of WSN (Wireless Sensor Network), M2M (Machine to Machine), robotics, wireless networking, Internet technologies, and Smart Devices. We dedicate a special section of Issue 2/2017 to IoT. Prospective authors are asked to make the submissions for this section no later than the 31st of March 2017, placing "IoT - " before the paper title in OpenConf.

2016-Jun-14
Thomson Reuters published the Journal Citations Report for 2015. The JCR Impact Factor of Advances in Electrical and Computer Engineering is 0.459, and the JCR 5-Year Impact Factor is 0.442.

2015-Dec-04
Starting with Issue 2/2016, the article processing charge is 300 EUR for each article accepted for publication. The charge of 25 EUR per page for papers over 8 pages will not be changed. Details are available in the For authors section.

Read More »


    
 

  3/2016 - 13

Back to Basics: Solving Games with SAT

QUER, S. See more information about QUER, S. on SCOPUS See more information about QUER, S. on IEEExplore See more information about QUER, S. on Web of Science
 
Click to see author's profile on See more information about the author on SCOPUS SCOPUS, See more information about the author on IEEE Xplore IEEE Xplore, See more information about the author on Web of Science Web of Science

Download PDF pdficon (1,045 KB) | Citation | Downloads: 87 | Views: 270

Author keywords
artificial intelligence, algorithm design and analysis, boolean algebra, formal verification, partitioning algorithms

References keywords
satisfiability(7), verification(4), solving(4), intelligence(4), design(4), artificial(4), aided(4)
Blue keywords are present in both the references section and the paper title.

About this article
Date of Publication: 2016-08-31
Volume 16, Issue 3, Year 2016, On page(s): 91 - 98
ISSN: 1582-7445, e-ISSN: 1844-7600
Digital Object Identifier: 10.4316/AECE.2016.03013
Web of Science Accession Number: 000384750000013
SCOPUS ID: 84991056316

Abstract
Quick view
Full text preview
Games became popular, within the formal verification community, after their application to automatic synthesis of circuits from specifications, and they have been receiving more and more attention since then. This paper focuses on coding the Sokoban puzzle, i.e., a very complex single-player strategy game. We show how its solution can be encoded and represented as a Bounded Model Checking problem, and then solved with a SAT solver. After that, to cope with very complex instances of the game, we propose two different ad-hoc divide-and-conquer strategies. Those strategies, somehow similar to state-of-the-art abstraction-and-refinement schemes, are able to decompose deep Bounded Model Checking instances into easier subtasks, trading-off between efficiency and completeness. We analyze a vast set of difficult hard-to-solve benchmark games, trying to push forward the applicability of state-of-the-art SAT solvers in the field. Those results show that games may provide one of the next frontier for the SAT community.


References | Cited By  «-- Click to see who has cited this paper

[1] A. Church, "Logic, arithmetic, and automata," International congress of mathematicians, Djursholm, Sweden, pp. 23-35, August 1963.
[CrossRef]


[2] P. J. G. Ramadge and W. M. Wonham, "The control of discrete event systems," Proceeding of the IEEE, 77(1), pp. 81-98, January 1989.
[CrossRef] [Web of Science Times Cited 1160] [SCOPUS Times Cited 1538]


[3] T. Wolfgang, "Infinite games and verification," in Ed Brinksma and Kim Guldstrand Larsen editors, in Proceedings of the Computer Aided Verification Confernce (CAV), London, UK, Springer, pp. 58-64, September 2002.
[CrossRef]


[4] H. Kautz and B. Selman, "Planning as satisfiability," in Proceedings of the 10th European Conference on Artificial Intelligence (ECAI’92), Vienna, Austria, John Wiley & Sons Inc. publisher, New York, NY, USA, pp. 359-363, 1992. ISBN: 0-471-93608-1

[5] W. Thomas, "Infinite games and verification," in Ed Brinksma and Kim Guldstrand Larsen editors, in Proceedings of the Computer Aided Verification Conference (CAV), volume 2102 of LNCS, Springer-Verlag, Copenhagen, Denmark, pp. 58-64, July 2002.
[CrossRef]


[6] R. Alur, P. Madhusudan, and W. Nam, "Symbolic computational techniques for solving games," International Journal on Software Tools for Technology Transfer (STTT), pp. 118-128, January 2005.
[CrossRef] [SCOPUS Times Cited 4]


[7] I. P. Gent and A. G. D. Rowley, "Encoding connect-4 using quantified Boolean formulae," in Proceedings of the 2nd International Workshop on Modelling and Reformulating Constraint Satisfaction Problems, Kinsale, Ireland, pp. 78-93, 2003.
[CrossRef]


[8] C. Ansotegui, C. P. Gomes, and B. Selman, "The Achilles' heel of QBF," in Proceedings of the 20th National Conference on Artificial Intelligence (AAAI’05), Pittsburg, Pennsylvania, AAAI Press, pp. 275-281. July 2005. ISBN: 1-57735-236-x.
[CrossRef]


[9] I. Lynce and J. Ouaknine, "Sudoku as a SAT problem," in Proceedings of the 9th International Symposium on Artificial Intelligence and Mathematics, Fort Lauderdale, Florida, January 2006.
[CrossRef]


[10] A. Sabharwal, C. Ansňtegui, C. P. Gomes, J. W. Hart, and B. Selman, "QBF modeling: exploiting player symmetry for simplicity and efficiency," in Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT’06), volume 4121 of LNCS, Springer-Verlag, Seattle, Washington, pp. 382-395, August 2006.
[CrossRef]


[11] J. P. Marques-Silva and K. A. Sakallah, "GRASP - a new search algorithm for satisfiability," in Proceedings of the International Conference on Computer Aided Design (ICCAD), November 1996.
[CrossRef]


[12] H. Jin and F. Somenzi, "CirCUs: a hybrid satisfiability solver," in Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, Vancouver, BC, Canada, May 2004.
[CrossRef]


[13] T. Walsh, C. Thiffault, and F. Bacchus, "Solving non-clausal formulas with DPLL search," in Proceedings of the International Conference on Theory and Applications of Satisfiability Testing, volume 2919 of LNCS, Springer-Verlag, pp. 663-678, 2004.
[CrossRef]


[14] L. Zhang, "Solving QBF with combined conjunctive and disjunctive normal form," in Proceedings of the 21th National Conference on Artificial Intelligence (AAAI’06), Boston, Massachusetts, AAAI Press, pp. 143-149, 2006. ISBN: 978-1-57735-281-5.
[CrossRef]


[15] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, " Symbolic model checking using SAT procedures instead of BDDs," in Proceedings of the 36th Design Automation Conference, New Orleans, Louisiana, IEEE Computer Society, pp. 317-320, June 1999.
[CrossRef]


[16] J. Whittemore, J. Kim, and K. Sakallah, "SATIRE: a new incremental satisfiability engine," in Proceedings of the 38th Design Automation Conference, New York, NY, USA, ACM Press, pp. 542-545, June 2001. ISBN: 1-58113-297-2.
[CrossRef]


[17] N. Een and N. Sorensson, "Temporal induction by incremental SAT solving," in First International Workshop on Bounded Model Checking (BMC’03), Boulder, Colorado, pp. 58-64, July 2003.
[CrossRef] [SCOPUS Times Cited 144]


[18] H. Cho, G. D. Hatchel, E. Macii, B. Plessier, and F. Somenzi, "Algorithms for approximate FSM traversal based on state space decomposition," IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, 15(12), pp. 1465-1478, 1996.
[CrossRef] [Web of Science Times Cited 26] [SCOPUS Times Cited 32]




References Weight

Web of Science® Citations for all references: 1,186 TCR
SCOPUS® Citations for all references: 1,718 TCR

Web of Science® Average Citations per reference: 62 ACR
SCOPUS® Average Citations per reference: 90 ACR

TCR = Total Citations for References / ACR = Average Citations per Reference

We introduced in 2010 - for the first time in scientific publishing, the term "References Weight", as a quantitative indication of the quality ... Read more

Citations for references background updated on 2017-02-19 15:14 in 103 seconds.




Note1: Web of Science® is a registered trademark of Thomson Reuters.
Note2: SCOPUS® is a registered trademark of Elsevier B.V.
Disclaimer: All queries to the respective databases were made by using the DOI record of every reference (where available). Due to technical problems beyond our control, the information is not always accurate. Please use the CrossRef link to visit the respective publisher site.

Copyright ©2001-2017
Faculty of Electrical Engineering and Computer Science
Stefan cel Mare University of Suceava, Romania


All rights reserved: Advances in Electrical and Computer Engineering is a registered trademark of the Stefan cel Mare University of Suceava. No part of this publication may be reproduced, stored in a retrieval system, photocopied, recorded or archived, without the written permission from the Editor. When authors submit their papers for publication, they agree that the copyright for their article be transferred to the Faculty of Electrical Engineering and Computer Science, Stefan cel Mare University of Suceava, Romania, if and only if the articles are accepted for publication. The copyright covers the exclusive rights to reproduce and distribute the article, including reprints and translations.

Permission for other use: The copyright owner's consent does not extend to copying for general distribution, for promotion, for creating new works, or for resale. Specific written permission must be obtained from the Editor for such copying. Direct linking to files hosted on this website is strictly prohibited.

Disclaimer: Whilst every effort is made by the publishers and editorial board to see that no inaccurate or misleading data, opinions or statements appear in this journal, they wish to make it clear that all information and opinions formulated in the articles, as well as linguistic accuracy, are the sole responsibility of the author.




Website loading speed and performance optimization powered by: