----------------
cqusat 1.0
----------------

cqusat is a conbstraint solver decides the satisfiability of a set of sentences containing Counting Quantifiers over Unary predicates. It also accepts Universally quantifies sentences over unary predicates, which are presented in the form of propositional clauses (classical Boolean logic
clauses). This implementation employs minisat as the SAT solver. It also emplouys COIN-OR Clp linear programming solver, and inherit from it.

Given a CQUSAT instance in normal form as input, the program returns a solution, if there is one. The implemented method employs dual Simplex Algorithm with Column Generation.

At each iteration, a SAT instance is generated and a SAT Solver (minisat) decides its satisfiability. Details about CQUSAT, its normal form and this turing reduction can be found in the paper
"CQUSAT.pdf" that comes with this package.

For more information, see the README file.

Features

  • Solving Constraints in the formar of Counting Quantifiers over Unary predicates

Project Activity

See All Activity >

Follow CQU

CQU Web Site

Other Useful Business Software
Simplify IT and security with a single endpoint management platform Icon
Simplify IT and security with a single endpoint management platform

Automate the hardest parts of IT

NinjaOne automates the hardest parts of IT, delivering visibility, security, and control over all endpoints for more than 20,000 customers. The NinjaOne automated endpoint management platform is proven to increase productivity, reduce security risk, and lower costs for IT teams and managed service providers. The company seamlessly integrates with a wide range of IT and security technologies. NinjaOne is obsessed with customer success and provides free and unlimited onboarding, training, and support.
Learn More
Rate This Project
Login To Rate This Project

User Reviews

Be the first to post a review of CQU!

Additional Project Details

Registered

2016-11-27