Search-based satisfiability procedures try to build a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input.
This content will become publicly available on August 11, 2023
- Editors:
- Deharbe, David; Hyvarinen, Antti E.
- Award ID(s):
- 1816936
- Publication Date:
- NSF-PAR ID:
- 10358980
- Journal Name:
- Satisfiability Modulo Theories workshop, CEUR Workshop Proceedings
- Volume:
- 3185
- Page Range or eLocation-ID:
- 18--37
- Sponsoring Org:
- National Science Foundation
More Like this
-
Abstract Conflict-driven procedures perform non-trivial inferences only when resolving conflicts between formulæ and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability ) is a method for conflict-driven reasoning inunions of theories . It combines inference systems for individual theories astheory modules within a solver for the union of the theories. This article augments CDSAT with a more generallemma learning capability and withproof generation . Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements forcompleteness andtermination of CDSAT. Proof generation is accomplished by aproof-carrying version of the CDSAT transition system that producesproof objects in memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT theLCF approach to proofs from interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs. -
Energy-harvesting designs typically include highly entangled app-lication-level and energy-management subsystems that span both hardware and software. This tight integration makes developing sophisticated energy-harvesting systems challenging, as developers have to consider both embedded system development and intermit-tent energy management simultaneously. Even when successful, solutions are often monolithic, produce suboptimal performance, and require substantial effort to translate to a new design. Instead, we propose a new energy-harvesting power management architecture, Altair that offloads all energy-management operations to the power supply itself while making the power supply programmable. Altair introduces an energy supervisor and a standard interface to enable an abstraction layer between the power supply hardware and the running application, making both replaceable and recon-figurable. To ensure minimal resource conflict on the application processor, while running resource-hungry optimization techniques in the supervisor, we implement the Altair design in a lower power microcontroller that runs in parallel with the application. We also develop a programmable power supply module and a software library for seamless application development with Altair. We evaluate the versatility of the proposed architecture across a spectrum of IoT devices and demonstrate the generality of the plat-form. We also design and implement an online energy-management technique using reinforcement learning on topmore »
-
Theories such as social baseline theory have argued that social groups serve a regulatory function but have not explored whether this regulatory process carries costs for the group. Allostatic load, the wear and tear on regulatory systems caused by chronic or frequent stress, is marked by diminished stress system flexibility and compromised recovery. We argue that allostatic load may develop within social groups as well and provide a model for how relationship dysfunction operates. Social allostatic load may be characterized by processes such as groups becoming locked into static patterns of interaction and may ultimately lead to up-regulation or down-regulation of a group’s set point, or the optimal range of arousal or affect around which the group tends to converge. Many studies of emotional and physiological linkage within groups have reported that highly correlated states of arousal, which may reflect failure to maintain a group-level regulatory baseline, occur in the context of stress, conflict, and relationship distress. Relationship strain may also place greater demands on neurocognitive regulatory processes. Just as allostatic load may be detrimental to individual health, social allostatic load may corrode relationship quality.
-
It takes great effort to manually or semi-automatically convert free-text phenotype narratives (e.g., morphological descriptions in taxonomic works) to a computable format before they can be used in large-scale analyses. We argue that neither a manual curation approach nor an information extraction approach based on machine learning is a sustainable solution to produce computable phenotypic data that are FAIR (Findable, Accessible, Interoperable, Reusable) (Wilkinson et al. 2016). This is because these approaches do not scale to all biodiversity, and they do not stop the publication of free-text phenotypes that would need post-publication curation. In addition, both manual and machine learning approaches face great challenges: the problem of inter-curator variation (curators interpret/convert a phenotype differently from each other) in manual curation, and keywords to ontology concept translation in automated information extraction, make it difficult for either approach to produce data that are truly FAIR. Our empirical studies show that inter-curator variation in translating phenotype characters to Entity-Quality statements (Mabee et al. 2007) is as high as 40% even within a single project. With this level of variation, curated data integrated from multiple curation projects may still not be FAIR. The key causes of this variation have been identified as semantic vaguenessmore »
-
Ultrasound directed self-assembly (DSA) allows organizing particles dispersed in a fluid medium into user-specified patterns, driven by the acoustic radiation force associated with a standing ultrasound wave. Accurate control of the spatial organization of the particles in the fluid medium requires accounting for medium viscosity and particle volume fraction. However, existing theories consider an inviscid medium or only determine the effect of viscosity on the magnitude of the acoustic radiation force rather than the locations where particles assemble, which is crucial information to use ultrasound DSA as a fabrication method. We experimentally measure the deviation between locations where spherical microparticles assemble during ultrasound DSA as a function of medium viscosity and particle volume fraction. Additionally, we simulate the experiments using coupled-phase theory and the time-averaged acoustic radiation potential, and we derive best-fit equations that predict the deviation between locations where particles assemble during ultrasound DSA when using viscous and inviscid theory. We show that the deviation between locations where particles assemble in viscous and inviscid media first increases and then decreases with increasing particle volume fraction and medium viscosity, which we explain by means of the sound propagation velocity of the mixture. This work has implications for using ultrasound DSAmore »
