TY - JOUR AU - Király, Bence AU - Sali, Attila TI - Minimal Armstrong Databases for Cardinality Constraints JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14589 PY - 2024 SP - 64 EP - 81 PG - 18 SN - 0302-9743 DO - 10.1007/978-3-031-56940-1_4 UR - https://m2.mtmt.hu/api/publication/34822027 ID - 34822027 N1 - Megjelent a Foundations of Information and Knowledge Systems : 13th International Symposium, FoIKS 2024, Sheffield, UK, April 8–11, 2024, Proceedings című kötetben; Softcover ISBN: 978-3-031-56939-5, eBook ISBN: 978-3-031-56940-1 AB - Hartmann et al. proved that calculating Armstrong instance for a collection of cardinality constraints is exactly exponential problem. In fact, they presented a collection of cardinality constraints based on some special graphs, whose minimal Armstrong instance is of exponential size. Motivated by that, graph based cardinality constraints are introduced in the present paper. That is, given a simple graph on the set of attributes, max cardinality constraints on edges end vertices, respectively are set. We take up the task to determine sizes of minimum Armstrong instances of graph based cardinality constraints for several graph classes, including bipartite graphs, complete multipartite graphs. We give exact results for several graph classes or give polynomial time algorithm to construct the minimum Armstrong table for other cases. We show that Armstrong tables of graph based cardinality constraints correspond to another graph defined on the maximal independent vertex sets of the constraint graph. The row graph of an Armstrong table is defined as a pair of rows form an edge if they contain identical entries in some column. It is shown that there exists a minimal Armstrong table for a collection of graph based cardinality constraints such that the line graph of its row graph is a spanning subgraph of the graph defined on the maximal independent sets of the constraint graph. This observation is used to find minimum Armstrong tables for bipartite constraint graphs. Feasible edge colourings of graphs introduced by Folkman and Fulkerson are used to construct minimum Armstrong tables for another class of constraint graphs. © The Author(s), under exclusive license to Springer Nature Switzerland AG 2024. LA - English DB - MTMT ER - TY - JOUR AU - Palágyi, Kálmán TI - 1-Attempt and Equivalent Thinning on the Hexagonal Grid JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 2024 PY - 2024 SP - 390 EP - 401 PG - 12 SN - 0302-9743 DO - 10.1007/978-3-031-57793-2_30 UR - https://m2.mtmt.hu/api/publication/34805111 ID - 34805111 LA - English DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Ádám, Zsófia AU - Micskei, Zoltán Imre TI - ConcurrentWitness2Test: Test-Harnessing the Power of Concurrency (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 330 EP - 334 PG - 5 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_16 UR - https://m2.mtmt.hu/api/publication/34768972 ID - 34768972 AB - ConcurrentWitness2Test is a violation witness validator for concurrent software. Taking both nondeterminism of data and interleaving-based nondeterminism into account, the tool aims to use the metadata described in the violation witnesses to synthesize an executable test harness. While plagued by some initial challenges yet to overcome, the validation performance of ConcurrentWitness2Test corroborates the usefulness of the proposed approach. LA - English DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Telbisz, Csanád Ferenc AU - Somorjai, Márk AU - Ádám, Zsófia AU - Dobos-Kovács, Mihály AU - Szekeres, Dániel AU - Mondok, Milán AU - Molnár, Vince TI - Theta: Abstraction Based Techniques for Verifying Concurrency (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 412 EP - 417 PG - 6 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_30 UR - https://m2.mtmt.hu/api/publication/34768428 ID - 34768428 AB - Theta is a model checking framework, with a strong emphasis on effectively handling concurrency in software using abstraction refinement algorithms. In SV-COMP 2024, we use 1) an abstraction-aware partial order reduction; 2) a dynamic statement reduction technique; and 3) enhanced support for call stacks to handle recursive programs. We integrate these techniques in an improved architecture with inherent support for portfolio-based verification using dynamic algorithm selection, with a diverse selection of supported SMT solvers as well. In this paper we detail the advances of Theta regarding concurrent and recursive software support. LA - English DB - MTMT ER - TY - JOUR AU - Bajczi, Levente AU - Szekeres, Dániel AU - Mondok, Milán AU - Ádám, Zsófia AU - Somorjai, Márk AU - Telbisz, Csanád Ferenc AU - Dobos-Kovács, Mihály AU - Molnár, Vince TI - EmergenTheta: Verification Beyond Abstraction Refinement (Competition Contribution) JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14572 PY - 2024 SP - 371 EP - 375 PG - 5 SN - 0302-9743 DO - 10.1007/978-3-031-57256-2_23 UR - https://m2.mtmt.hu/api/publication/34768422 ID - 34768422 AB - Theta is a model checking framework conventionally based on abstraction refinement techniques. While abstraction is useful for a large number of verification problems, the over-reliance on the technique led to Theta being unable to meaningfully adapt. Identifying this problem in previous years of SV-COMP has led us to create EmergenTheta , a sandbox for the new approaches we want Theta to support. By differentiating between mature and emerging techniques, we can experiment more freely without hurting the reliability of the overall framework. In this paper we detail the development route to EmergenTheta , and its first debut on SV-COMP’24 in the ReachSafety category. LA - English DB - MTMT ER - TY - JOUR AU - Pandey, C. AU - Angryk, R.A. AU - Aydin, B. TI - Explaining Full-Disk Deep Learning Model for Solar Flare Prediction Using Attribution Methods JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14175 PY - 2023 SP - 72 EP - 89 PG - 18 SN - 0302-9743 DO - 10.1007/978-3-031-43430-3_5 UR - https://m2.mtmt.hu/api/publication/34823002 ID - 34823002 N1 - Cited By :1 Export Date: 26 April 2024 Correspondence Address: Pandey, C.; Georgia State UniversityUnited States; email: cpandey1@gsu.edu LA - English DB - MTMT ER - TY - JOUR AU - Keshan, Neha AU - Hendler, James A. TI - SCIVO. Skills to Career with Interests and Values Ontology TS - Skills to Career with Interests and Values Ontology JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14382 PY - 2023 SP - 262 EP - 276 PG - 15 SN - 0302-9743 DO - 10.1007/978-3-031-47745-4_19 UR - https://m2.mtmt.hu/api/publication/34772650 ID - 34772650 LA - English DB - MTMT ER - TY - JOUR AU - Nelyubina, Elena AU - Ryazanov, Vladimir AU - Vinogradov, Alexander TI - Analogs of Image Analysis Tools in the Search of Latent Regularities in Applied Data JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 13644 PY - 2023 SP - 529 EP - 540 PG - 12 SN - 0302-9743 DO - 10.1007/978-3-031-37742-6_41 UR - https://m2.mtmt.hu/api/publication/34756865 ID - 34756865 LA - English DB - MTMT ER - TY - JOUR AU - Vadász, Noémi TI - Resolving Hungarian Anaphora with ChatGPT JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 14102 PY - 2023 SP - 45 EP - 57 PG - 13 SN - 0302-9743 DO - 10.1007/978-3-031-40498-6_5 UR - https://m2.mtmt.hu/api/publication/34754557 ID - 34754557 LA - English DB - MTMT ER - TY - JOUR AU - Pelofske, Elijah AU - Bärtschi, Andreas AU - Eidenbenz, Stephan TI - Quantum Annealing vs. QAOA: 127 Qubit Higher-Order Ising Problems on NISQ Computers JF - LECTURE NOTES IN COMPUTER SCIENCE J2 - LNCS VL - 13948 PY - 2023 SP - 240 EP - 258 PG - 19 SN - 978-3-031-32041-5 SN - 0302-9743 UR - https://m2.mtmt.hu/api/publication/34719645 ID - 34719645 AB - Quantum annealing (QA) and Quantum Alternating Operator Ansatz (QAOA) are both heuristic quantum algorithms intended for sampling optimal solutions of combinatorial optimization problems. In this article we implement a rigorous direct comparison between QA on D-Wave hardware and QAOA on IBMQ hardware. These two quantum algorithms are also compared against classical simulated annealing. The studied problems are instances of a class of Ising models, with variable assignments of $$+1$$+1or $$-1$$-1, that contain cubic ZZZ interactions (higher order terms) and match both the native connectivity of the Pegasus topology D-Wave chips and the heavy hexagonal lattice of the IBMQ chips. The novel QAOA implementation on the heavy hexagonal lattice has a CNOT depth of 6 per round and allows for usage of an entire heavy hexagonal lattice. Experimentally, QAOA is executed on an ensemble of randomly generated Ising instances with a grid search over 1 and 2 round angles using all 127 programmable superconducting transmon qubits of ibm_washington. The error suppression technique digital dynamical decoupling is also tested on all QAOA circuits. QA is executed on the same Ising instances with the programmable superconducting flux qubit devices D-Wave Advantage_system4.1 and Advantage_system6.1 using modified annealing schedules with pauses. We find that QA outperforms QAOA on all problem instances. We also find that dynamical decoupling enables 2-round QAOA to marginally outperform 1-round QAOA, which is not the case without dynamical decoupling. LA - English DB - MTMT ER -