Activity Feed

Bio small

Dewald d. added photos to project Resolver

Medium 500e3f6a d804 48b3 a8b3 7b8cfb9814ee

Resolver

The boolean satisfiability problem (SAT) is the first problem to be proven NP-complete. In the last decade, the usefulness of SAT has increased so much that much effort has been put into improving technology that can find solutions to these satisfiability problems (SAT solvers). SAT solvers can be split into two main categories: Complete and incomplete. Complete SAT solvers are guaranteed to find a satisfying assignment if one exists (Given enough time) while incomplete solvers are not. Many different kinds of problems can be encoded as a propositional logic formula and then fed into a SAT solver to find a solution to the problem. The areas of application include, but are not limited to, formal software verification, scheduling tasks, automated mathematical proofs and hardware and software design.

This project is aimed at making progress in the development of an incomplete SAT solver that makes use of concepts from artificial intelligence and certain heuristics to improve solving time. Some solvers of interest are WalkSAT, GSAT and FlipGA. Research on improving FlipGA and developing crossover operators that work better in the context of SAT has been done by Lardeux et al. and the GASAT algorithm was born. This algorithm makes use of a genetic algorithm and three proposed crossover operators. Furthermore, a local search algorithm, specifically tabu search, is used to guide the search. This project includes implementing the GASAT algorithm and running experiments with several different configurations. This is done via a randomized grid search to optimise the parameters for specific problems and then trying to find a general trend. We hope to make a breakthrough in applying evolutionary algorithms to SAT and contribute to the scientific community.

We are a team of 5 undergraduate students at the University of Pretoria and are doing this project as part of our final year project for an undergraduate computer science degree. Our leaders in the project are two post-doctoral researchers in the field of formal software verification and who wish to use this project to further their research in bounded model checking.

Medium bio small

Dewald d. created project Resolver

Medium 500e3f6a d804 48b3 a8b3 7b8cfb9814ee

Resolver

The boolean satisfiability problem (SAT) is the first problem to be proven NP-complete. In the last decade, the usefulness of SAT has increased so much that much effort has been put into improving technology that can find solutions to these satisfiability problems (SAT solvers). SAT solvers can be split into two main categories: Complete and incomplete. Complete SAT solvers are guaranteed to find a satisfying assignment if one exists (Given enough time) while incomplete solvers are not. Many different kinds of problems can be encoded as a propositional logic formula and then fed into a SAT solver to find a solution to the problem. The areas of application include, but are not limited to, formal software verification, scheduling tasks, automated mathematical proofs and hardware and software design.

This project is aimed at making progress in the development of an incomplete SAT solver that makes use of concepts from artificial intelligence and certain heuristics to improve solving time. Some solvers of interest are WalkSAT, GSAT and FlipGA. Research on improving FlipGA and developing crossover operators that work better in the context of SAT has been done by Lardeux et al. and the GASAT algorithm was born. This algorithm makes use of a genetic algorithm and three proposed crossover operators. Furthermore, a local search algorithm, specifically tabu search, is used to guide the search. This project includes implementing the GASAT algorithm and running experiments with several different configurations. This is done via a randomized grid search to optimise the parameters for specific problems and then trying to find a general trend. We hope to make a breakthrough in applying evolutionary algorithms to SAT and contribute to the scientific community.

We are a team of 5 undergraduate students at the University of Pretoria and are doing this project as part of our final year project for an undergraduate computer science degree. Our leaders in the project are two post-doctoral researchers in the field of formal software verification and who wish to use this project to further their research in bounded model checking.

About

Featured Projects

See All

Bigger abstract 0021
  • Projects 1
  • Followers 9

Keoagile Dinake

University of Pretoria Student.. Freerunner for MunkieZA, freelance web developer, and producer

81 Cunningham Ln, Akasia, 0201, South Africa

Bigger 16406830 606334852894281 907894597027123666 n
  • Projects 0
  • Followers 6

Joel Tiogo

Electrical technician and Programmer.

77 Edgar Rd, Eveleigh, Boksburg, 1459, South Africa

Medium real sense
Featured
  • Followers 1430

Intel RealSense™

Natural interaction, immersive, collaboration, gaming and learning, 3D scanning. Integrate tracki...

Medium android
Featured
  • Followers 1452

Android

Intel is inside more and more Android devices, and we have tools and resources to make your app d...

Medium big data
Featured
  • Followers 1500

Modern Code

Drive faster breakthroughs through faster code: Get more results on your hardware today and carry...

Medium networking
Featured
  • Followers 1371

Networking

Software-Defined Networking (SDN) and Network Functions Virtualization (NFV) are transforming the...

Medium achievement unlocked logo
Featured
  • Followers 1304

Game Development

Upgrade your skills as a game developer, share your game projects, and connect with other develop...

Medium mesh robotics
  • Followers 210

Robotics

Flying, walking, and roving machines. Browse the expertise on display in these robotics projects.

Medium vr large 575x441
Featured
  • Followers 995

Virtual Reality

VR, AR, mixed reality...you'll find projects based on all these new platforms here. Share your own!

No users to show at the moment.