Showing 1–10 of 10 results for author: Ansótegui, C

SAT, Gadgets, Max2XOR, and Quantum Annealers

Authors: Carlos Ansótegui, Jordi Levy

Abstract: Quantum Annealers are basically quantum computers that with high probability can optimize certain quadratic functions on Boolean variables in constant time. These functions are basically the Hamiltonian of Ising models that reach the ground energy state, with a high probability, after an annealing process. They have been proposed as a way to solve SAT. These Hamiltonians can be seen as Max2XOR p… ▽ More Quantum Annealers are basically quantum computers that with high probability can optimize certain quadratic functions on Boolean variables in constant time. These functions are basically the Hamiltonian of Ising models that reach the ground energy state, with a high probability, after an annealing process. They have been proposed as a way to solve SAT. These Hamiltonians can be seen as Max2XOR problems, i.e. as the problem of finding an assignment that maximizes the number of XOR clauses of at most 2 variables that are satisfied. In this paper, we present several gadgets to reduce SAT to Max2XOR. We show how they can be used to translate SAT instances to initial configurations of a quantum annealer. △ Less

Submitted 13 May, 2024; v1 submitted 29 February, 2024; originally announced March 2024.

Comments: arXiv admin note: text overlap with arXiv:2204.01774

Exploiting Configurations of MaxSAT Solvers

Authors: Josep Alòs, Carlos Ansótegui, Josep M. Salvia, Eduard Torres

Abstract: In this paper, we describe how we can effectively exploit alternative parameter configurations to a MaxSAT solver. We describe how these configurations can be computed in the context of MaxSAT. In particular, we experimentally show how to easily combine configurations of a non-competitive solver to obtain a better solving approach. In this paper, we describe how we can effectively exploit alternative parameter configurations to a MaxSAT solver. We describe how these configurations can be computed in the context of MaxSAT. In particular, we experimentally show how to easily combine configurations of a non-competitive solver to obtain a better solving approach. △ Less

Submitted 13 June, 2023; originally announced June 2023.

A Benchmark Generator for Combinatorial Testing

Authors: Carlos Ansotegui, Eduard Torres

Abstract: Combinatorial Testing (CT) tools are essential to test properly a wide range of systems (train systems, Graphical User Interfaces (GUIs), autonomous driving systems, etc). While there is an active research community working on developing CT tools, paradoxically little attention has been paid to making available enough resources to test the CT tools themselves. In particular, the set of available b… ▽ More Combinatorial Testing (CT) tools are essential to test properly a wide range of systems (train systems, Graphical User Interfaces (GUIs), autonomous driving systems, etc). While there is an active research community working on developing CT tools, paradoxically little attention has been paid to making available enough resources to test the CT tools themselves. In particular, the set of available benchmarks to asses their correctness, effectiveness and efficiency is rather limited. In this paper, we introduce a new generator of CT benchmarks that essentially borrows the structure contained in the plethora of available Combinatorial Problems from other research communities in order to create meaningful benchmarks. We additionally perform an extensive evaluation of CT tools with these new benchmarks. Thanks to this study we provide some insights on under which circumstances a particular CT tool should be used. △ Less

Submitted 24 January, 2023; v1 submitted 29 December, 2022; originally announced January 2023.

Comments: Extended some explanations and added comparison with the SUT generator in the CT Competition 2022

Reducing SAT to Max2XOR

Authors: Carlos Ansótegui, Jordi Levy

Abstract: Representing some problems with XOR clauses (parity constraints) can allow to apply more efficient reasoning techniques. In this paper, we present a gadget for translating SAT clauses into Max2XOR constraints, i.e., XOR clauses of at most 2 variables equal to zero or to one. Additionally, we present new resolution rules for the Max2XOR problem which asks for which is the maximum number of constrai… ▽ More Representing some problems with XOR clauses (parity constraints) can allow to apply more efficient reasoning techniques. In this paper, we present a gadget for translating SAT clauses into Max2XOR constraints, i.e., XOR clauses of at most 2 variables equal to zero or to one. Additionally, we present new resolution rules for the Max2XOR problem which asks for which is the maximum number of constraints that can be satisfied from a set of 2XOR equations. △ Less

Submitted 4 April, 2022; originally announced April 2022.

Interpretable Decision Trees Through MaxSAT

Authors: Josep Alos, Carlos Ansotegui, Eduard Torres

Abstract: We present an approach to improve the accuracy-interpretability trade-off of Machine Learning (ML) Decision Trees (DTs). In particular, we apply Maximum Satisfiability technology to compute Minimum Pure DTs (MPDTs). We improve the runtime of previous approaches and, show that these MPDTs can outperform the accuracy of DTs generated with the ML framework sklearn. We present an approach to improve the accuracy-interpretability trade-off of Machine Learning (ML) Decision Trees (DTs). In particular, we apply Maximum Satisfiability technology to compute Minimum Pure DTs (MPDTs). We improve the runtime of previous approaches and, show that these MPDTs can outperform the accuracy of DTs generated with the ML framework sklearn. △ Less

Submitted 14 July, 2022; v1 submitted 26 October, 2021; originally announced October 2021.

Incomplete MaxSAT Approaches for Combinatorial Testing

Authors: Carlos Ansótegui, Felip Manyà, Jesus Ojeda, Josep M. Salvia, Eduard Torres

Abstract: We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length, referred to as the Covering Array Number problem. This problem is central in Combinatorial Testing for the detection of system failures. In particular, we show how to apply Maximum Satisfiability (MaxSAT) technology by describing efficient encodings for different classes of compl… ▽ More We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length, referred to as the Covering Array Number problem. This problem is central in Combinatorial Testing for the detection of system failures. In particular, we show how to apply Maximum Satisfiability (MaxSAT) technology by describing efficient encodings for different classes of complete and incomplete MaxSAT solvers to compute optimal and suboptimal solutions, respectively. Similarly, we show how to solve through MaxSAT technology a closely related problem, the Tuple Number problem, which we extend to incorporate constraints. For this problem, we additionally provide a new MaxSAT-based incomplete algorithm. The extensive experimental evaluation we carry out on the available Mixed Covering Arrays with Constraints benchmarks and the comparison with state-of-the-art tools confirm the good performance of our approaches. △ Less

Submitted 26 May, 2021; originally announced May 2021.

Learning How to Optimize Black-Box Functions With Extreme Limits on the Number of Function Evaluations

Authors: Carlos Ansotegui, Meinolf Sellmann, Tapan Shah, Kevin Tierney

Abstract: We consider black-box optimization in which only an extremely limited number of function evaluations, on the order of around 100, are affordable and the function evaluations must be performed in even fewer batches of a limited number of parallel trials. This is a typical scenario when optimizing variable settings that are very costly to evaluate, for example in the context of simulation-based opti… ▽ More We consider black-box optimization in which only an extremely limited number of function evaluations, on the order of around 100, are affordable and the function evaluations must be performed in even fewer batches of a limited number of parallel trials. This is a typical scenario when optimizing variable settings that are very costly to evaluate, for example in the context of simulation-based optimization or machine learning hyperparameterization. We propose an original method that uses established approaches to propose a set of points for each batch and then down-selects from these candidate points to the number of trials that can be run in parallel. The key novelty of our approach lies in the introduction of a hyperparameterized method for down-selecting the number of candidates to the allowed batch-size, which is optimized offline using automated algorithm configuration. We tune this method for black box optimization and then evaluate on classical black box optimization benchmarks. Our results show that it is possible to learn how to combine evaluation points suggested by highly diverse black box optimization methods conditioned on the progress of the optimization. Compared with the state of the art in black box minimization and various other methods specifically geared towards few-shot minimization, we achieve an average reduction of 50\% of normalized cost, which is a highly significant improvement in performance. △ Less

Submitted 18 March, 2021; originally announced March 2021.

Scale-Free Random SAT Instances

Authors: Carlos Ansótegui, Maria Luisa Bonet, Jordi Levy

Abstract: We focus on the random generation of SAT instances that have properties similar to real-world instances. It is known that many industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide a different generation model of SAT instances, called \em… ▽ More We focus on the random generation of SAT instances that have properties similar to real-world instances. It is known that many industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide a different generation model of SAT instances, called \emph{scale-free random SAT instances}. It is based on the use of a non-uniform probability distribution $P(i)\sim i^{-β}$ to select variable $i$, where $β$ is a parameter of the model. This results into formulas where the number of occurrences $k$ of variables follows a power-law distribution $P(k)\sim k^{-δ}$ where $δ= 1 + 1/β$. This property has been observed in most real-world SAT instances. For $β=0$, our model extends classical random SAT instances. We prove the existence of a SAT-UNSAT phase transition phenomenon for scale-free random 2-SAT instances with $β<1/2$ when the clause/variable ratio is $m/n=\frac{1-2β}{(1-β)^2}$. We also prove that scale-free random k-SAT instances are unsatisfiable with high probability when the number of clauses exceeds $ω(n^{(1-β)k})$. %This implies that the SAT/UNSAT phase transition phenomena vanishes when $β>1-1/k$, and formulas are unsatisfiable due to a small core of clauses. The proof of this result suggests that, when $β>1-1/k$, the unsatisfiability of most formulas may be due to small cores of clauses. Finally, we show how this model will allow us to generate random instances similar to industrial instances, of interest for testing purposes. △ Less

Submitted 17 July, 2019; v1 submitted 12 July, 2017; originally announced August 2017.

Journal ref: Algorithms 15(6): 219 (2022)

Community Structure in Industrial SAT Instances

Authors: Carlos Ansótegui, Maria Luisa Bonet, Jesús Giráldez-Cru, Jordi Levy, Laurent Simon

Abstract: Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit the underlying structure of industrial instances. However, there are few works trying to exactly characterize the main features of this structure. The research community on compl… ▽ More Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental process. It is believed that these techniques exploit the underlying structure of industrial instances. However, there are few works trying to exactly characterize the main features of this structure. The research community on complex networks has developed techniques of analysis and algorithms to study real-world graphs that can be used by the SAT community. Recently, there have been some attempts to analyze the structure of industrial SAT instances in terms of complex networks, with the aim of explaining the success of SAT solving techniques, and possibly improving them. In this paper, inspired by the results on complex networks, we study the community structure, or modularity, of industrial SAT instances. In a graph with clear community structure, or high modularity, we can find a partition of its nodes into communities such that most edges connect variables of the same community. In our analysis, we represent SAT instances as graphs, and we show that most application benchmarks are characterized by a high modularity. On the contrary, random SAT instances are closer to the classical Erdös-Rényi random graph model, where no structure can be observed. We also analyze how this structure evolves by the effects of the execution of a CDCL SAT solver. In particular, we use the community structure to detect that new clauses learned by the solver during the search contribute to destroy the original structure of the formula. This is, learned clauses tend to contain variables of distinct communities. △ Less

Submitted 17 July, 2019; v1 submitted 10 June, 2016; originally announced June 2016.

Journal ref: J. Artif. Intell. Res. 66: 443-472 (2019)

The Fractal Dimension of SAT Formulas

Authors: C. Ansótegui, M. L. Bonet, J. Giráldez-Cru, J. Levy

Abstract: Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental testing process. Recently, there have been some attempts to analyze the structure of these formulas in terms of complex networks, with the long-term aim of explaining the success of these SAT solving techniques, and possibly improving… ▽ More Modern SAT solvers have experienced a remarkable progress on solving industrial instances. Most of the techniques have been developed after an intensive experimental testing process. Recently, there have been some attempts to analyze the structure of these formulas in terms of complex networks, with the long-term aim of explaining the success of these SAT solving techniques, and possibly improving them. We study the fractal dimension of SAT formulas, and show that most industrial families of formulas are self-similar, with a small fractal dimension. We also show that this dimension is not affected by the addition of learnt clauses. We explore how the dimension of a formula, together with other graph properties can be used to characterize SAT instances. Finally, we give empirical evidence that these graph properties can be used in state-of-the-art portfolios. △ Less

Submitted 23 August, 2013; originally announced August 2013.

Comments: 20 pages, 11 Postscript figures

Journal ref: Automated Reasoning, LNCS 8562, pp 107-121, Springer (2014)