skip to main content

This content will become publicly available on August 11, 2023

Title: CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length
CDSAT (Conflict-Driven Satisfiability) is a paradigm for theory combination that works by coordinating theory modules to reason in the union of the theories in a conflict-driven manner. We generalize CDSAT to the case of nondisjoint theories by presenting a new CDSAT theory module for a theory of arrays with abstract length, which is an abstraction of the theory of arrays with length. The length function is a bridging function as it forces theories to share symbols, but the proposed abstraction limits the sharing to one predicate symbol. The CDSAT framework handles shared predicates with minimal changes, and the new module satisfies the CDSAT requirements, so that completeness is preserved.
Authors:
; ;
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
  1. Abstract

    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.Conflict-drivenprocedures 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 moduleswithin a solver for the union of the theories. This article augments CDSAT with a more generallemma learningcapability and withproof generation. Furthermore, theory modules for several theories of practical interest are shown to fulfill the requirements forcompletenessandterminationof CDSAT. Proof generation is accomplished by aproof-carryingversion of the CDSAT transition system that producesproof objectsin memory accommodating multiple proof formats. Alternatively, one can apply to CDSAT theLCF approach to proofsfrom interactive theorem proving, by defining a kernel of reasoning primitives that guarantees the correctness by construction of CDSAT proofs.

  2. 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 »of the platform and compare the performance against fixed duty-cycle baselines. Results indicate that sensors running the online energy-manager perform similar to continuously powered sensors, have a l0x higher event generation rate than the intermittently powered ones, 1.8-7x higher event detection accuracy, experience 50% fewer power failures, and are 44% more available than the sensors that maintain a constant duty-cycle.« less
  3. 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.

  4. 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 »in original phenotype descriptions and difficulties in using standardized vocabularies (ontologies). We argue that the authors describing characters are the key to the solution. Given the right tools and appropriate attribution, the authors should be in charge of developing a project's semantics and ontology. This will speed up ontology development and improve the semantic clarity of the descriptions from the moment of publication. In this presentation, we will introduce the Platform for Author-Driven Computable Data and Ontology Production for Taxonomists, which consists of three components: a web-based, ontology-aware software application called 'Character Recorder,' which features a spreadsheet as the data entry platform and provides authors with the flexibility of using their preferred terminology in recording characters for a set of specimens (this application also facilitates semantic clarity and consistency across species descriptions); a set of services that produce RDF graph data, collects terms added by authors, detects potential conflicts between terms, dispatches conflicts to the third component and updates the ontology with resolutions; and an Android mobile application, 'Conflict Resolver,' which displays ontological conflicts and accepts solutions proposed by multiple experts. a web-based, ontology-aware software application called 'Character Recorder,' which features a spreadsheet as the data entry platform and provides authors with the flexibility of using their preferred terminology in recording characters for a set of specimens (this application also facilitates semantic clarity and consistency across species descriptions); a set of services that produce RDF graph data, collects terms added by authors, detects potential conflicts between terms, dispatches conflicts to the third component and updates the ontology with resolutions; and an Android mobile application, 'Conflict Resolver,' which displays ontological conflicts and accepts solutions proposed by multiple experts. Fig. 1 shows the system diagram of the platform. The presentation will consist of: a report on the findings from a recent survey of 90+ participants on the need for a tool like Character Recorder; a methods section that describes how we provide semantics to an existing vocabulary of quantitative characters through a set of properties that explain where and how a measurement (e.g., length of perigynium beak) is taken. We also report on how a custom color palette of RGB values obtained from real specimens or high-quality specimen images, can be used to help authors choose standardized color descriptions for plant specimens; and a software demonstration, where we show how Character Recorder and Conflict Resolver can work together to construct both human-readable descriptions and RDF graphs using morphological data derived from species in the plant genus Carex (sedges). The key difference of this system from other ontology-aware systems is that authors can directly add needed terms to the ontology as they wish and can update their data according to ontology updates. a report on the findings from a recent survey of 90+ participants on the need for a tool like Character Recorder; a methods section that describes how we provide semantics to an existing vocabulary of quantitative characters through a set of properties that explain where and how a measurement (e.g., length of perigynium beak) is taken. We also report on how a custom color palette of RGB values obtained from real specimens or high-quality specimen images, can be used to help authors choose standardized color descriptions for plant specimens; and a software demonstration, where we show how Character Recorder and Conflict Resolver can work together to construct both human-readable descriptions and RDF graphs using morphological data derived from species in the plant genus Carex (sedges). The key difference of this system from other ontology-aware systems is that authors can directly add needed terms to the ontology as they wish and can update their data according to ontology updates. The software modules currently incorporated in Character Recorder and Conflict Resolver have undergone formal usability studies. We are actively recruiting Carex experts to participate in a 3-day usability study of the entire system of the Platform for Author-Driven Computable Data and Ontology Production for Taxonomists. Participants will use the platform to record 100 characters about one Carex species. In addition to usability data, we will collect the terms that participants submit to the underlying ontology and the data related to conflict resolution. Such data allow us to examine the types and the quantities of logical conflicts that may result from the terms added by the users and to use Discrete Event Simulation models to understand if and how term additions and conflict resolutions converge. We look forward to a discussion on how the tools (Character Recorder is online at http://shark.sbs.arizona.edu/chrecorder/public) described in our presentation can contribute to producing and publishing FAIR data in taxonomic studies.« less
  5. 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 »to fabricate, e.g., engineered polymer composite materials that derive their function from accurately organizing a pattern of particles embedded in the polymer matrix.

    « less