More Like this

1. CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length

   Bonacina, Maria Paola ; Graham-Lengrand, Stephane ; Shankar, Natarajan ( August 2022 , Satisfiability Modulo Theories workshop, CEUR Workshop Proceedings)

   Deharbe, David ; Hyvarinen, Antti E. (Ed.)

   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.
2. SMC: Satisfiability Modulo Convex Programming

   https://doi.org/10.1109/JPROC.2018.2849003  

   Shoukry, Yasser ; Nuzzo, Pierluigi ; Sangiovanni-Vincentelli, Alberto L. ; Seshia, Sanjit A. ; Pappas, George J. ; Tabuada, Paulo ( January 2018 , Proceedings of the IEEE)

   The design of cyber-physical systems (CPSs) requires methods and tools that can efficiently reason about the interaction between discrete models, e.g., representing the behaviors of ``cyber'' components, and continuous models of physical processes. Boolean methods such as satisfiability (SAT) solving are successful in tackling large combinatorial search problems for the design and verification of hardware and software components. On the other hand, problems in control, communications, signal processing, and machine learning often rely on convex programming as a powerful solution engine. However, despite their strengths, neither approach would work in isolation for CPSs. In this paper, we present a new satisfiability modulo convex programming (SMC) framework that integrates SAT solving and convex optimization to efficiently reason about Boolean and convex constraints at the same time. We exploit the properties of a class of logic formulas over Boolean and nonlinear real predicates, termed monotone satisfiability modulo convex formulas, whose satisfiability can be checked via a finite number of convex programs. Following the lazy satisfiability modulo theory (SMT) paradigm, we develop a new decision procedure for monotone SMC formulas, which coordinates SAT solving and convex programming to provide a satisfying assignment or determine that the formula is unsatisfiable. A key step inmore »our coordination scheme is the efficient generation of succinct infeasibility proofs for inconsistent constraints that can support conflict-driven learning and accelerate the search. We demonstrate our approach on different CPS design problems, including spacecraft docking mission control, robotic motion planning, and secure state estimation. We show that SMC can handle more complex problem instances than state-of-the-art alternative techniques based on SMT solving and mixed integer convex programming.« less
3. Clausal Proofs for Pseudo-Boolean Reasoning

   https://doi.org/10.1007/978-3-030-99524-9_25  

   Bryant, Randal E. ; Heule, Marijn J. ( January 2022 , International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

   Fisman, D. ; Rosu, G. (Ed.)

   When augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has no solution. By converting the intermediate constraints generated by the PB solver into ordered binary decision diagrams (BDDs), a proof-generating, BDD-based SAT solver can then produce a clausal proof that the input formula is unsatisfiable. Working together, the two solvers can generate proofs of unsatisfiability for problems that are intractable for other proof-generating SAT solvers. The PB solver can, at times, detect that the proof can exploit modular arithmetic to give smaller BDD representations and therefore shorter proofs.
4. Simulating Strong Practical Proof Systems with Extended Resolution

   https://doi.org/10.1007/s10817-020-09554-z  

   Kiesl, Benjamin ; Rebola-Pardo, Adrián ; Heule, Marijn J. ; Biere, Armin ( July 2020 , Journal of Automated Reasoning)

   Proof systems for propositional logic provide the basis for decision procedures that determine the satisfiability status of logical formulas. While the well-known proof system of extended resolution—introduced by Tseitin in the sixties—allows for the compact representation of proofs, modern SAT solvers (i.e., tools for deciding propositional logic) are based on different proof systems that capture practical solving techniques in an elegant way. The most popular of these proof systems is likely DRAT, which is considered the de-facto standard in SAT solving. Moreover, just recently, the proof system DPR has been proposed as a generalization of DRAT that allows for short proofs without the need of new variables. Since every extended-resolution proof can be regarded as a DRAT proof and since every DRAT proof is also a DPR proof, it was clear that both DRAT and DPR generalize extended resolution. In this paper, we show that—from the viewpoint of proof complexity—these two systems are no stronger than extended resolution. We do so by showing that (1) extended resolution polynomially simulates DRAT and (2) DRAT polynomially simulates DPR. We implemented our simulations as proof-transformation tools and evaluated them to observe their behavior in practice. Finally, as a side note, we show howmore »Kullmann’s proof system based on blocked clauses (another generalization of extended resolution) is related to the other systems.« less
5. The computational thinking for science (CT-S) framework: operationalizing CT-S for K–12 science education researchers and educators

   https://doi.org/10.1186/s40594-022-00391-7  

   Hurt, Timothy ; Greenwald, Eric ; Allan, Sara ; Cannady, Matthew A. ; Krakowski, Ari ; Brodsky, Lauren ; Collins, Melissa A. ; Montgomery, Ryan ; Dorph, Rena ( January 2023 , International Journal of STEM Education)

   Contemporary science is a field that is becoming increasingly computational. Today’s scientists not only leverage computational tools to conduct their investigations, they often must contribute to the design of the computational tools for their specific research. From a science education perspective, for students to learn authentic science practices, students must learn to use the tools of the trade. This necessity in science education has shaped recent K–12 science standards including the Next Generation Science Standards, which explicitly mention the use of computational tools and simulations. These standards, in particular, have gone further and mandated thatcomputational thinkingbe taught and leveraged as a practice of science. While computational thinking is not a new term, its inclusion in K–12 science standards has led to confusion about what the term means in the context of science learning and to questions about how to differentiate computational thinking from other commonly taught cognitive skills in science like problem-solving, mathematical reasoning, and critical thinking. In this paper, we propose a definition ofcomputational thinking for science(CT-S) and a framework for its operationalization in K–12 science education. We situate our definition and framework in Activity Theory, from the learning sciences, in order to position computational thinking as anmore »input to and outcome of science learning that is mediated by computational tools.

   « less