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.
- Award ID(s):
- 1816936
- NSF-PAR ID:
- 10358980
- Editor(s):
- Deharbe, David; Hyvarinen, Antti E.
- Date Published:
- Journal Name:
- Satisfiability Modulo Theories workshop, CEUR Workshop Proceedings
- Volume:
- 3185
- Page Range / eLocation ID:
- 18--37
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
more » « less
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. -
more » « less
Abstract People who hold scientific explanations for natural phenomena also hold folk explanations, and the two types of explanations compete under some circumstances. Here, we explore the question of why folk explanations persist in the face of a well‐understood scientific alternative, a phenomenon known as
explanatory coexistence . We consider two accounts: an associative account, where coexistence is driven by low‐level associations between co‐occurring ideas in experience or discourse, and a theory‐based account, where coexistence reflects high‐level competition between distinct sets of causal expectations. We present data that assess the relative contributions of these two accounts to the cognitive conflict elicited by counterintuitive scientific ideas. Participants (134 college undergraduates) verified scientific statements like “air has weight” and “bacteria have DNA” as quickly as possible, and we examined the speed and accuracy of their verifications in relation to measures of associative information (lexical co‐occurrence of the statements' subjects and predicates) and theory‐based expectations (ratings of whether the statements' subjects possess theory‐relevant attributes). Both measures explained a significant amount of variance in participants' responses, but the theory‐based measures explained three to five times more. These data suggest that the cognitive conflict elicited by counterintuitive scientific ideas typically arises from competing theories and that such ideas might be made more intuitive by strengthening scientific theories or weakening folk theories. -
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 top 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.more » « less
-
more » « less
Abstract Photon extraction and capture efficiency is a complex function of the material's composition, its molecular structure at the nanoscale, and the overall organization spanning multiple length scales. The architecture of the material defines the performance; nanostructured features within the materials enhance the energy efficiency. Photon capturing materials are largely produced through lithographic, top‐down, manufacturing schemes; however, there are limits to the smallest dimension achievable using this technology. To overcome these technological barriers, a bottom‐up nanomanufacturing is pursued. Inspired by the self‐programmed assembly of virus arrays in host cells resulting in iridescence of infected organisms, virus‐programmed, nanostructured arrays are studied to pave the way for new design principles in photon management and biology‐inspired materials science. Using the nanoparticles formed by plant viruses in combination with charged polymers (dendrimers), a bottom‐up approach is illustrated to prepare a family of broadband, low‐angular dependent antireflection mesoscale layered materials for potential application as photon management coatings. Measurement and theory demonstrate antireflectance and phototrapping properties of the virus‐programmed assembly. This opens up new bioengineering principles for the nanomanufacture of coatings and films for use in LED lighting and photovoltaics.
-
more » « less
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.
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Conference Paper:
- The DOI is not currently available.
