Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 15

Proceedings of the 2018 Federated Conference on Computer Science and Information Systems

Visualization of logical formulas

DOI: http://dx.doi.org/10.15439/2018F264

Citation: Proceedings of the 2018 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 15, pages 419424 ()

Full text

Abstract. Visualization of logical formulas for classical propositional calculus gains a new meaning in the context of a huge development of SAT solvers which find solutions of satisfiability problems of bigger and more complex tasks including the ones of industrial meaning. The aim of this work is to create, using modern IT tools, a coherent and widely accessible system in a form of web application, which will be able to provide a coopertive system, as well as will help to visualize, analyze and transform logical formulas. The system itself is now in the initial, however, mature implementation phase. It is open for new ideas and methods. New functionalities have already been introduced but there are plans to create the new ones.


  1. A. Biere, M. Heule, H. van Maaren, and T. Walsh, Handbook of Satisfiability: Volume 185 Frontiers in Artificial Intelligence and Applications. Amsterdam, The Netherlands, The Netherlands: IOS Press, 2009.
  2. R. Klimek, “Exploration of human activities using message streaming brokers and automated logical reasoning for ambient-assisted services,” IEEE Access, vol. 6, pp. 27 127–27 155, 2018.
  3. C. P. Gomes, H. A. Kautz, A. Sabharwal, and B. Selman, “Satisfiability solvers,” in Handbook of Knowledge Representation, ser. Foundations of Artificial Intelligence, F. van Harmelen, V. Lifschitz, and B. W. Porter, Eds. Elsevier, 2008, vol. 3, pp. 89–134.
  4. D. E. Knuth, The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability, 1st ed. Addison-Wesley Professional, 2015.
  5. P. Baranowski, “System for visualization of logical formulas, Engineering diploma thesis, supervisor: Radosław Klimek, AGH University of Science and Technology,” 2018.
  6. C. Sinz, “Visualizing SAT Instances and Runs of the DPLL Algorithm,” Journal of Automated Reasoning, vol. 39, no. 2, pp. 219–243, Aug. 2007. [Online]. Available: http://dx.doi.org/10.1007/s10817-007-9074-1
  7. N. Eén and A. Biere, “Effective preprocessing in sat through variable and clause elimination,” in Theory and Applications of Satisfiability Testing, F. Bacchus and T. Walsh, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2005, pp. 61–75.
  8. T. Christie, “Website: Django rest framework,” 2018, accessed on 6-Jan-2018. [Online]. Available: http://www.django-rest-framework.org/
  9. Celery Development Team, “Website: Celery: Distributed task queue,” 2018, accessed on 6-Jan-2018. [Online]. Available: http://www.celeryproject.org/
  10. Rabbit Technologies Ltd., “Website: RabbitMQ documentation,” 2018, accessed on 7-Feb-2018. [Online]. Available: https://www.rabbitmq.com/documentation.html
  11. vis.js Development Team, “Website: vis.js. dynamic browser based visualization library,” 2018, accessed on 6-Jan-2018. [Online]. Available: http://visjs.org/
  12. NGINX Development Team, “Website: Nginx products,” 2018, accessed on 6-Jan-2018. [Online]. Available: https://www.nginx.com/resources/wiki/
  13. Docker Development Team, “Website: Docker - software containeraization platform,” 2018, accessed on 6-Jan-2018. [Online]. Available: http://www.docker.com/