An efficient solver for weighted Max-SAT

We present a new branch and bound algorithm for weighted Max-SAT, called Lazy which incorporates original data structures and inference rules, as well as a lower bound of better quality. We provide experimental evidence that our solver is very competitive and outperforms some of the best performing Max-SAT and weighted Max-SAT solvers on a wide range of instances.

A Write-Based Solver for SAT Modulo the Theory of Arrays

The extensional theory of arrays is one of the most important ones for applications of SAT Modulo Theories (SMT) to hardware and software verification. Here we present a new T-solver for arrays in the context of the DPLL(T) approach to SMT. The main characteristics of our solver are: (i) no translation of writes into reads is needed, (ii) there is no axiom instantiation, and (iii) the T-solver interacts with the Boolean engine by asking to split on equality literals between indices. As far as we know, this is the first accurate description of an array solver integrated in a state-of-the-art SMT solver and, unlike most state-of-the-art solvers, it is not based on a lazy instantiation of the array axioms. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals

An approximation algorithm for #k-SAT

"Vegeu el resum a l'inici del document del fitxer adjunt"

Disseny, implementació i avaluació d'algorismes Max-SAT multivaluats

La finalitat d'aquest projecte és definir el problema Max-SAT amb codificació multiavaluada, implementar algorismes exactes de resolució del problema i construir un generador aleatori de problemes que permeti avaluar aquests algorismes.

SAT Modulo Linear Arithmetic for Solving Polynomial

Polynomial constraint solving plays a prominent role in several areas of hardware and software analysis and verification, e.g., termination proving, program invariant generation and hybrid system verification, to name a few. In this paper we propose a new method for solving non-linear constraints based on encoding the problem into an SMT problem considering only linear arithmetic. Unlike other existing methods, our method focuses on proving satisfiability of the constraints rather than on proving unsatisfiability, which is more relevant in several applications as we illustrate with several examples. Nevertheless, we also present new techniques based on the analysis of unsatisfiable cores that allow one to efficiently prove unsatisfiability too for a broad class of problems. The power of our approach is demonstrated by means of extensive experiments comparing our prototype with state-of-the-art tools on benchmarks taken both from the academic and the industrial world.

Generating hard SAT/CSP instances using expander graphs

In this paper we provide a new method to generate hard k-SAT instances. We incrementally construct a high girth bipartite incidence graph of the k-SAT instance. Having high girth assures high expansion for the graph, and high expansion implies high resolution width. We have extended this approach to generate hard n-ary CSP instances and we have also adapted this idea to increase the expansion of the system of linear equations used to generate XORSAT instances, being able to produce harder satisfiable instances than former generators.

Edge matching puzzles as hard SAT/CSP benchmarks

Recently, edge matching puzzles, an NP-complete problem, have rececived, thanks to money-prized contests, considerable attention from wide audiences. We consider these competitions not only a challenge for SAT/CSP solving techniques but also as an opportunity to showcase the advances in the SAT/CSP community to a general audience. This paper studies the NP-complete problem of edge matching puzzles focusing on providing generation models of problem instances of variable hardness and on its resolution through the application of SAT and CSP techniques. From the generation side, we also identify the phase transition phenomena for each model. As solving methods, we employ both; SAT solvers through the translation to a SAT formula, and two ad-hoc CSP solvers we have developed, with different levels of consistency, employing several generic and specialized heuristics. Finally, we conducted an extensive experimental investigation to identify the hardest generation models and the best performing solving techniques.

Sonda de infrarrojo cercano como herramienta para evaluar la composición de grasa subcutánea de cerdos alimentados con CLA

El objetivo de este trabajo fue la utilización de la tecnología de Infrarrojo cercano por aplicación directa de una fibra óptica en tejido adiposo de cerdos alimentados con diferentes dietas (CONTROL, CÍTRICOS y CLA). Para ello, 265 animales fueron alimentados con tres dietas diferentes y se analizó el perfil de ácidos grasos en la grasa del jamón mediante cromatografía de gases y FT-NIR (espectroscopia de infrarrojo cercano con transformada de Fourier). La adquisición de espectros se realizó con un espectrómetro Optics Matrix-F duplex de Bruker equipado con una sonda de contacto IN-268-2. Los cerdos que fueron alimentados con la dieta enriquecida en CLA mostraron diferencias significativas tanto en la composición de ácidos grasos como en los espectros de NIR ya que la ingesta de CLA aumentó el porcentaje de ácidos grasos saturados (SAT) y poliinsaturados (PUFA) mientras que los monoinsaturados (MUFA) disminuyeron con respecto a las otras dietas. Los resultados sugieren que la espectroscopia de infrarrojo cercano es un método rápido y de fácil implementación para identificar animales alimentados con diferentes dietas.

A numerical solver for a nonlinear Fokker-Planck equation representation of neuronal network dynamics

To describe the collective behavior of large ensembles of neurons in neuronal network, a kinetic theory description was developed in [13, 12], where a macroscopic representation of the network dynamics was directly derived from the microscopic dynamics of individual neurons, which are modeled by conductance-based, linear, integrate-and-fire point neurons. A diffusion approximation then led to a nonlinear Fokker-Planck equation for the probability density function of neuronal membrane potentials and synaptic conductances. In this work, we propose a deterministic numerical scheme for a Fokker-Planck model of an excitatory-only network. Our numerical solver allows us to obtain the time evolution of probability distribution functions, and thus, the evolution of all possible macroscopic quantities that are given by suitable moments of the probability density function. We show that this deterministic scheme is capable of capturing the bistability of stationary states observed in Monte Carlo simulations. Moreover, the transient behavior of the firing rates computed from the Fokker-Planck equation is analyzed in this bistable situation, where a bifurcation scenario, of asynchronous convergence towards stationary states, periodic synchronous solutions or damped oscillatory convergence towards stationary states, can be uncovered by increasing the strength of the excitatory coupling. Finally, the computation of moments of the probability distribution allows us to validate the applicability of a moment closure assumption used in [13] to further simplify the kinetic theory.

A block solver for the exponentally fitted IIPG-0 method

We consider an exponentially fitted discontinuous Galerkin method for advection dominated problems and propose a block solver for the resulting linear systems. In the case of strong advection the solver is robust with respect to the advection direction and the number of unknowns.

A 48-week study of fat molecular alterations in HIV naïve patients starting tenofovir/emtricitabine with lopinavir/ritonavir or efavirenz: Greater deleterious effects of efavirenz.

S’han descrit informes contradictoris sobre els efectes d’Efavirenz (EFV) i lopinavir/ritonavir (LPV/r) al teixit adipós subcutani (SAT). L’objectiu d’aquest estudi era evaluar els efectes moleculars i clínics de LPV/r i EFV, tots dos en combinació amb tenofovir/emtricitabina (TDF/FTC), sobre el SAT dels pacients infectats per VIH sense tractament antirretroviral previ. Després de 48 setmanes de tractament, TDF/FTC més LPV/r va augmentar de forma significativa el greix de les extremitats i els paràmetres lipídics, mentre que TDF/FTC/EFV només va augmentar de forma significativa el colesterol total i LDL. La expressió dels gens implicats en la diferenciació dels adipòcits i dels gens relacionats amb la mitocondria no va canviar de forma significativa en el SAT dels pacients exposats a LPV/r, mentre que Cyt b i els gens relacionats amb la imflamació estaven estimulats de forma significativa en el SAT dels pacients exposats a EFV.

Projecte P.I.T.O.S (Projecte d'informació telefònica d'orientació al S.A.T)

JCM és una empresa dedicada al disseny de sistemes de control d’accés. Disposa d’uns equips elèctrics amb molts paràmetres configurables, així es poden utilitzar en molts tipus d’instal•lació. Aquets paràmetres són configurables pels clients. JCM, disposa d’un servei d’atenció telefònica (SAT), que intenta donar solucions a tots els problemes que puguin sorgir als clients. Sovint, no poden donar suport als dubtes dels clients per culpa de la poca informació que reben a través del client. L'objectiu del projecte és resoldre el problema de falta d'informació i mala comunicació per millorar la qualitat del servei que ofereix el SAT. La solució, no ha d’alterar el cost de producció del producte. S’ha de tenir en compte també que els equips poden estar instal•lats en qualsevol part del món i que només es poden utilitzar recursos de fàcil accés per tots els clients. Per complir amb aquests objectius, emetrem un missatge, a través del brunzidor del equip, amb la informació de configuració de l'equip. Aquest missatge viatjarà a través de la xarxa telefònica fins al SAT. Un cop allà, el descodificarem i n'enviarem les dades a un PC perquè pugui presentar les dades sobre la configuració de una forma clara pel SAT.

A Threat to a Virtual Hand Elicits Motor Cortex Activation

We report an experiment where participants observed an attack on their virtual body as experienced in an immersive virtual reality (IVR) system. Participants sat by a table with their right hand resting upon it. In IVR, they saw a virtual table that was registered with the real one, and they had a virtual body that substituted their real body seen from a first person perspective. The virtual right hand was collocated with their real right hand. Event-related brain potentials were recorded in two conditions, one where the participant"s virtual hand was attacked with a knife and a control condition where the knife only struck the virtual table. Significantly greater P450 potentials were obtained in the attack condition confirming our expectations that participants had a strong illusion of the virtual hand being their own, which was also strongly supported by questionnaire responses. Higher levels of subjective virtual hand ownership correlated with larger P450 amplitudes. Mu-rhythm event-related desynchronization in the motor cortex and readiness potential (C3C4) negativity were clearly observed when the virtual hand was threatened as would be expected, if the real hand was threatened and the participant tried to avoid harm. Our results support the idea that event-related potentials may provide a promising non-subjective measure of virtual embodiment. They also support previous experiments on pain observation and are placed into context of similar experiments and studies of body perception and body ownership within cognitive neuroscience.

Laboratory diagnosis of brucellosis in a rural endemic area in northeastern Spain

Sera obtained from 62 patients from four mountain counties in Catalonia (Northeastern Spain), in whom brucellosis had been diagnosed on the basis of clinical evidence and/or personal history, were analyzed using the rose Bengal test, standard serum agglutination test (SAT), Coombs" test, ELISA, and complement fixation. The diagnosis was further confirmed through blood cultures. Clinical evidence, epidemiology, and the results from serologic tests were used to assign patients to one of two groups: group 1 (n = 38) patients had primary infections, whereas group 2 (n = 24) patients had been previously exposed to the microorganism, i.e. re-infection of group 2 individuals occurred after long periods of time during which no active infection by Brucella had been detected. Receivingoperating charts (ROC) were used to determine the diagnostic value of the different tests and to establish discriminant values. Blood culture was a valuable diagnostic tool in group 1 (0.92 sensitivity) but was inappropriate in group 2 (0.08). The combination of positive rose Bengal test and agglutination ≥1/160 was valid for diagnosis in group 1. In group 2, agglutination < 1/160 (including negative agglutination) did not rule out brucellosis. The combination of positive rose Bengal test and Coombs" test ≥1/320 was the best diagnostic criterion (0.8 specificity; 1 sensitivity). ELISA (for IgG, IgM, or both) did not improve diagnostic accuracy