Timetabler
|
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< CClause > | getClauses () 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. | |
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.
Clauses::Clauses | ( | const std::vector< CClause > & | clauses | ) |
Constructs the Clauses object.
[in] | clauses | The clauses in the set of clauses |
Clauses::Clauses | ( | const CClause & | clause | ) |
Constructs the Clauses object.
[in] | clause | A single clause that forms the set of clauses |
Clauses::Clauses | ( | const Lit & | lit | ) |
Constructs the Clauses object.
[in] | lit | A 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.
[in] | var | A 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 |
void Clauses::addClauses | ( | const CClause & | other | ) |
void Clauses::addClauses | ( | const std::vector< CClause > & | other | ) |
void Clauses::addClauses | ( | const Clauses & | other | ) |
std::vector< CClause > Clauses::getClauses | ( | ) | const |
Gets the clauses in this object.
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.
other | The Clauses with which AND is performed |
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.
other | The Clauses object which is implied by this object |
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 ...
x | y
other | The Clauses object to perform the OR operation with |
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.