More Like this

1. Translating Pseudo-Boolean Proofs into Boolean Clausal Proofs

   Nukala, Karthik; Choudhuri, Soumyaditya; Bryant, Randal E; Heule, Marijn J_H (October 2024, TU Wien Academic Press)

   Narodytska, Nina; Rümmer, Philipp (Ed.)

   Clausal proofs, particularly those based on the deletion resolution asymmetric tautology (DRAT) proof system, are widely used by Boolean satisfiability solvers for expressing proofs of unsatisfiability. Their success stems from their simplicity and scalability. When solvers go beyond pure propositional reasoning, however, generating clausal proofs becomes more difficult. Solvers that employ pseudo-Boolean reasoning, including cutting-planes operations, can express proofs in the VeriPB proof system, but its adoption is not widespread. We introduce PBIP (Pseudo-Boolean Implication Proof), a framework that provides an intermediate representation between VeriPB and clausal proofs. We also introduce a toolchain comprising 1) a VeriPB-to-PBIP translator that performs proof trimming and optimization, and 2) a PBIP-to-LRAT translator that makes use of proof-generating operations on ordered binary decision diagrams (BDDs) to generate clausal proofs in LRAT format, a variant of the DRAT that allows efficient checking. We demonstrate the viability of our approach, the effectiveness of our trimming, and the performance of our clausal proof generator on a set of native PB benchmarks and compare our approach to direct checking of VeriPB proofs. 

   more » « less
2. ZDD Boolean Synthesis

   Lin, Yi; Tabajara, Lucas M.; Vardi, Moshe Y. (April 2022, International Conference on Tools and Algorithms for the Construction and Analysis of Systems)

   Dana Fisman and Grigore Rosu (Ed.)

   Motivated by applications in boolean-circuit design, boolean synthesis is the process of synthesizing a boolean function with multiple outputs, given a relation between its inputs and outputs. Previous work has attempted to solve boolean functional synthesis by converting a specification formula into a Binary Decision Diagram (BDD) and quantifying existentially the output variables. We make use of the fact that the specification is usually given in the form of a Conjunctive Normal Form (CNF) formula, and we can perform resolution on a symbolic representation of a CNF formula in the form of a Zero-suppressed Binary Decision Diagram (ZDD). We adapt the realizability test to the context of CNF and ZDD, and show that the Cross operation defined in earlier work can be used for witness construction. Experiments show that our approach is complementary to BDD-based Boolean synthesis. 

   more » « less
3. Introducing Boolean Semilattices

   https://doi.org/http://dx.doi.org/10.1007/978-3-319-74772-9_4  

   Bergman, Clifford (March 2018, Don Pigozzi on Algebraic Logic)

   We present and discuss a variety of Boolean algebras with operators that is closely related to the variety generated by all complex algebras of semilattices. We consider the problem of finding a generating set for the variety, representation questions, and axiomatizability. Several interesting subvarieties are presented. We contrast our results with those obtained for a number of other varieties generated by complex algebras of groupoids. 

   more » « less
4. Boolean modelling in plant biology

   https://doi.org/10.1017/qpb.2022.26  

   Karanam, Aravind; Rappel, Wouter-Jan (January 2022, Quantitative Plant Biology)

   Abstract Signalling and genetic networks underlie most biological processes and are often complex, containing many highly connected components. Modelling these networks can provide insight into mechanisms but is challenging given that rate parameters are often not well defined. Boolean modelling, in which components can only take on a binary value with connections encoded by logic equations, is able to circumvent some of these challenges, and has emerged as a viable tool to probe these complex networks. In this review, we will give an overview of Boolean modelling, with a specific emphasis on its use in plant biology. We review how Boolean modelling can be used to describe biological networks and then discuss examples of its applications in plant genetics and plant signalling. 

   more » « less
5. Efficient Analog Circuits for Boolean Satisfiability

   https://doi.org/10.1109/TVLSI.2017.2754192  

   Yin, Xunzhao; Sedighi, Behnam; Varga, Melinda; Ercsey-Ravasz, Maria; Toroczkai, Zoltan; Hu, Xiaobo Sharon (January 2018, IEEE Transactions on Very Large Scale Integration (VLSI) Systems)