Time
Teaching

Current courses - rozvrh ZS2011
   ------

Courses - 2010/2011
  BI-CAO - Číslicové a analogové obvody
  BI-SAP - Struktura a architektura počítačů

Courses - 2009/2010
  X36PJC - Programovací jazyk C++
  Y36ALG - Algoritmizace

Nabízené bakalářské a diplomové práce

  • Prozkoumejte možnosti rozšíření ATPG (Automatic Test Patterns Generator) SAT-Solveru (MiniSat, zChaff, ...) o techniku "aktivace klauzulí", "preprocessing" a "postprocessing" ke zvýšení počtu DC (Don't Care) bitů. Proveďte srovnání původní a rozšířené verze SAT-Solveru pro různé typy instancí SAT problému (umělé instance vs. instance generované v ATPG).
    -> Programovací jazyk C, C++
    -> SAT-Solver=nástroj řešící splnitelnost booleovské formule

    SP, BP, DP


  • Prozkoumejte možnosti vnitřní reprezentace klauzulí SAT-Solveru (MiniSat, zChaff, ...). Upravte vnitřní reprezentaci zvoleného SAT-Solveru a prohledávácí heuristiku na reprezentaci klauzulí pomocí ZDD (Zero-Suppressed Decision Diagram). Zjistěte možnosti komprese instance SAT problému pomocí ZDD a vliv vnitřní reprezentace na rychlost řešení. Měření proveďte pro umělé a ATPG (Automatic Test Patterns Generator) SAT instance.
    -> Programovací jazyk C, C++
    -> SAT instance=problém splnitelnosti zadán jako booleovská formule v konjunktivní normální formě; SAT-Solver=nástroj řešící splnitelnost booleovské formule

    DP (SP, BP)


  • Prozkoumejte možnosti vnitřní reprezentace klauzulí SAT-Solveru (MiniSat, zChaff, ...). Upravte vnitřní reprezentaci zvoleného SAT-Solveru a prohledávácí heuristiku na reprezentaci klauzulí pomocí BDD (Binary Decision Diagram). Porovnejte vliv vnitřní reprezentace na rychlost řešení. Měření proveďte pro umělé a ATPG (Automatic Test Patterns Generator) SAT instance.
    -> Programovací jazyk C, C++
    -> SAT instance=problém splnitelnosti zadán jako booleovská formule v konjunktivní normální formě; SAT-Solver=nástroj řešící splnitelnost booleovské formule

    DP (SP, BP)


  • Prozkoumejte možnosti SSMIBDDs (Structurally Synthesized Multiple Input BDDs) v simulaci digitálních obvodů a implementujte simulátor poruch využívající tuto reprezentaci. Vaše řešení porovnejte se stávajícími simulátory a výsledky zhodnoťe.
    -> Programovací jazyk C, C++

    SP, BP, DP


  • Prostudujte možnosti generování SAT instance v CNF (Conjunctive Normal Form) reprezentující množinu testovacích vektorů pro poruchu v digitálním obvodu. Implementujte několik způsobů a proveďte jejich srovnání (velikost, doba generování, rychlost řešení SAT-solvery).
    -> Programovací jazyk C, C++
    -> SAT instance=problém splnitelnosti zadán jako booleovská formule v konjunktivní normální formě; SAT-Solver=nástroj řešící splnitelnost booleovské formule

    SP, BP (DP)


  • Nastudujte problematiku SSMIBDDs (Structurally Synthesized Multiple Input BDDs) a implementujte knihovnu funkcí pro práci s touto strukturou. Funkčnost řešení demonstrujte na jednoduchých příkladech.
    -> Programovací jazyk C, C++

    SP, BP, DP

Last update: 04.09.2011   17:27:36