Have a personal or library account? Click to login

A Compact SAT Encoding for Non-Preemptive Task Scheduling on Multiple Identical Resources

Open Access
|Sep 2025

References

  1. Buttazzo, G. C., M. Bertogna, G. Yao. Limited Preemptive Scheduling for Real-Time Systems: A Survey. – IEEE Transactions on Industrial Informatics, Vol. 9, 2012, No 1, pp. 3-15.
  2. Korst, J., E. Aarts, J. K. Lenstra, J. Wessels. Periodic Multiprocessor Scheduling. Berlin, Heidelberg, Springer, 1991.
  3. Garey, M. R., D. S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman and Company, 1979.
  4. Joo, I.-Y., D.-H. Choi. Optimal Household Appliance Scheduling Considering Consumer’s Electricity Bill Target. – IEEE Transactions on Consumer Electronics, Vol. 63, 2017, No 1, pp. 19-27.
  5. Patel, J., G. Panchal. An IoT-Based Portable Smart Meeting Space with Real-Time Room Occupancy. – In: Intelligent Communication and Computational Technologies: Proceedings of Internet of Things for Technological Development, IoT4TD 2017, Springer, 2018, pp. 35-42.
  6. Tran, L. D., A. Stojcevski, T. C. Pham, T. de Souza-Daw, N. T. Nguyen, V. Q. Nguyen, C. M. Nguyen. A Smart Meeting Room Scheduling and Management System with Utilization Control and ad-hoc Support Based on Real-Time Occupancy Detection. – In: Proc. of 6th IEEE International Conference on Communications and Electronics (ICCE’16), IEEE, 2016, pp. 186-191.
  7. Wang, C., X. Li, A. Wang, X. Zhou. A Classroom Scheduling Service for Smart Classes. – IEEE Transactions on Services Computing, Vol. 10, 2015, No 2, pp. 155-164.
  8. Aloul, F. A., S. Z. Zahidi, A. Al-Farra, B. Al-Roh, B. Al-Rawi. Solving the Employee Timetabling Problem Using Advanced SAT & ILP Techniques. – Journal of Computing, Vol. 8, 2013, No 4, pp. 851-858.
  9. Aloul, F., I. Zabalawi, A. Wasfy. A SAT-Based Approach to Solve the Faculty Course Scheduling Problem. – In: 2013 Africon, IEEE, 2013, pp. 1-5.
  10. Pham, T. N., M.-F. Tsai, D. B. Nguyen, C.-R. Dow, D.-J. Deng. A Cloud-Based Smart-Parking System Based on Internet-of-Things Technologies. – IEEE Access, Vol. 3, 2015, pp. 1581-1591.
  11. Rao, Y. R. Automatic Smart Parking System Using Internet of Things (IoT). – International Journal of Engineering Technology Science and Research, Vol. 4, 2017, No 5, pp. 1-8.
  12. Krempl, M. Allocation of Trains to Platforms Optimization. – In: Proc. of 30th International Conference Mathematical Methods in Economics, Czech Republic, University of Economics, Prague, 2012, pp. 320-325.
  13. Carey, M., S. Carville. Scheduling and Platforming Trains at Busy Complex Stations. – Transportation Research Part A: Policy and Practice, Vol. 37, 2003, No 3, pp. 195-224.
  14. Mayank, J., A. Mondal. Efficient SAT Encoding Scheme for Schedulability Analysis of Non-Preemptive Tasks on Multiple Computational Resources. – Journal of Systems Architecture, Vol. 110, 2020, 101818.
  15. Papadimitriou, C. H., K. Steiglitz. Combinatorial Optimization: Algorithms and Complexity. Mineola, NY, USA, Dover Publications, 1998.
  16. Rossi, F., P. Van Beek, T. Walsh. Handbook of Constraint Programming. Amsterdam, Netherlands, Elsevier, 2006.
  17. Cucu-Grosjean, L., O. Buffet. Global Multiprocessor Real-Time Scheduling as a Constraint Satisfaction Problem. – In: Proc. of International Conference on Parallel Processing Workshops, IEEE, 2009, pp. 42-49.
  18. Woeginger, G. J. An Efficient Algorithm for a Class of Constraint Satisfaction Problems. – Operations Research Letters, Vol. 30, 2002, No 1, pp. 9-16.
  19. Dincbas, M., H. Simonis, P. van Hentenryck. Solving the Car-Sequencing Problem in Constraint Logic Programming. – In: Proc. of 8th European Conference on Artificial Intelligence (ECAI’18), 2018, London, UK, Pitman Publishing, 1988, pp. 290-295.
  20. Lawler, E. L., D. E. Wood. Branch-and-Bound Methods: A Survey. – Operations Research, Vol. 14, 1966, No 4, pp. 699-719.
  21. Hart, P. E., N. J. Nilsson, B. Raphael. A Formal Basis for the Heuristic Determination of Minimum Cost Paths. – IEEE Transactions on Systems Science and Cybernetics, Vol. 4, 1968, No 2, pp. 100-107.
  22. Biere, A., M. Heule, H. van Maaren, T. Walsh. Handbook of Satisfiability. Amsterdam, Netherlands, IOS Press, 2009.
  23. Ansótegui, C., M. L. Bonet, J. Levy. SAT-Based MaxSAT Algorithms. – Artificial Intelligence, Vol. 196, 2013, pp. 77-105.
  24. Marques-Silva, J. P., K. A. Sakallah. GRASP: A Search Algorithm for Propositional Satisfiability. – IEEE Transactions on Computers, Vol. 48, 1999, No 5, pp. 506-521.
  25. Horbach, A., T. Bartsch, D. Briskorn. Using a SAT-Solver to Schedule Sports Leagues. – Journal of Scheduling, Vol. 15, 2012, pp. 117-125.
  26. Koshimura, M., H. Nabeshima, H. Fujita, R. Hasegawa. Solving Open Job-Shop Scheduling Problems by SAT Encoding. – IEICE Transactions on Information and Systems, Vol. 93, 2010, No 8, pp. 2316-2318.
  27. Memik, S. O., F. Fallah. Accelerated SAT-Based Scheduling of Control/Data Flow Graphs. – In: Proc. of IEEE International Conference on Computer Design: VLSI in Computers and Processors, IEEE, 2002, pp. 395-400.
  28. Liu, W., M. Yuan, X. He, Z. Gu, X. Liu. Efficient SAT-Based Mapping and Scheduling of Homogeneous Synchronous Dataflow Graphs for Throughput Optimization. – In: Proc. of 2008 Real-Time Systems Symposium, IEEE, 2008, pp. 492-504.
  29. Liu, W., Z. Gu, J. Xu, X. Wu, Y. Ye. Satisfiability Modulo Graph Theory for Task Mapping and Scheduling on Multiprocessor Systems. – IEEE Transactions on Parallel and Distributed Systems, Vol. 22, 2010, No 8, pp. 1382-1389.
  30. Metzner, A., M. Franzle, C. Herde, I. Stierand. Scheduling Distributed Real-Time Systems by Satisfiability Checking. – In: Proc. of 11th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA’05), IEEE, 2005, pp. 409-415.
  31. Metzner, A., C. Herde. RTSAT – An Optimal and Efficient Approach to the Task Allocation Problem in Distributed Architectures. – In: Proc. of 2006 27th IEEE International Real-Time Systems Symposium (RTSS’06), IEEE, 2006, pp. 147-158.
  32. Davis, L. Job Shop Scheduling with Genetic Algorithms. – In: Proc. of 1st International Conference on Genetic Algorithms and their Applications, Lawrence Erlbaum Associates, Hillsdale, NJ, USA, 1985, pp. 136-140.
  33. Sotskov, Y. N., T.-C. Lai, F. Werner. Measures of Problem Uncertainty for Scheduling with Interval Processing Times. – OR Spectrum, Vol. 35, 2013, No 3, pp. 659-689.
  34. Eén, N., N. Sörensson. An Extensible SAT-Solver. – In: Proc. of International Conference on Theory and Applications of Satisfiability Testing, Springer, 2003, pp. 502-518.
  35. Biere, A. CaDiCaL, Lingeling, Plingeling, Treengeling and YalSAT Entering the SAT Competition 2018. – Proceedings of SAT Competition, Vol. 14, 2017, pp. 316-336.
  36. Bailleux, O., Y. Boufkhad, O. Roussel. A Translation of Pseudo Boolean Constraints to SAT. – Journal on Satisfiability, Boolean Modeling and Computation, Vol. 2, 2006, No 1-4, pp. 191-200.
  37. Abío, I., R. Asín, R. Nieuwenhuis, A. Oliveras, E. Rodríguez-Carbonell. BDDs for Pseudo-Boolean Constraints – Revisited. – In: Proc. of International Conference on Theory and Applications of Satisfiability Testing, 2012, Berlin, Heidelberg, Springer, 2012, pp. 63-76.
  38. Moskewicz, M. W., C. F. Madigan, Y. Zhao, L. Zhang, S. Malik. Chaff: Engineering an Efficient SAT Solver. – In: Proc. of 38th Annual Design Automation Conference, ACM, 2001, pp. 530-535.
  39. Goldberg, E., Y. Novikov. BerkMin: A Fast and Robust SAT-Solver. – In: Proc. of Design, Automation and Test in Europe Conference and Exhibition 2002, IEEE, 2002, pp. 142-149.
  40. Audemard, G., L. Simon. Predicting Learnt Clauses Quality in Modern SAT Solvers. – In: Proc. of 21st International Joint Conference on Artificial Intelligence (IJCAI’09), AAAI Press, 2009, pp. 399-404.
  41. Biere, A. Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. – In: SAT Race, 2010, pp. 1-4.
  42. Kochemazov, S. F2TRC: Deterministic Modifications of SC2018-SR2019 Winners. – Proceedings of SAT Competition, 2020, pp. 21-22.
  43. Afzalirad, M., J. Rezaeian. Resource-Constrained Unrelated Parallel Machine Scheduling Problem with Sequence Dependent Setup Times, Precedence Constraints and Machine Eligibility Restrictions. – Computers & Industrial Engineering, Vol. 98, 2016, pp. 40-52.
DOI: https://doi.org/10.2478/cait-2025-0025 | Journal eISSN: 1314-4081 | Journal ISSN: 1311-9702
Language: English
Page range: 104 - 122
Published on: Sep 25, 2025
Published by: Bulgarian Academy of Sciences, Institute of Information and Communication Technologies
In partnership with: Paradigm Publishing Services
Publication frequency: 4 issues per year

© 2025 Tuyen Van Kieu, Khanh Van To, published by Bulgarian Academy of Sciences, Institute of Information and Communication Technologies
This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.