Timetabler
Public Member Functions | List of all members
Clauses Class Reference

Class for representing a set of clauses. More...

#include <clauses.h>

Public Member Functions

 Clauses (const std::vector< CClause > &)
 Constructs the Clauses object. More...
 
 Clauses (const CClause &)
 Constructs the Clauses object. More...
 
 Clauses (const Lit &)
 Constructs the Clauses object. More...
 
 Clauses (const Var &)
 Constructs the Clauses object. More...
 
 Clauses ()
 Constructs the Clauses object, with no clauses in it.
 
Clauses operator~ ()
 Defines the negation operation on a set of clauses. More...
 
Clauses operator& (const Clauses &)
 Defines the conjunction operation between two sets of clauses. More...
 
Clauses operator& (const CClause &)
 Defines the conjunction operation between a Clauses and a CClause. More...
 
Clauses operator| (const Clauses &)
 Defines the disjunction operation between two sets of clauses. More...
 
Clauses operator| (const CClause &)
 Defines the disjunction operation between a Clauses and a CClause. More...
 
Clauses operator>> (const Clauses &)
 Defines the implication operation between two sets of Clauses. More...
 
void addClauses (const CClause &)
 Adds a CClause to the set of clauses. More...
 
void addClauses (const std::vector< CClause > &)
 Adds a vector of CClause to the set of clauses. More...
 
void addClauses (const Clauses &)
 Adds the clauses of a Clauses object to this object. More...
 
std::vector< CClausegetClauses () const
 Gets the clauses in this object. More...
 
void print ()
 Displays the clauses in this object.
 
void clear ()
 Clears the Clauses object by removing all the clauses.
 

Detailed Description

Class for representing a set of clauses.

A set of clauses is represented as a vector of type CClause. This class defines operations between sets of clauses, such as AND, OR, NOT, and IMPLIES. This also defines functions to create Clauses, add clauses, and work with them. All clauses are always maintained in the CNF form.

Constructor & Destructor Documentation

Clauses::Clauses ( const std::vector< CClause > &  clauses)

Constructs the Clauses object.

Parameters
[in]clausesThe clauses in the set of clauses
Clauses::Clauses ( const CClause clause)

Constructs the Clauses object.

Parameters
[in]clauseA single clause that forms the set of clauses
Clauses::Clauses ( const Lit &  lit)

Constructs the Clauses object.

Parameters
[in]litA single literal, a Lit, that is converted to a unit clause and forms the set of clauses
Clauses::Clauses ( const Var &  var)

Constructs the Clauses object.

Parameters
[in]varA single variable, a Var, that is converted to a literal with positive polarity, then converted to a unit clause, which then forms the set of clauses

Member Function Documentation

void Clauses::addClauses ( const CClause other)

Adds a CClause to the set of clauses.

Parameters
[in]otherThe CClause to add
void Clauses::addClauses ( const std::vector< CClause > &  other)

Adds a vector of CClause to the set of clauses.

Parameters
[in]otherThe CClause vector to append
void Clauses::addClauses ( const Clauses other)

Adds the clauses of a Clauses object to this object.

Parameters
[in]otherThe Clauses object whose clauses are to be added
std::vector< CClause > Clauses::getClauses ( ) const

Gets the clauses in this object.

Returns
The clauses
Clauses Clauses::operator& ( const Clauses other)

Defines the conjunction operation between two sets of clauses.

The conjunction of a set of clauses ((a1 OR a2) AND (b1 OR b2)) with ((x1 OR x2) AND (y1 OR y2)) is given by ((a1 OR a2) AND (b1 OR b2) AND (x1 OR x2) AND (y1 OR y2)). Thus, this function performs this concatenation of clauses and returns a Clauses object containing all the clauses.

Parameters
otherThe Clauses with which AND is performed
Returns
A Clauses object with the result of the AND operation
Clauses Clauses::operator& ( const CClause other)

Defines the conjunction operation between a Clauses and a CClause.

Parameters
otherThe CClause with which the AND operation is performed
Returns
A Clauses object with the result of the AND operation
Clauses Clauses::operator>> ( const Clauses other)

Defines the implication operation between two sets of Clauses.

The implication of a set of clauses p to a set of clauses q, which is (p->q), is given by (~p OR q). Thus, this operation is performed using the existing definitions of NOT and OR for sets of clauses.

Parameters
otherThe Clauses object which is implied by this object
Returns
A Clauses object with the result of the implication operation
Clauses Clauses::operator| ( const Clauses other)

Defines the disjunction operation between two sets of clauses.

The disjunction of a set of clauses ((a1 OR a2) AND (b1 OR b2)) with ((x1 OR x2) AND (y1 OR y2)) is given by ((a1 OR a2 OR x1 OR x2) AND (a1 OR a2 OR y1 OR y2) AND (b1 OR b2 OR x1 OR x2) AND (b1 OR b2 OR y1 OR y2)). This function performs this operation and returns a Clauses object with the resultant clauses. Given m clauses in the first operand and n clauses in the second operand, the solution has O(mn) clauses. Using auxiliary variables gives a O(m+n) equisatisfiable formula.

Following is a example with auxiliary variables. ((a1 | a2 | a3 | a4) & (a5 | a6 | ...) & ...) | ((b1 | b2 | b3 | b4) & (b5 | ...) & ...) # Add the following as hard clauses ~x | c1 (c1 is auxiliary variable for (a1 | a2 | a3 | a4)) ... x | ~c1 | c2 | ... ~c1 | a1 | a2 | a3 | a4 c1 | ~a1 c1 | ~a2 ...

Return the following as soft clause

x | y

Parameters
otherThe Clauses object to perform the OR operation with
Returns
A Clauses object with the result of the OR operation
Clauses Clauses::operator| ( const CClause other)

Defines the disjunction operation between a Clauses and a CClause.

Parameters
otherThe CClause to perform the OR operation with
Returns
A Clauses object with the result of the OR operation
Clauses Clauses::operator~ ( )

Defines the negation operation on a set of clauses.

The negation of a set of clauses ((a1 OR a2) AND (b1 OR b2)) is defined as ((~a1 AND ~a2) OR (~b1 AND ~b2)). The OR operation defined in this class is then used to convert the Clauses to CNF form.

Returns
The result of the negation operation on the set of clauses

The documentation for this class was generated from the following files: