Showing 1–22 of 22 results for author: Levy, J

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

Generalization in medical AI: a perspective on develo** scalable models

Authors: Joachim A. Behar, Jeremy Levy, Leo Anthony Celi

Abstract: Over the past few years, research has witnessed the advancement of deep learning models trained on large datasets, some even encompassing millions of examples. While these impressive performance on their hidden test sets, they often underperform when assessed on external datasets. Recognizing the critical role of generalization in medical AI development, many prestigious journals now require repor… ▽ More Over the past few years, research has witnessed the advancement of deep learning models trained on large datasets, some even encompassing millions of examples. While these impressive performance on their hidden test sets, they often underperform when assessed on external datasets. Recognizing the critical role of generalization in medical AI development, many prestigious journals now require reporting results both on the local hidden test set as well as on external datasets before considering a study for publication. Effectively, the field of medical AI has transitioned from the traditional usage of a single dataset that is split into train and test to a more comprehensive framework using multiple datasets, some of which are used for model development (source domain) and others for testing (target domains). However, this new experimental setting does not necessarily resolve the challenge of generalization. This is because of the variability encountered in intended use and specificities across hospital cultures making the idea of universally generalizable systems a myth. On the other hand, the systematic, and a fortiori recurrent re-calibration, of models at the individual hospital level, although ideal, may be overoptimistic given the legal, regulatory and technical challenges that are involved. Re-calibration using transfer learning may not even be possible in some instances where reference labels of target domains are not available. In this perspective we establish a hierarchical three-level scale system reflecting the generalization level of a medical AI algorithm. This scale better reflects the diversity of real-world medical scenarios per which target domain data for re-calibration of models may or not be available and if it is, may or not have reference labels systematically available. △ Less

Submitted 9 November, 2023; originally announced November 2023.

Active Inverse Learning in Stackelberg Trajectory Games

Authors: Yue Yu, Jacob Levy, Negar Mehr, David Fridovich-Keil, Ufuk Topcu

Abstract: Game-theoretic inverse learning is the problem of inferring the players' objectives from their actions. We formulate an inverse learning problem in a Stackelberg game between a leader and a follower, where each player's action is the trajectory of a dynamical system. We propose an active inverse learning method for the leader to infer which hypothesis among a finite set of candidates describes the… ▽ More Game-theoretic inverse learning is the problem of inferring the players' objectives from their actions. We formulate an inverse learning problem in a Stackelberg game between a leader and a follower, where each player's action is the trajectory of a dynamical system. We propose an active inverse learning method for the leader to infer which hypothesis among a finite set of candidates describes the follower's objective function. Instead of using passively observed trajectories like existing methods, the proposed method actively maximizes the differences in the follower's trajectories under different hypotheses to accelerate the leader's inference. We demonstrate the proposed method in a receding-horizon repeated trajectory game. Compared with uniformly random inputs, the leader inputs provided by the proposed method accelerate the convergence of the probability of different hypotheses conditioned on the follower's trajectory by orders of magnitude. △ Less

Submitted 15 August, 2023; originally announced August 2023.

Simultaneous column-based deep learning progression analysis of atrophy associated with AMD in longitudinal OCT studies

Authors: Adi Szeskin, Roei Yehuda, Or Shmueli, Jaime Levy, Leo Joskowicz

Abstract: Purpose: Disease progression of retinal atrophy associated with AMD requires the accurate quantification of the retinal atrophy changes on longitudinal OCT studies. It is based on finding, comparing, and delineating subtle atrophy changes on consecutive pairs (prior and current) of unregistered OCT scans. Methods: We present a fully automatic end-to-end pipeline for the simultaneous detection and… ▽ More Purpose: Disease progression of retinal atrophy associated with AMD requires the accurate quantification of the retinal atrophy changes on longitudinal OCT studies. It is based on finding, comparing, and delineating subtle atrophy changes on consecutive pairs (prior and current) of unregistered OCT scans. Methods: We present a fully automatic end-to-end pipeline for the simultaneous detection and quantification of time-related atrophy changes associated with dry AMD in pairs of OCT scans of a patient. It uses a novel simultaneous multi-channel column-based deep learning model trained on registered pairs of OCT scans that concurrently detects and segments retinal atrophy segments in consecutive OCT scans by classifying light scattering patterns in matched pairs of vertical pixel-wide columns (A-scans) in registered prior and current OCT slices (B-scans). Results: Experimental results on 4,040 OCT slices with 5.2M columns from 40 scans pairs of 18 patients (66% training/validation, 33% testing) with 24.13+-14.0 months apart in which Complete RPE and Outer Retinal Atrophy (cRORA) was identified in 1,998 OCT slices (735 atrophy lesions from 3,732 segments, 0.45M columns) yield a mean atrophy segments detection precision, recall of 0.90+-0.09, 0.95+-0.06 and 0.74+-0.18, 0.94+-0.12 for atrophy lesions with AUC=0.897, all above observer variability. Simultaneous classification outperforms standalone classification precision and recall by 30+-62% and 27+-0% for atrophy segments and lesions. Conclusions: simultaneous column-based detection and quantification of retinal atrophy changes associated with AMD is accurate and outperforms standalone classification methods. Translational relevance: an automatic and efficient way to detect and quantify retinal atrophy changes associated with AMD. △ Less

Submitted 31 July, 2023; originally announced July 2023.

Comments: 34 pages, 5 figures and 2 tables

Enabling Efficient, Reliable Real-World Reinforcement Learning with Approximate Physics-Based Models

Authors: Tyler Westenbroek, Jacob Levy, David Fridovich-Keil

Abstract: We focus on develo** efficient and reliable policy optimization strategies for robot learning with real-world data. In recent years, policy gradient methods have emerged as a promising paradigm for training control policies in simulation. However, these approaches often remain too data inefficient or unreliable to train on real robotic hardware. In this paper we introduce a novel policy gradient… ▽ More We focus on develo** efficient and reliable policy optimization strategies for robot learning with real-world data. In recent years, policy gradient methods have emerged as a promising paradigm for training control policies in simulation. However, these approaches often remain too data inefficient or unreliable to train on real robotic hardware. In this paper we introduce a novel policy gradient-based policy optimization framework which systematically leverages a (possibly highly simplified) first-principles model and enables learning precise control policies with limited amounts of real-world data. Our approach $1)$ uses the derivatives of the model to produce sample-efficient estimates of the policy gradient and $2)$ uses the model to design a low-level tracking controller, which is embedded in the policy class. Theoretical analysis provides insight into how the presence of this feedback controller overcomes key limitations of stand-alone policy gradient methods, while hardware experiments with a small car and quadruped demonstrate that our approach can learn precise control strategies reliably and with only minutes of real-world data. △ Less

Submitted 6 November, 2023; v1 submitted 16 July, 2023; originally announced July 2023.

General Boolean Formula Minimization with QBF Solvers

Authors: Eduardo Calò, Jordi Levy

Abstract: The minimization of propositional formulae is a classical problem in logic, whose first algorithms date back at least to the 1950s with the works of Quine and Karnaugh. Most previous work in the area has focused on obtaining minimal, or quasi-minimal, formulae in conjunctive normal form (CNF) or disjunctive normal form (DNF), with applications in hardware design. In this paper, we are interested i… ▽ More The minimization of propositional formulae is a classical problem in logic, whose first algorithms date back at least to the 1950s with the works of Quine and Karnaugh. Most previous work in the area has focused on obtaining minimal, or quasi-minimal, formulae in conjunctive normal form (CNF) or disjunctive normal form (DNF), with applications in hardware design. In this paper, we are interested in the problem of obtaining an equivalent formula in any format, also allowing connectives that are not present in the original formula. We are primarily motivated in applying minimization algorithms to generate natural language translations of the original formula, where using shorter equivalents as input may result in better translations. Recently, Buchfuhrer and Umans have proved that the (decisional version of the) problem is $Σ_2^p$-complete. We analyze three possible (practical) approaches to solving the problem. First, using brute force, generating all possible formulae in increasing size and checking if they are equivalent to the original formula by testing all possible variable assignments. Second, generating the Tseitin coding of all the formulae and checking equivalence with the original using a SAT solver. Third, encoding the problem as a Quantified Boolean Formula (QBF), and using a QBF solver. Our results show that the QBF approach largely outperforms the other two. △ Less

Submitted 12 March, 2023; originally announced March 2023.

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.

Vaccine Search Patterns Provide Insights into Vaccination Intent

Authors: Sean Malahy, Mimi Sun, Keith Spangler, Jessica Leibler, Kevin Lane, Shailesh Bavadekar, Chaitanya Kamath, Akim Kumok, Yuantong Sun, Jai Gupta, Tague Griffith, Adam Boulanger, Mark Young, Charlotte Stanton, Yael Mayer, Karen Smith, Tomer Shekel, Katherine Chou, Greg Corrado, Jonathan Levy, Adam Szpiro, Evgeniy Gabrilovich, Gregory A Wellenius

Abstract: Despite ample supply of COVID-19 vaccines, the proportion of fully vaccinated individuals remains suboptimal across much of the US. Rapid vaccination of additional people will prevent new infections among both the unvaccinated and the vaccinated, thus saving lives. With the rapid rollout of vaccination efforts this year, the internet has become a dominant source of information about COVID-19 vacci… ▽ More Despite ample supply of COVID-19 vaccines, the proportion of fully vaccinated individuals remains suboptimal across much of the US. Rapid vaccination of additional people will prevent new infections among both the unvaccinated and the vaccinated, thus saving lives. With the rapid rollout of vaccination efforts this year, the internet has become a dominant source of information about COVID-19 vaccines, their safety and efficacy, and their availability. We sought to evaluate whether trends in internet searches related to COVID-19 vaccination - as reflected by Google's Vaccine Search Insights (VSI) index - could be used as a marker of population-level interest in receiving a vaccination. We found that between January and August of 2021: 1) Google's weekly VSI index was associated with the number of new vaccinations administered in the subsequent three weeks, and 2) the average VSI index in earlier months was strongly correlated (up to r = 0.89) with vaccination rates many months later. Given these results, we illustrate an approach by which data on search interest may be combined with other available data to inform local public health outreach and vaccination efforts. These results suggest that the VSI index may be useful as a leading indicator of population-level interest in or intent to obtain a COVID-19 vaccine, especially early in the vaccine deployment efforts. These results may be relevant to current efforts to administer COVID-19 vaccines to unvaccinated individuals, to newly eligible children, and to those eligible to receive a booster shot. More broadly, these results highlight the opportunities for anonymized and aggregated internet search data, available in near real-time, to inform the response to public health emergencies. △ Less

Submitted 22 November, 2021; originally announced November 2021.

Comments: Main text 21 pages, 6 figures, 2 tables. Submitted to Nature Medicine

Shrinking Bigfoot: Reducing wav2vec 2.0 footprint

Authors: Zilun Peng, Akshay Budhkar, Ilana Tuil, Jason Levy, Parinaz Sobhani, Raphael Cohen, Jumana Nassour

Abstract: Wav2vec 2.0 is a state-of-the-art speech recognition model which maps speech audio waveforms into latent representations. The largest version of wav2vec 2.0 contains 317 million parameters. Hence, the inference latency of wav2vec 2.0 will be a bottleneck in production, leading to high costs and a significant environmental footprint. To improve wav2vec's applicability to a production setting, we ex… ▽ More Wav2vec 2.0 is a state-of-the-art speech recognition model which maps speech audio waveforms into latent representations. The largest version of wav2vec 2.0 contains 317 million parameters. Hence, the inference latency of wav2vec 2.0 will be a bottleneck in production, leading to high costs and a significant environmental footprint. To improve wav2vec's applicability to a production setting, we explore multiple model compression methods borrowed from the domain of large language models. Using a teacher-student approach, we distilled the knowledge from the original wav2vec 2.0 model into a student model, which is 2 times faster and 4.8 times smaller than the original model. This increase in performance is accomplished with only a 7% degradation in word error rate (WER). Our quantized model is 3.6 times smaller than the original model, with only a 0.1% degradation in WER. To the best of our knowledge, this is the first work that compresses wav2vec 2.0. △ Less

Submitted 1 April, 2021; v1 submitted 29 March, 2021; originally announced March 2021.

Comments: Submitted to INTERSPEECH 2021

Nominal Unification and Matching of Higher Order Expressions with Recursive Let

Authors: Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret, Yunus Kutz

Abstract: A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expression… ▽ More A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expressions with recursive let and atom-variables, where we show that it also runs in nondeterministic polynomial time. In addition we prove that there is a guessing strategy for nominal unification with letrec and atom-variable that is a trade-off between exponential growth and non-determinism. Nominal matching with variables representing partial letrec-environments is also shown to be in NP. △ Less

Submitted 26 April, 2022; v1 submitted 16 February, 2021; originally announced February 2021.

Comments: 37 pages, 9 figures, This paper is an extended version of the conference publication: Manfred Schmidt-Schauß and Temur Kutsia and Jordi Levy and Mateu Villaret and Yunus Kutz, Nominal Unification of Higher Order Expressions with Recursive Let, LOPSTR-16, Lecture Notes in Computer Science 10184, Springer, p 328 -344, 2016. arXiv admin note: text overlap with arXiv:1608.03771

ACM Class: I.2.3

Journal ref: Fundamenta Informaticae, Volume 185, Issue 3 (May 6, 2022) fi:7191

Contrastive Unsupervised Learning for Speech Emotion Recognition

Authors: Mao Li, Bo Yang, Joshua Levy, Andreas Stolcke, Viktor Rozgic, Spyros Matsoukas, Constantinos Papayiannis, Daniel Bone, Chao Wang

Abstract: Speech emotion recognition (SER) is a key technology to enable more natural human-machine communication. However, SER has long suffered from a lack of public large-scale labeled datasets. To circumvent this problem, we investigate how unsupervised representation learning on unlabeled datasets can benefit SER. We show that the contrastive predictive coding (CPC) method can learn salient representat… ▽ More Speech emotion recognition (SER) is a key technology to enable more natural human-machine communication. However, SER has long suffered from a lack of public large-scale labeled datasets. To circumvent this problem, we investigate how unsupervised representation learning on unlabeled datasets can benefit SER. We show that the contrastive predictive coding (CPC) method can learn salient representations from unlabeled datasets, which improves emotion recognition performance. In our experiments, this method achieved state-of-the-art concordance correlation coefficient (CCC) performance for all emotion primitives (activation, valence, and dominance) on IEMOCAP. Additionally, on the MSP- Podcast dataset, our method obtained considerable performance improvements compared to baselines. △ Less

Submitted 12 February, 2021; originally announced February 2021.

Machine learning for nocturnal diagnosis of chronic obstructive pulmonary disease using digital oximetry biomarkers

Authors: Jeremy Levy, Daniel Alvarez, Felix del Campo, Joachim A. Behar

Abstract: Objective: Chronic obstructive pulmonary disease (COPD) is a highly prevalent chronic condition. COPD is a major source of morbidity, mortality and healthcare costs. Spirometry is the gold standard test for a definitive diagnosis and severity grading of COPD. However, a large proportion of individuals with COPD are undiagnosed and untreated. Given the high prevalence of COPD and its clinical impor… ▽ More Objective: Chronic obstructive pulmonary disease (COPD) is a highly prevalent chronic condition. COPD is a major source of morbidity, mortality and healthcare costs. Spirometry is the gold standard test for a definitive diagnosis and severity grading of COPD. However, a large proportion of individuals with COPD are undiagnosed and untreated. Given the high prevalence of COPD and its clinical importance, it is critical to develop new algorithms to identify undiagnosed COPD, especially in specific groups at risk, such as those with sleep disorder breathing. To our knowledge, no research has looked at the feasibility of COPD diagnosis from the nocturnal oximetry time series. Approach: We hypothesize that patients with COPD will exert certain patterns and/or dynamics of their overnight oximetry time series that are unique to this condition. We introduce a novel approach to nocturnal COPD diagnosis using 44 oximetry digital biomarkers and 5 demographic features and assess its performance in a population sample at risk of sleep-disordered breathing. A total of n=350 unique patients polysomnography (PSG) recordings. A random forest (RF) classifier is trained using these features and evaluated using the nested cross-validation procedure. Significance: Our research makes a number of novel scientific contributions. First, we demonstrated for the first time, the feasibility of COPD diagnosis from nocturnal oximetry time series in a population sample at risk of sleep disordered breathing. We highlighted what digital oximetry biomarkers best reflect how COPD manifests overnight. The results motivate that overnight single channel oximetry is a valuable pathway for COPD diagnosis. △ Less

Submitted 10 December, 2020; originally announced December 2020.

Comments: 34 pages, 9 figures

The Impact of Heterogeneity and Geometry on the Proof Complexity of Random Satisfiability

Authors: Thomas Bläsius, Tobias Friedrich, Andreas Göbel, Jordi Levy, Ralf Rothenberger

Abstract: Satisfiability is considered the canonical NP-complete problem and is used as a starting point for hardness reductions in theory, while in practice heuristic SAT solving algorithms can solve large-scale industrial SAT instances very efficiently. This disparity between theory and practice is believed to be a result of inherent properties of industrial SAT instances that make them tractable. Two cha… ▽ More Satisfiability is considered the canonical NP-complete problem and is used as a starting point for hardness reductions in theory, while in practice heuristic SAT solving algorithms can solve large-scale industrial SAT instances very efficiently. This disparity between theory and practice is believed to be a result of inherent properties of industrial SAT instances that make them tractable. Two characteristic properties seem to be prevalent in the majority of real-world SAT instances, heterogeneous degree distribution and locality. To understand the impact of these two properties on SAT, we study the proof complexity of random k-SAT models that allow to control heterogeneity and locality. Our findings show that heterogeneity alone does not make SAT easy as heterogeneous random k-SAT instances have superpolynomial resolution size. This implies intractability of these instances for modern SAT-solvers. On the other hand, modeling locality with an underlying geometry leads to small unsatisfiable subformulas, which can be found within polynomial time. A key ingredient for the result on geometric random k-SAT can be found in the complexity of higher-order Voronoi diagrams. As an additional technical contribution, we show a linear upper bound on the number of non-empty Voronoi regions, that holds for points with random positions in a very general setting. In particular, it covers arbitrary p-norms, higher dimensions, and weights affecting the area of influence of each point multiplicatively. This is in stark contrast to quadratic lower bounds for the worst case. △ Less

Submitted 23 November, 2021; v1 submitted 15 April, 2020; originally announced April 2020.

Comments: 53 pages, 2 figures

ACM Class: F.2.2; G.2.1; G.3

Longevity Associated Geometry Identified in Satellite Images: Sidewalks, Driveways and Hiking Trails

Authors: Joshua J. Levy, Rebecca M. Lebeaux, Anne G. Hoen, Brock C. Christensen, Louis J. Vaickus, Todd A. MacKenzie

Abstract: Importance: Following a century of increase, life expectancy in the United States has stagnated and begun to decline in recent decades. Using satellite images and street view images prior work has demonstrated associations of the built environment with income, education, access to care and health factors such as obesity. However, assessment of learned image feature relationships with variation in… ▽ More Importance: Following a century of increase, life expectancy in the United States has stagnated and begun to decline in recent decades. Using satellite images and street view images prior work has demonstrated associations of the built environment with income, education, access to care and health factors such as obesity. However, assessment of learned image feature relationships with variation in crude mortality rate across the United States has been lacking. Objective: Investigate prediction of county-level mortality rates in the U.S. using satellite images. Design: Satellite images were extracted with the Google Static Maps application programming interface for 430 counties representing approximately 68.9% of the US population. A convolutional neural network was trained using crude mortality rates for each county in 2015 to predict mortality. Learned image features were interpreted using Shapley Additive Feature Explanations, clustered, and compared to mortality and its associated covariate predictors. Main Outcomes and Measures: County mortality was predicted using satellite images. Results: Predicted mortality from satellite images in a held-out test set of counties was strongly correlated to the true crude mortality rate (Pearson r=0.72). Learned image features were clustered, and we identified 10 clusters that were associated with education, income, geographical region, race and age. Conclusion and Relevance: The application of deep learning techniques to remotely-sensed features of the built environment can serve as a useful predictor of mortality in the United States. Tools that are able to identify image features associated with health-related outcomes can inform targeted public health interventions. △ Less

Submitted 5 March, 2020; originally announced March 2020.

Domain-Independent turn-level Dialogue Quality Evaluation via User Satisfaction Estimation

Authors: Praveen Kumar Bodigutla, Longshaokan Wang, Kate Ridgeway, Joshua Levy, Swanand Joshi, Alborz Geramifard, Spyros Matsoukas

Abstract: An automated metric to evaluate dialogue quality is vital for optimizing data driven dialogue management. The common approach of relying on explicit user feedback during a conversation is intrusive and sparse. Current models to estimate user satisfaction use limited feature sets and rely on annotation schemes with low inter-rater reliability, limiting generalizability to conversations spanning mul… ▽ More An automated metric to evaluate dialogue quality is vital for optimizing data driven dialogue management. The common approach of relying on explicit user feedback during a conversation is intrusive and sparse. Current models to estimate user satisfaction use limited feature sets and rely on annotation schemes with low inter-rater reliability, limiting generalizability to conversations spanning multiple domains. To address these gaps, we created a new Response Quality annotation scheme, based on which we developed turn-level User Satisfaction metric. We introduced five new domain-independent feature sets and experimented with six machine learning models to estimate the new satisfaction metric. Using Response Quality annotation scheme, across randomly sampled single and multi-turn conversations from 26 domains, we achieved high inter-annotator agreement (Spearman's rho 0.94). The Response Quality labels were highly correlated (0.76) with explicit turn-level user ratings. Gradient boosting regression achieved best correlation of ~0.79 between predicted and annotated user satisfaction labels. Multi Layer Perceptron and Gradient Boosting regression models generalized to an unseen domain better (linear correlation 0.67) than other models. Finally, our ablation study verified that our novel features significantly improved model performance. △ Less

Submitted 19 August, 2019; originally announced August 2019.

Comments: Implications of Deep Learning for Dialog Modeling - Special session at SIGdial 2019

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle

Authors: Ran Chen, Cyril Cohen, Jean-Jacques Levy, Stephan Merz, Laurent Thery

Abstract: Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle. Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle. △ Less

Submitted 29 October, 2018; originally announced October 2018.

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)

Nominal Unification of Higher Order Expressions with Recursive Let

Authors: Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret

Abstract: A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine the complexity of corresponding unification problems. A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine the complexity of corresponding unification problems. △ Less

Submitted 12 August, 2016; originally announced August 2016.

Comments: Pre-proceedings paper presented at the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016), Edinburgh, Scotland UK, 6-8 September 2016 (arXiv:1608.02534)

Report number: LOPSTR/2016/34

Journal ref: Logic-Based Program Synthesis and Transformation, LNCS 10184, pp 328-344, Springer (2016)

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)

Simulating Lattice Spin Models on Graphics Processing Units

Authors: Tal Levy, Guy Cohen, Eran Rabani

Abstract: Lattice spin models are useful for studying critical phenomena and allow the extraction of equilibrium and dynamical properties. Simulations of such systems are usually based on Monte Carlo (MC) techniques, and the main difficulty is often the large computational effort needed when approaching critical points. In this work, it is shown how such simulations can be accelerated with the use of NVIDIA… ▽ More Lattice spin models are useful for studying critical phenomena and allow the extraction of equilibrium and dynamical properties. Simulations of such systems are usually based on Monte Carlo (MC) techniques, and the main difficulty is often the large computational effort needed when approaching critical points. In this work, it is shown how such simulations can be accelerated with the use of NVIDIA graphics processing units (GPUs) using the CUDA programming architecture. We have developed two different algorithms for lattice spin models, the first useful for equilibrium properties near a second-order phase transition point and the second for dynamical slowing down near a glass transition. The algorithms are based on parallel MC techniques, and speedups from 70- to 150-fold over conventional single-threaded computer codes are obtained using consumer-grade hardware. △ Less

Submitted 3 September, 2012; originally announced September 2012.

Journal ref: Journal of Chemical Theory and Computation 6, 11, 3293-3301, 2010

Nominal Unification from a Higher-Order Perspective

Authors: Jordi Levy, Mateu Villaret

Abstract: Nominal Logic is a version of first-order logic with equality, name-binding, renaming via name-swap** and freshness of names. Contrarily to higher-order logic, bindable names, called atoms, and instantiable variables are considered as distinct entities. Moreover, atoms are capturable by instantiations, breaking a fundamental principle of lambda-calculus. Despite these differences, nominal unific… ▽ More Nominal Logic is a version of first-order logic with equality, name-binding, renaming via name-swap** and freshness of names. Contrarily to higher-order logic, bindable names, called atoms, and instantiable variables are considered as distinct entities. Moreover, atoms are capturable by instantiations, breaking a fundamental principle of lambda-calculus. Despite these differences, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be reduced to a particular fragment of higher-order unification problems: Higher-Order Pattern Unification. This reduction proves that nominal unification can be decided in quadratic deterministic time, using the linear algorithm for Higher-Order Pattern Unification. We also prove that the translation preserves most generality of unifiers. △ Less

Submitted 20 May, 2010; originally announced May 2010.

ACM Class: F.4.1

Journal ref: ACM Transactions on Computational Logics, Vol. 13, Num. 2, pp. 10, year 2012