ABSTRACT. Symmetries in Boolean satisfiability (SAT) problems often cause redundant exploration of equivalent regions of the search space, significantly degrading solver performance. Symmetry breaking constraints (SBCs) address this issue by eliminating symmetric solutions while preserving satisfiability. In this work, we study the generation of SBCs from known symmetries for a given SAT formula. We present a tool for constructing SBCs using patterns, a compact representation introduced in previous work. The proposed approach generates clauses using selected sets of permutations while allowing control over the depth of generating constraints, providing a trade-off between the strength of symmetry breaking and the size of the resulting formula. Our main focus is an experimental evaluation of how different sets of permutations influence the effectiveness of symmetry breaking. The experiments are conducted on problems naturally representable as binary matrices, but more complex problems may be considered. We evaluate both solving performance and the reduction in the number of symmetric solutions using state-of-the-art SAT solvers.

ABSTRACT. This paper is a contribution to the analysis of variable ordering heuristics for constraint satisfaction problems. A model of information flow leading to heuristic decisions is presented that includes four distinguishable components: discriminability, feature and message value quality, and decision quality. Experimental results demonstrate that each of the quality components has a definite effect on performance when other components are held constant. These results should improve the analysis of CSP heuristics going forward. They also bear on an earlier analysis of heuristic effects, or heuristic actions, since they clarify one of these actions that had not been adequately characterized prior to this work. As a result, we now have the makings of a complete framework for explaining how variable ordering heuristics actually work.

ABSTRACT. Earlier work has shown that variable ordering heuristics for CSPs improve search by enhancing two fundamentally different actions, labeled simplification and contention. The present work deals with the corresponding problem of why different problems in a supposedly homogeneous set respond differentially to these two heuristic actions. To this end, DNNs were tested to determine whether they could learn to discriminate among problems on this basis given a particular set of feature measurements. Following the success of these tests, XAI (specifically, SHAP) methods were used to gain some insight into the basis for this capacity. The most important features involved the structure of the constraint graph, in particular the degree distribution across variables. However, further tests showed that a number of other features had to be incorporated for highly accurate classification.

ABSTRACT. When studying machine learning (ML) models induced from the same training data, one query of interest is predictive equivalence, i.e. to decide whether two models compute the same function. By keeping a single representative of the ML models computing the same function, one removes unwanted redundancy from the Rashomon set associated with the given training data. Furthermore, it is often paramount to answer queries about ML models when not all inputs are known, i.e. when there exists missing data. Examples of relevant queries include prediction sufficiency, but also several other queries related to explainable artificial intelligence (XAI). This paper shows that most of these queries related with reasoning about decision trees can be solved in polynomial time. Furthermore, the paper proves a lower bound on the complexity of enumeration of abductive explanations also in the case of DTs.

ABSTRACT. This project introduces a case study which investigates how pretrained Large Language Models (LLMs), namely OPT, BLOOM, Llama-2, and Llama-3.1, handle five tasks from the bAbI dataset -- a set of common sense and reading comprehension problems stemming from the Facebook research group in 2015. In this investigation, our goal is to provide evaluations of the models themselves rather than their embedding within more complex platforms such as chatbots. By reframing bAbI question answering tasks as language generation problems, we study whether LLMs can function as general-purpose alternatives to specialized information extraction and question answering systems. To this end, we contextualize this investigation with respect to specialized tools designed to solve tasks from the bAbI dataset, including the neural network approach AM+NG+NL MemNN as well as joint statistical NLP and symbolic reasoning approaches s IRLR and TEXT2ALM.

ABSTRACT. The integration of Large Language Models (LLMs) into multi-agent systems promises to enhance agent decision-making with flexible natural-language reasoning, yet raises concerns about controllability, predictability, and safety. We present a principled approach to this problem implemented in DALI2, a logic-based multi-agent framework running on SWI-Prolog. Our key insight is that the tell/told communication filters—originally designed in the DALI language for inter-agent message filtering—can be uniformly extended to govern agent-LLM interactions. Tell rules declaratively constrain what queries an agent may send to an LLM oracle; told rules constrain which responses the agent will accept, with support for pattern matching, state-dependent conditions, and priority-based ordering. The mechanism is fully declarative, bidirectional, and operates within the standard agent reasoning cycle without architectural changes. We formalise the filtering protocol, evaluate it on three test scenarios (smart agriculture, emergency response, and a state-dependent suite), and discuss its properties in comparison with existing LLM guardrail approaches.