Connection and convenience come at a cost, particularly in the Internet of Things (IoT), where smart devices such as bulbs and surveillance cameras widen the attack surface for malicious actors. Intrusion Detection Systems (IDSs) are a critical line of defense, but their effectiveness must be balanced with strict resource constraints across edge, fog, and cloud layers. In this work, we propose lightweight machine learning (ML) and deep learning (DL) models for deployment across the edge–fog–cloud continuum, evaluating eight models on the RT-IoT2022 dataset. Using Optuna for hyperparameter tuning, we find that the ensemble models perform best, with LightGBM achieving the highest macro-F1 score (98.07%). However, a compact 28.8 KB Fully Connected Neural Network (FCNN) offers a favorable trade-off, attaining a macro-F1 of 94.80% with consistent sub-millisecond inference and relatively low power usage across all devices. Notably, while neural networks may not always match ensemble models in classification performance, they exhibit comparatively lower variability in inference times, making them attractive where predictability and throughput stability are crucial. Our statistical testing confirms the superiority of ensemble models while quantifying the gaps in performance. We further analyze the deployment across diverse hardware and compare ONNX runtimes against native C/C++ code generation to illustrate the convenience–performance trade-offs. We note that while quantization preserves accuracy, it can increase latency or power consumption for already-small models, cautioning against its blanket adoption. Finally, we release a reproducible end-to-end pipeline and provide practical deployment guidelines to support model and device selection under heterogeneous IoT constraints.

Women's representation in engineering has progressively increased worldwide, yet significant gender gaps remain in enrollment, retention, and professional participation. Globally, women constitute a minority within engineering programs-commonly between 20% and 30% of total enrollments-while their progression into leadership and industry roles remains comparatively low. In the United Arab Emirates (UAE), government-driven initiatives and cultural shifts have accelerated women's engagement in engineering disciplines. Female engineering enrollment in many UAE universities is on an upward trajectory, in some cases approaching or surpassing international averages. Despite this encouraging trend, challenges persist, including underrepresentation in advanced research roles and slower progression into senior industry positions. Against this broader landscape, the American University of Sharjah (AUS) demonstrates a notable increase in female student intake and sustained engagement in its engineering programs. AUS's targeted recruitment efforts, supportive campus environment, and mentorship opportunities contribute to higher female retention rates and promising career trajectories postgraduation. AUS efforts specifically illustrate how institutional support, and societal endorsement can catalyze women's advancement and success in engineering at levels comparable to-and in certain cases exceeding-international standards. This paper shares the current practices and support mechanisms adopted by the College of Engineering at AUS, to enhance the Women's participation and progression within the Engineering Discipline.

The College of Engineering (CEN) at the American University of Sharjah (@ www.aus.edu) offers seven undergraduate programs. Six engineering programs in Civil, Chemical, Electrical, Computer, Industrial and Mechanical engineering, as well as a Computer Science major. The college believes that developing and maintaining an undergraduate research program benefits both students and faculty mentors and the education experience in general. Incorporating a research component coupled with a sound academic curriculum enables students to develop independent critical thinking skills along with oral and written communication skills. A well-designed research experience impacts valuable learning objectives that would no doubt have a lasting influence as undergraduates prepare for their professional career. At the beginning of Fall, 2021 semester, the college working with the Office of Research and Graduate Studies in the university initiated an undergraduate research program and allocated a sizable fund for it. A call for proposals was sent out to students, seeking individual or group proposals supervised by a faculty member. In Fall 2021, the committee responsible received a total of 19 proposals. Another call was sent out for the Spring 2022 semester. This experiment is repeated, with the numbers of proposals reaching 43 in Fall 2022 with the quality of the proposed work improving with every cycle because of the newly established competitive ecosystem among the students. The nature of the projects varied from theoretical, to simulation based to experimental. The deliverables ranged from a building working prototype, to winning a local or regional competition to publishing the outcomes of the work in a reputable professional conference or journal. The aim of this article is to share the path followed to infuse this research experience into the existing college culture, to layout the mechanisms by which we intend to measure the effectiveness of this approach in enriching the undergraduate research experience for engineering students and finally identify ways of improving it.

The Internet of Tangible Things (IoTT) provides new opportunities for building technology-enhanced learning systems that wirelessly connect tangible sensor data to remote learning services. This paper presents the design and implementation of an IoTT voice driven learning platform that uses Amazon Alexa along with sensor-enabled wireless dice to build tangible and interactive math games for kindergarten and primary school children. The wireless dice used sensors in a 9-axis IMU to accurately detect the face each die falls on and sent this information to Amazon Web Services (AWS) using the MQTT protocol using AWS-IoT service to enact arithmetic learning scenarios. An initial evaluation shows that most children from ages 5 to 9 enjoyed playing with this system. Half the children liked everything about the game, and they all liked the concept. This game is a first step towards a new genre of educational learning technology called Internet of Tangible Learning Things (IoTLT).

One out of four deaths is caused by heart related issues. Acting upon early signs of heart disease can, thus, drastically increase probability of saving lives. This paper discusses a cost-effective and reliable method of diagnosing heart abnormalities by using mobile phones that are nowadays typically available to an average user. A mobile application is developed to detect heart abnormal activities using either a digital stethoscope measurement as input, or a mobile recording of the heart beat using the mobile's microphone. To process the raw heart sound data, we first denoise the signal using wavelet transforms, and then apply machine learning techniques, namely, Convolutional Neural Networks for the classification of the stored heart sounds. A database consisting of recorded human heart sounds and their corresponding diagnosis is used to train the neural network. Moreover, neural network fine-tuning techniques such as ADAM Regularization is used to smoothen the prediction process. The proposed approach is tested on heart sound signals, that are 5 to 8 seconds long, and is shown to perform with an accuracy of 94.2% on the validation set.

Remote patient monitoring (RPM) uses technology to assess patients' health within and beyond the healthcare facilities. RPM is becoming a reality by connecting the patient's healthcare devices to the Internet. Modern healthcare devices come with a cloud-based support that provides patients with new features such as the broad network access to their vitals' readings from anywhere. This shift of cloud-based support brought a new way to interact with the patients' devices, as well as, new challenges that are different from the traditional Bluetooth interaction that is heavily studied in the literature. In real situations, patients usually have multiple devices to measure different vital signs that are made by different providers. Hence, it is not possible with the current approaches to have all patient vital readings consolidated in a single location. This consolidation enables the management of the chronic disorders and to analyze the health trends as part of the valuation of the treatment process. This work proposes a cloud-based brokering solution that seamlessly integrates multiple health cloud providers through a set of services that uses the web services cloud standard for the purpose of remote patient monitoring application. This work is validated by a prototype implementation.

Autism Spectrum Disorder (ASD) is one of the major mental disorders in terms of neurodevelopment brain functions. The three types of symptoms which Autistic patients exhibit are: social development, difficulty in communication and unusual behavior. Unfortunately, based on the nature of ASD, it cannot be diagnosed through the help of applications. However, applications can be a tremendous help in monitoring and the treatment of patients. This work presents an architectural solution that enables the interoperability between an autistic person and caregivers to contribute on the treatment and monitoring to persons with ASD. The solution is implemented by creating a mobile application and tested with a population in an Autism center. The results show that the application made a positive treatment contribution to a person with ASD.

This paper aims to provide a Parkinson's Disease (PD) symptoms assessment tool using an Android smartphone application that allows PD patients to assess their symptoms using both quantitative and qualitative tests. Simple touch screen and motion tests focus on objectively measuring PD symptoms, whereas a questionnaire targets the subjective ones. The concatenation of the collected results will allow the application to accurately target several PD symptoms without visual or traditional assessment. Physicians, hospitals, and clinics will then be able to receive this data over the network for further assessment, analysis, and research. This enables the self-monitoring of patients, as well as remote monitoring from physicians in clinics and hospitals. In addition to this, this application aims to expand PD research and provide improvements to the current treatment process. Ultimately, the aim is to enable thousands of people, anywhere and at any time, to easily diagnose and assess the PD before visiting a specialist.

The availability of built-in sensors in mobile phones has enabled a host of innovative applications. One class of applications deals with detecting a user's emotions. Previous applications have primarily relied on recording and displaying self-reported emotions. This paper presents an intelligent emotion detection system for mobile phones implemented as a smart keyboard. The smart keyboard independently infers a user's emotional state using machine learning techniques. The system uses accelerometer readings and various aspect of typing behavior like speed, number of backspaces, and time delay between letters to train a classifier to predict emotions. Naïve Bayes, J48, IBK, Multi-response linear regression and SVM were evaluated and J48 was found to be the best classifier with over 90% accuracy and precision. In addition to providing emotive feedback to individual users, the system also uses geo-tagged data to collect and display emotional states of regions or countries through a website.

Increasing cyber-security presents an ongoing challenge to security professionals. Research continuously suggests that online users are a weak link in information security. This research explores the relationship between cyber-security and cultural, personality and demographic variables.

mHealth is a growing field that enables individuals to monitor their health status and facilitates the sharing of medical records with physicians and between hospitals anytime and anywhere. Unfortunately, smartphones and mHealth applications are still vulnerable to a wide range of security threats due to their portability and weaknesses in management and design. Nevertheless, mHealth users are becoming more aware of the security and privacy issues related to their personal healthcare information. This survey discusses the security and privacy issues in current mHealth systems and their impact. We also discuss the latest threats, attacks and proposed countermeasures that could support secure sensitive mHealth systems. Finally, we conclude with a brief summary of open security problems that still need to be addressed in the mHealth field.

Abstract Port scanning is one of the most popular reconnaissance techniques that many attackers use to profile running services on a potential target before launching an attack. Many port scanning detection mechanisms have been suggested in literature. To test the proposed detection approaches, researchers use data sets that are available online or simulate their own. However, the available data sets do not provide complete logs and are usually outdated. Furthermore, the simulated data sets provide logs that do not resemble real‒life scenarios. These deficiencies in the available data sets highly affect the performance of testing the intrusion detection systems (IDSs) and result in poor evaluations. Meanwhile, very little work has been done on generating port scanning benchmarks that researchers can use to test their detection methods. In this work, we suggest a simulation framework using OMNeT++ to generate benchmarks that resemble real‒life traffic. We approach the problem by dividing it into three modules: (1) topology creation; (2) good traffic generation; and (3) bad traffic generation, each of which are made realistic, similar to deployed and usable networks. The benchmark is then tested using Snort and MalwareAnalysis. The tested IDSs were not able to catch many of the generated port scanning attacks, specifically the slow and distributed ones. We also measured the attack detection efficiency of the IDSs under different loads of background activities. Hence, the proposed framework and the annotated benchmarks will provide researchers and industry with an effective way of testing the power of IDSs' port scanning detection modules. Copyright © 2014 John Wiley & Sons, Ltd.

Obstructive Sleep Apnea (OSA) is a common sleep disorder which is characterized by recurrent blockage of the upper airway, often resulting in oxygen desaturation. Attended overnight polysomnography (PSG) has been recommended as the golden standard for the diagnostic of OSA at hospitals, which requires an expensive attended overnight stay at a hospital with considerable wiring between the PSG device and the human body. In this work, we implement a reliable, comfortable, inexpensive, and easily available portable device that allows users to apply the OSA test at home without the need for attended overnight tests. The design takes advantage of a smartphone's built-in sensors, pervasiveness, computational capabilities, and user-friendly interface to screen OSA. We extract three main physiological signals to diagnose OSA which are (1) oxygen saturation using an external oximeter, (2) respiratory effort using the smartphone's built-in microphone, and (3) body movement using the smartphone's built-in accelerometer. The signals are analyzed on the smartphone to screen the OSA. Finally, we examine our system's ability to screen the disease as compared to the golden standard by testing it on 15 subjects. Results show that 100% of the sick subjects were correctly classified as having OSA, and 85.7% of the healthy subjects were correctly classified as not having OSA. These preliminary results demonstrate the effectiveness of the proposed system when compared to the golden standard and emphasize the important role of smartphones in healthcare.

Port scanning is one of the most popular reconnaissance techniques that many attackers use to profile running services on a potential target before launching an attack. Many port scanning detection mechanisms have been suggested in literature. However, very little work has been done on generating port scanning benchmarks that researchers can use to test their detection methods. In this paper, we suggest a simulation framework using OMNeT++ to generate benchmarks that resemble real-life traffic. We approach the problem by dividing it into three modules (topology creation, good traffic generation, bad traffic generation), each of which we make realistic, similar to deployed and usable networks. Hence the resultant benchmark is annotated and made public.

Obstructive Sleep Apnea (OSA) is a sleeping disorder characterized by the repetitive reduction of airflow during sleep. In this paper, we discuss the design and implementation of a user-friendly mobile application developed on multiple platforms (Windows and Android) to monitor and detect symptoms of sleep apnea using the smart phone's built-in sensors. The purpose of the application, Sleep Apnea Monitor (SAM), is to allow users to get a sense of whether or not they are likely to have sleep apnea, before continuing with more expensive and advanced sleep tests. In addition, SAM provides doctors and sleep specialists with remote access to patients' records and allows them to confirm their initial diagnosis. The parameters measured by this application are breathing patterns and movement patterns, which are recorded respectively using the built-in microphone and accelerometer. The recorded data is sent to a server for analysis in order to diagnose patients and maintain geographical studies of areas with sleep apnea patterns. The application is successfully tested among a number of users in the UAE. The system diagnoses and reports the level of the user's sleep apnea. In addition, doctors can remotely monitor users through the website, which is interfaced with Google Maps to keep track of user locations, and keep track of their analysed records.

Improvements over recent years in the performance of Integer Linear Programming (ILP) and Boolean Satisfiability (SAT) solvers have encouraged the modeling of complex engineering problems as ILP. An example is the Clustering Problem in Mobile Ad-Hoc Networks (MANETs). The Clustering Problem in MANETs consists of selecting the most suitable nodes of a given MANET topology as clusterheads, and ensuring that regular nodes are connected to clusterheads such that the lifetime of the network is maximized. This paper proposes enhanced ILP formulations for the Clustering Problem, through the enablement of multi-hop connections and intra-cluster communication, and assesses the performance of state-of-the art generic ILP and SAT solvers in solving the enhanced formulations.

Abstract Wired and wireless networks are being attacked and hacked on continuous basis. One of the critical pieces of information the attacker needs to know is the open ports on the victim's machine, thus the attacker does what is called port scanning. Port scanning is considered one of the dangerous attacks that intrusion detection tries to detect. Snort, a famous network intrusion detection system (NIDS), detects a port scanning attack by combining and analyzing various traffic parameters. Because these parameters cannot be easily combined using a mathematical formula, fuzzy logic can be used to combine them; fuzzy logic can also reduce the number of false alarms. This paper presents a novel approach, based on fuzzy logic, to detect port scanning attacks. A fuzzy logic controller is designed and integrated with Snort in order to enhance the functionality of port scanning detection. Experiments are carried out in both wired and wireless networks. The results show that applying fuzzy logic adds to the accuracy of determining bad traffic. Moreover, it gives a level of degree for each type of port scanning attack. Copyright © 2010 John Wiley & Sons, Ltd.

This paper presents a new technique for multipath detection in wideband mobile radio systems. An intelligent search algorithm using Boolean Satisfiability (SAT) techniques is used to search for the multipath delays. The proposed algorithm finds the multipath components with high probability and hence allows the system to utilize the inherent diversity in these components to mitigate channel fading. Simulation results indicate that the system can achieve 90% detection or higher of all paths at low signal-to-noise ratio under frequency-selective Rayleigh fading conditions.

This paper describes a method of implementing two factor authentication using mobile phones. The proposed method guarantees that authenticating to services, such as online banking or ATM machines, is done in a very secure manner. The proposed system involves using a mobile phone as a software token for one time password generation. The generated one time password is valid for only a short user-defined period of time and is generated by factors that are unique to both, the user and the mobile device itself. Additionally, an SMS-based mechanism is implemented as both a backup mechanism for retrieving the password and as a possible mean of synchronization. The proposed method has been implemented and tested. Initial results show the success of the proposed method.

The wide spread of mobiles as handheld devices would naturally lead to various innovative applications that makes use of their ever increasing presence in our daily life. One such application is location-tracking in indoor environments. In this paper we discuss the implementation of a simple and cost effective system that assists users in tracking colleagues and friends within a campus environment. The system uses the information built in a typical mobile such as its IMEI and IMSI and the various WiFi access points on campuses to pin point a user's position. A mobile application program communicates with a web server and a GSM modem to provide users with real time data related to a person's movements and location.

In mobile radio communication systems using spread spectrum technology, an accurate estimate of the signal propagation delay is needed in order to recover the transmitted data. This process is usually done using a pseudo noise (PN) code acquisition algorithm to search for the correct propagation delay within a window of possible delays. In this paper, we propose a new approach to solving the PN code acquisition problem using advanced Boolean satisfiability (SAT) techniques. SAT solvers use intelligent search algorithms that can traverse the search space and efficiently prune parts that contain no solutions. These solvers have recently been used to solve many challenging problems in Engineering and Computer Science. In this paper, we show how to formulate the PN code acquisition problem as a SAT instance and evaluate the use of advanced SAT techniques in solving the problem. Our approach is verified by simulation and presented results indicate that the proposed system achieves a detection probability for the correct delay of almost 100% for all practical cases.

Optical networks consist of switches that are connected using fiber optics links. Each link consists of a set of wavelengths and each wavelength can be used by one or more users to transmit information between two switches. In order to establish a connection between the source and destination nodes, a set of switches and links must be efficiently selected. This is known as the routing problem. A wavelength is then assigned in each selected link to establish the connection. This is known as the wavelength assignment problem. The problem of routing and wavelength assignment (RWA) in optical networks has been shown to be NP-complete. In this paper, we propose a new approach to solving the RWA problem using advanced Boolean satisfiability (SAT) techniques. SAT has been heavily researched in the last few years. Significant advances have been proposed and have lead to the development of powerful SAT solvers that can handle very large problems. SAT solvers use intelligent search algorithms that can traverse the search space and efficiently prune parts that contain no solutions. These solvers have recently been used to solve many challenging problems in Engineering and Computer Science. In this paper, we show how to formulate the RWA problem as a SAT instance and evaluate several advanced SAT techniques in solving the problem. Our approach is verified on various network topologies. The results are promising and indicate that using the proposed approach can improve on previous techniques.

Optimized solvers for the Boolean satisfiability (SAT) problem have many applications in areas such as hardware and software verification, FPGA routing, planning, and so forth. Further uses are complicated by the need to express "counting constraints" in conjunctive normal form (CNF). Expressing such constraints by pure CNF leads to more complex SAT instances. Alternatively, those constraints can be handled by integer linear programming (ILP), but generic ILP solvers may ignore the Boolean nature of 0-1 variables. Therefore, specialized 0-1 ILP solvers extend SAT solvers to handle these so-called "pseudo-Boolean" (PB) constraints. This work provides an update on the on-going competition between generic ILP techniques and specialized 0-1 ILP techniques. To make a fair comparison, we generalize recent ideas for fast SAT-solving to more general 0-1 ILP problems that may include counting constraints and optimization. This generalization is embodied in our PB constraint solver and optimizer PBS, which is compared with state-of-the-art CNF and generic ILP solvers. Another aspect of our comparison is the evaluation on 0-1 ILP benchmarks that originate in electronic design automation (EDA) but that cannot be directly solved by an SAT solver. Specifically, we solve instances of the max-SAT and max-ONEs optimization problems, which seek to maximize the number of satisfied clauses and the "true" values over all satisfying assignments, respectively. Those problems have straightforward applications to SAT-based routing and are additionally important due to reductions from max-cut, max-clique, and min vertex cover. Our experimental results show that specialized 0-1 techniques implemented in PBS tend to outperform generic ILP techniques on Boolean optimization problems, as well as on general EDA SAT problems.

To excite a stuck-open fault in a CMOS combinational circuit, it is only necessary that the output of the gate containing the fault takes on opposite values during the application of two successive input vectors to the primary inputs of the circuit. In this paper we formulate the excitation problem as an ILP instance and use two advanced ILP solvers, one is Boolean satisfiability (SAT)-based and the other is generic, to search for a pair of input vectors that maximizes the simultaneous excitation of as many stuck-open faults in the circuit as possible. The proposed approach was tested using benchmarks from the ISCAS 89 suite of circuits. Experimental results indicate that fault-excitation, within a reasonable CPU time limit, is possible in most cases.

Unmanned aerial vehicles (UAVs) represent an important class of networked robotic applications that must be both highly dependable and autonomous. This paper addresses sensor selection and placement problems for distributed failure diagnosis in such networks where multiple vehicles must agree on the fault status of another UAV. An integer linear programming (ILP) approach is proposed to solve these problems. The ILP models of interest are developed and solved using two different solvers. Experimental results indicate that the proposed models are tractable for medium-sized topologies

To achieve high reliability in VLSI designs, estimation of the maximum power dissipation during the design cycle is becoming important. In previous work, it was shown that maximizing dissipation is equivalent to maximizing gate output activity, appropriately weighted to account for differing load capacitances. Recent advances in Boolean satisfiability (SAT) models and algorithms have made it tempting to use satisfiability-based techniques in solving various VLSI design-related problems such as verification and test generation. SAT solvers have also been extended to handle 0-1 integer linear programming (ILP) problems. In this paper, we present an ILP-based solution to compute the maximum weighted activity of combinational circuits. The problem is formulated as an ILP instance and the new SAT-based ILP solvers are used to find an estimate for the power dissipation. For performance comparison, the problem is also solved using generic ILP solvers. The validity of the proposed approach is demonstrated using benchmarks from the MCNC suite

Code optimization and high level synthesis can be posed as constraint satisfaction and optimization problems, such as graph coloring used in register allocation. Graph coloring is also used to model more traditional CSPs relevant to AI, such as planning, time-tabling and scheduling. Provably optimal solutions may be desirable for commercial and defense applications. Additionally, for applications such as register allocation and code optimization, naturally-occurring instances of graph coloring are often small and can be solved optimally. A recent wave of improvements in algorithms for Boolean satisfiability (SAT) and 0-1 Integer Linear Programming (ILP) suggests generic problem-reduction methods, rather than problem-specific heuristics, because (1) heuristics may be upset by new constraints, (2) heuristics tend to ignore structure, and (3) many relevant problems are provably inapproximable. Problem reductions often lead to highly symmetric SAT instances, and symmetries are known to slow down SAT solvers. In this work, we compare several avenues for symmetry breaking, in particular when certain kinds of symmetry are present in all generated instances. Our focus on reducing CSPs to SAT allows us to leverage recent dramatic improvement in SAT solvers and automatically benefit from future progress. We can use a variety of black-box SAT solvers without modifying their source code because our symmetry-breaking techniques are static, i.e., we detect symmetries and add symmetry breaking predicates (SBPs) during pre-processing. An important result of our work is that among the types of instance-independent SBPs we studied and their combinations, the simplest and least complete constructions are the most effective. Our experiments also clearly indicate that instance-independent symmetries should mostly be processed together with instance-specific symmetries rather than at the specification level, contrary to what has been suggested in the literature.

Identifying and breaking the symmetries of conjunctive normal form (CNF) formulae has been shown to lead to significant reductions in search times. Symmetries in the search space are broken by adding appropriate symmetry-breaking predicates (SBPs) to an SAT instance in CNF. The SBPs prune the search space by acting as a filter that confines the search to nonsymmetric regions of the space without affecting the satisfiability of the CNF formula. For symmetry breaking to be effective in practice, the computational overhead of generating and manipulating SBPs must be significantly less than the runtime savings they yield due to search space pruning. In this paper, we describe a more systematic and efficient construction of SBPs. In particular, we use the cycle structure of symmetry generators, which typically involve very few variables, to drastically reduce the size of SBPs. Furthermore, our new SBP construction grows linearly with the number of relevant variables as opposed to the previous quadratic constructions. Our empirical data suggest that these improvements reduce search runtimes by one to two orders of magnitude on a wide variety of benchmarks with symmetries.

With impressive progress in Boolean Satisfiability (SAT) solving and several extensions to pseudo-Boolean (PB) constraints, many applications that use SAT, such as high-performance formal verification techniques are still restricted to checking satisfiability of certain conditions. However, there is also frequently a need to express a preference for certain solutions. Extending SAT-solving to Boolean optimization allows the use of objective functions to describe a desirable solution. Although recent work in 0-1 Integer Linear Programming (ILP) offers extensions that can optimize a linear objective function, this is often achieved by solving a series of SAT or ILP decision problems. Our work articulates some pitfalls of this approach. An objective function may complicate the use of any symmetry that might be present in the given constraints, even when the constraints are unsatisfiable and the objective function is irrelevant. We propose several new techniques that treat objective functions differently from CNF/PB constraints and accelerate Boolean optimization in many practical cases. We also develop an adaptive flow that analyzes a given Boolean optimization problem and picks the symmetry-breaking technique that is best suited to the problem characteristics. Empirically, we show that for non-trivial objective functions that destroy constraint symmetries, the benefit of static symmetry-breaking is lost but dynamic symmetry-breaking accelerates problem-solving in many cases. We also introduce a new objective function, Localized Bit Selection (LBS), that can be used to specify a preference for bit values in formal verification applications.

Code optimization and high level synthesis can be posed as constraint satisfaction and optimization problems, such as graph coloring used in register allocation. Naturally-occurring instances of such problems are often small and can be solved optimally. A recent wave of improvements in algorithms for Boolean satisfiability (SAT) and 0-1 ILP suggests generic problem-reduction methods, rather than problem-specific heuristics, because: (1) heuristics are easily upset by new constraints; (2) heuristics tend to ignore structure; and (3) many relevant problems are provably inapproximable. The NP-spec project offers a language to specify NP-problems and automatic reductions to SAT. Problem reductions often lead to highly symmetric SAT instances, and symmetries are known to slow down SAT solvers. In this work, we compare several avenues for symmetry-breaking, in particular when certain kinds of symmetry are present in all generated instances. Our surprising conclusion is that instance-independent symmetries should often be processed together with instance-specific symmetries rather than earlier, at the specification level.

We present empirical analyses of two Boolean satisfiability (SAT) formulations of FPGA (field programmable gate array) detailed routing constraints. Boolean SAT-based routing transforms a routing problem into a Boolean SAT instance by rendering geometric routing constraints as an atomic Boolean function. The generated Boolean function is satisfiable if and only if the corresponding routing is possible. Two different Boolean SAT-based routing models are analyzed: the track-based and the route-based routing constraint model. The track-based routing model transforms a routing task into a net-to-track assignment problem, whereas the route-based routing model reduces it into a routability-checking problem with explicitly enumerated set of detailed routes for nets. In both models, routing constraints are represented as CNF Boolean satisfiability clauses. Through comparative experiments, we demonstrate that the route-based formulation yields an easier-to-evaluate and more scalable routability Boolean function than the track-based method. This is empirical evidence that a smart/efficient Boolean formulation can achieve significant performance improvement in real-world applications.

Boolean satisfiability (SAT) solvers have experienced dramatic improvements in their performance and scalability over the last several years [5, 7] and are now routinely used in diverse EDA applications. Nevertheless, a number of practical SAT instances remain difficult to solve [9] and continue to defy even the best available SAT solvers [5, 7]. Recent work pointed out that symmetries in the Boolean search space are often to blame. A theoretical framework for detecting and breaking such symmetries was introduced in [2]. This framework was subsequently extended, refined, and empirically shown to yield significant speed-ups for a large number of benchmark classes in [1].Symmetries in the search space are broken by adding appropriate symmetry-breaking predicates (SBPs) to a SAT instance in conjunctive normal form (CNF). The SBPs prune the search space by acting as a filter that confines the search to non-symmetric regions of the space without affecting the satisfiability of the CNF formula. For symmetry breaking to be effective in practice, the computational overhead of generating and manipulating the SBPs must be significantly less than the run time savings they yield due to search space pruning. In this paper we present several new constructions of SBPs that improve on previous work. Specifically, we give a linear-sized CNF formula that selects lex-leaders (among others) for single permutations. We also show how that formula can be simplified by taking advantage of the sparsity of permutations. We test these improvements against earlier constructions and show that they yield smaller SBPs and lead to run time reductions on many benchmarks.

The MINCE heuristic for variable-ordering [1] can successfully reduce the size of BDDs and accelerate SAT-solving. Applications to reachability analysis have also been successful [12]. The main drawback of MINCE is its implementation complexity - the authors used a pre-existing min-cut placer [6] that is several times larger than any existing SAT solver. Tweaking MINCE is difficult.In this work we propose a replacement heuristic, FORCE which is easy to implement from scratch and tweak. It is dramatically faster than MINCE in practice. While FORCE may produce seemingly inferior variable orderings, the difference with MINCE orderings does not affect subsequent SAT-solving.

Research in algorithms for Boolean satisfiability (SAT) and their implementations (Goldberg and Novikov, 2002), (Moskewicz et al., 2001), (Silva and Sakallah, 1999) has recently outpaced benchmarking efforts. Most of the classic DIMACS benchmarks (ftp:dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf ) can now be solved in seconds on commodity PCs. More recent benchmarks (Velev and Bryant, 2001) take longer to solve due to their large size, but are still solved in minutes. Yet, relatively small and difficult SAT instances must exist if P /spl ne/ NP. To this end, our paper articulates SAT instances that are unusually difficult for their size, including satisfiable instances derived from very large scale integration (VLSI) routing problems. With an efficient implementation to solve the graph automorphism problem (McKay, 1990), (Soicher, 1993) (Spitznagel, 1994), we show that in structured SAT instances, difficulty may be associated with large numbers of symmetries. We point out that a previously published symmetry extraction mechanism (Crawford et al., 1996) based on a reduction to the graph automorphism problem often produces many spurious symmetries. Our paper contributes two new reductions to graph automorphism, which extract all correct symmetries found previously (Crawford et al., 1996) as well as phase-shift symmetries not found earlier. The correctness of our reductions is rigorously proven, and they are evaluated empirically. We also formulate an improved construction of symmetry-breaking clauses in terms of permutation cycles and propose to use only generators of symmetries in this process. These ideas are implemented in a fully automated flow that first extracts symmetries from a given SAT instance, preprocesses it by adding symmetry-breaking clauses, and then calls a state-of-the-art backtrack SAT solver. Significant speed-ups are shown on many benchmarks versus direct application of the solver. In an attempt to further improve the practicality of our approach, we propose a scheme for fast "opportunistic" symmetry extraction and also show that considerations of symmetry may lead to more efficient reductions to SAT in the VLSI routing domain.

We introduce Satometer, a tool that can be used to estimate the percentage of the search space actually explored by a backtrack Boolean satisfiability (SAT) solver. Satometer calculates a normalized minterm count for those portions of the search space identified by conflicts. The computation is carried out using a zero-suppressed binary decision diagram data structure and can have adjustable accuracy. The data provided by Satometer can help diagnose the performance of SAT solvers and can shed light on the nature of a SAT instance.

Research in algorithms for Boolean satisfiability and their implementations [23, 6] has recently outpaced benchmarking efforts. Most of the classic DIMACS benchmarks [10] can be solved in seconds on commodity PCs. More recent benchmarks take longer to solve because of their large size, but are still solved in minutes [25]. Yet, small and difficult SAT instances must exist because Boolean satisfiability is NP-complete.We propose an improved construction of symmetry-breaking clauses [9] and apply it to achieve significant speed-ups over current state-of-the-art in Boolean satisfiability. Our techniques are formulated as pre-processing and can be applied to any SAT solver without changing its source code. We also show that considerations of symmetry may lead to more efficient reductions to SAT in the routing domain.Our work articulates SAT instances that are unusually difficult for their size, including satisfiable instances derived from routing problems. Using an efficient implementation to solve the graph automorphism problem [18, 20, 22], we show that in structured SAT instances difficulty may be associated with large numbers of symmetries.

We introduce Satometer, a tool that can be used to estimate the percentage of the search space actually explored by a backtrack SAT solver. Satometer calculates a normalized minterm count for those portions of the search space identified by conflicts. The computation is carried out using a zero-suppressed BDD data structure and can have adjustable accuracy. The data provided by Satometer can help diagnose the performance of SAT solvers and can shed light on the nature of a SAT instance.

We introduce a new approach to Boolean satisfiability (SAT) that combines backtrack search techniques and zero-suppressed binary decision diagrams (ZBDDs). This approach implicitly represents SAT instances using ZBDDs, and performs search using an efficient implementation of unit propagation on the ZBDD structure. The adaptation of backtrack search algorithms to such an implicit representation allows for a potential exponential increase in the size of problems that can be handled.

Optimized solvers for the Boolean Satisfiability (SAT) problem have many applications in areas such as hardware and software verification, FPGA routing, planning, etc. Further uses are complicated by the need to express "counting constraints" in conjunctive normal form (CNF). Expressing such constraints by pure CNF leads to more complex SAT instances. Alternatively, those constraints can be handled by Integer Linear Programming (ILP), but generic ILP solvers may ignore the Boolean nature of 0--1 variables. Therefore specialized 0--1 ILP solvers extend SAT solvers to handle these so-called "pseudo-Boolean" constraints.This work provides an update on the on-going competition between generic ILP techniques and specialized 0--1 ILP techniques. To make a fair comparison, we generalize recent ideas for fast SAT-solving to more general 0--1 ILP problems that may include counting constraints and optimization. Another aspect of our comparison is evaluation on 0--1 ILP benchmarks that originate in Electronic Design Automation (EDA), but that cannot be directly solved by a SAT solver. Specifically, we solve instances of the Max-SAT and Max-ONEs optimization problems which seek to maximize the number of satisfied clauses and the "true" values over all satisfying assignments, respectively. Those problems have straightforward applications to SAT-based routing and are additionally important due to reductions from Max-Cut, Max-Clique, and Min Vertex Cover. Our experimental results show that specialized 0--1 techniques tend to outperform generic ILP techniques on Boolean optimization problems as well as on general EDA SAT problems.

Boolean functions are fundamental to synthesis and verification of digital logic, and compact representations of Boolean functions have great practical significance. Popular representations, such as CNF, DNF, circuits and ROBDDs [4], offer different advantages and are preferred for different tasks. Conversion between those representations is common, especially when one is used to represent the input and another speeds up relevant algorithms. Our work addresses the construction of ROBDDs that represent outputs of a given Boolean circuit. It is used in synthesis and verification. Earlier works (Fujita, Fujisawa, and Kawato, 1988. Malik et al., 1988.) proposed ordering circuit inputs and gates by graph traversals. We contribute orderings based on circuit partitioning and placement, leveraging the progress in recursive bisection and multi-level min-cut partitioning achieved in late 1990s. Our empirical results show that the proposed orderings based on circuit partitioning and placement are more successful than straightforward DFS and BFS, as well as related heuristics.

We introduce a new verification methodology for modern micro-processors that uses a simple checker processor to validate the exe-cution of a companion high-performance processor. The checker can be viewed as an at-speed emulator that is formally verified to be compliant to an ISA specification. This verification approach en-ables the practical deployment of formal methods without impact-ing overall performance.

The increasing popularity of SAT and BDD techniques in verification and synthesis encourages the search for additional speed-ups. Since typical SAT and BDD algorithms are exponential in the worst-case, the structure of real-world instances is a natural source of improvements. While SAT and BDD techniques are often presented as mutually exclusive alternatives, our work points out that both can be improved via the use of the same structural properties of instances. Our proposed methods are based on efficient problem partitioning and can be easily applied as pre-processing with arbitrary SAT solvers and BDD packages without source code modifications. Our contribution is validated on the ISCAS circuits and the DIMACS benchmarks. Empirically, our technique often outperforms existing techniques by a factor of two or more. Our results motivate search for stronger dynamic ordering heuristics and combined static/dynamic techniques.

A Boolean-based router expresses the routing constraints as a Bool?ean function which is satisfiable if and only if the layout is routable. Compared to traditional routers, Boolean-based routers offer two unique features: (1) simultaneous embedding of all nets regardless of net ordering, and (2) ability to demonstrate routing infeasibility by proving the unsatisfiability of the generated routing constraint Boolean function. In this paper, we introduce a new Boolean-based FPGA detailed routing formulation that yields an easy-to-evaluate and more scalable routability Boolean function than the previous methods. The routability constraints are expressed in terms of a set of route variables each of which designating a specific detailed route for a given net. Experimental results clearly show the superi?ority of this formulation over an earlier formulation that expressed the constraints in terms of track variables.

Interest in propositional satisfiability (SAT) has been on the rise lately, spurred in part by the recent availability of powerful solvers that are sufficiently efficient and robust to deal with the large-scale SAT problems that typically arise in electronic design automation application. A frequent question that CAD tool developers and users typically ask is which of these various solvers is "best"; the quick answer is, of course, "it depends". In this paper we attempt to gain some insight into, rather than definitively answer, this question.