CQU Files

----------------
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.

Copying  conditions  about  psat-minisat  can   be  found  in  the  'LICENSE',
'LICENSE-minisat' and 'LICENSE-CoinCl' files.

To contact the author: marcelo.finger@gmail.com

---------------
Installation
---------------

You  must have  in your  computer the  compilers gcc  and g++.   The necessary
libraries  (linux   64bits)  are   inserted  in  the   package  in   the  lib/
directory.  For other  installations, one  may need  to get  the corresponding
libClp and libClpUtils libraries. 

To compile the cqusat, all you have to do is type, at the
directory where all source files have been placed, 

$ make

To remove all compiled files, just type

$ make clean

There  is no  need to  separately install  the minisat  SAT solver,  as it  is
included in the code.  

---------------
Using cqusat
---------------

See the usage.txt file included in this package.