Go to the content (press return)

Theory and applications in satisfiability and constraint optimization

Total activity: 7
Type of activity
Competitive project
Funding entity
Funding entity code
52.743,90 €
Start date
End date
algorithms, algoritmos, complejidad computacional, computational complexity, constraint optimization, constraint satisfaction, lógica proposicional, optimización de restricciones, propositional logic, satisfacción de restricciones
This project pivots around the satisfiability and constraint optimization problems for logical languages including propositional logic (SAT) and more
general expressive constraint satisfaction problems (CSP). Our purpose is to conduct frontier research in this area exploiting the expertise of the four
groups that participate in the project. TASSAT 2 is the continuation of the project that gives birth to it, TASSAT, that already proved its potential and
viability. For this reason, the main objectives of this project are partly follow-ups on those of the previous project and partly new, with the following
concrete goals in particular:
In SAT we want to continue studying the structure of instances arising in industry, and apply this knowledge to develop more efficient solvers, both for
SAT and for MAXSAT. In CSP we want to continue contributing to the problem of classification of tractable constraint languages. We will also study
algorithms for geometric instances of MAXCSP and combinatorial problems of interest in computational complexity theory. An important novelty of the
present proposal is its stronger emphasis in the implementation of practical solvers, including new branch-and-bound algorithms for MAXSAT, soft
learning for MAXSAT, better variable selection techniques, portfolios, etc. We want to expand our presence in international solver competitions and
participate in the solution of industrial problems. Another significant novelty in the goals is that we plan to expand the range of applications of the
geometric methods to include graph isomorphism problems and other structures of interest in combinatorics and other areas of science. This new goal
derives from some of the results obtained in the previous project that already had a notable international impact.
Efficiency appears as one of the keywords in the ICT-related activities of the European H2020 (see SC4 and SC5 in "Societal challenges"). This may
refer to efficiency in energy distribution, logistics applications, etc. SAT and MAXSAT solvers are a relatively new technology for optimization that can be
applied in some of these areas. One of our goals in this project is to consolidate a consortium of research groups in the area, to compete in the
application of European research projects.
Adm. Estat
Plan Estatal de Investigación Científica y Técnica y de Innovación 2013-2016
Call year
Funcding program
Programa Estatal de Fomento de la Investigación Científica y Técnica de Excelencia
Funding subprogram
Subprograma Estatal de Generación de Conocimiento
Funding call
Excelencia: Proyectos I+D
Grant institution
Gobierno De España. Ministerio De Economía Y Competitividad, Mineco


Scientific and technological production

1 to 7 of 7 results
  • Generalized satisfiability problems via operator assignments  Open access

     Atserias, A.; Kolaitis, Ph.; Severini, S.
    Journal of computer and system sciences
    Vol. 105, p. 171-198
    DOI: 10.1016/j.jcss.2019.05.003
    Date of publication: 2019-11
    Journal article
    Access to the full text
  • Quantum and non-signalling graph isomorphisms

     Atserias, A.; Mancinska, L.; Roberson, D.; Samal, R.; Severini, S.; Varvitsiotis, A.
    Journal of combinatorial theory. Series B
    Vol. 136, p. 289-328
    DOI: 10.1016/j.jctb.2018.11.002
    Date of publication: 2019-05
    Journal article
  • Relative entailment among probabilistic implications  Open access

     Atserias, A.; Balcazar, J. L.; Piceno, M.
    Logical methods in computer science
    Vol. 15, num. 1, p. 10:1-10:30
    DOI: 10.23638/LMCS-15(1:10)2019
    Date of publication: 2019-02-06
    Journal article
    Access to the full text
  • Proof complexity meets algebra  Open access

     Atserias, A.; Ochremiak, J.
    ACM transactions on computational logic
    Vol. 20, num. 1, p. 1:1-1:46
    DOI: 10.1145/3265985
    Date of publication: 2018-12-01
    Journal article
    Access to the full text
  • Definable inapproximability: New challenges for duplicator  Open access

     Atserias, A.; Dawar, A.
    Annual Conference on Computer Science Logic
    p. 1-21
    DOI: 10.4230/LIPIcs.CSL.2018.7
    Presentation's date: 2018-09-04
    Presentation of work at congresses
    Access to the full text
  • Short proofs of the Kneser-Lovász coloring principle

     Aisenberg, J.; Bonet, M.; Buss, S.; Craciun, A.; Istrate, G.
    Information and computation
    Vol. 261, Part 2, p. 296-310
    DOI: 10.1016/j.ic.2018.02.010
    Date of publication: 2018-08
    Journal article
  • Narrow proofs may be maximally long  Open access

     Atserias, A.; Lauria, M.; Nordström, J.
    ACM transactions on computational logic
    Vol. 17, num. 3, p. 19:1-19:30
    DOI: 10.1145/2898435
    Date of publication: 2016-07-03
    Journal article
    Access to the full text