sukrutrao / Timetabler

A customizable timetabling software for educational institutions that encodes timetabling constraints as a SAT formula and solves them using a MaxSAT solver
https://timetabler.readthedocs.io
MIT License
38 stars 9 forks source link

Use Tseitin encoding to decrease memory usage #6

Closed Siddiq200 closed 6 years ago

Siddiq200 commented 6 years ago
terminate called after throwing an instance of 'std::bad_alloc'
  what():  std::bad_alloc
Aborted (core dumped)

What is the reason of this ERROR.

I entered 50 courses and slots and teachers are enough. but while adding constraints the process is terminated.

Thanks in advance.

prateekkumarweb commented 6 years ago

Current implementation uses lot of memory. Tseitin encoding is to be used to decrease memory footprint.

prateekkumarweb commented 6 years ago

TODO: Use this encoding for disjunction of clauses (Tseitin encoding) Example:

((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
sukrutrao commented 6 years ago

@Siddiq200 This issue has been fixed.