/* przyklad pliku .lp dla lp_solve, problem: MAX-SAT a*/
/* liczba zmiennych: 6 */
/* liczba klauzul: 5 */
/* xi - wartosc i-tej zm. binarnej */
/* ci - liczba 1-ek w i-tej klauzuli */
/* bi - wartosc i-tej klauzuli */
/* klauzule: */
/* ' - negacja
(x1+x2')
(x2+x3+x4)
(x3'+x4'+x5)
(x1+x3')
(x4+x5')

Negacje zapisujemy jako x'=1-x, np.:
x2'=1-x2
*/

max: liczba_spelnionych;

b1 + b2 + b3 + b4 + b5 - liczba_spelnionych =0;

/* ograniczenie - wartosc klauzul */

x1 - x2 - c1 = -1;
x2 + x3 + x4 - c2 = 0;
- x3 - x4 + x5 - c3= -2;
x1 - x3 - c4 = -1;
x4 - x5 - c5 = -1;

/* wartosc klauzul musi byc binarna */
b1-c1 <=0;
b2-c2 <=0;
b3-c3 <=0;
b4-c4 <=0;
b5-c5 <=0;

/* zmienne binarne */
bin x1, x2, x3, x4, x5, x6;
int c1, c2, c3, c4, c5;
bin b1, b2, b3, b4, b5;